Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Riemann Integral of a Vector-Valued or Matrix-Valued Map
definitiondef:riemann-integral-vector-matrix-map-2026aAnalysisLinear AlgebraA map from a set of reals into Euclidean space or into real matrices is integrable on a closed interval when each component or entry is, and its oriented integral is the point or matrix of the componentwise integrals.Derivative of a Vector-Valued or Matrix-Valued Map on an Interval
definitiondef:derivative-vector-matrix-map-2026aAnalysisLinear AlgebraA map from an interval into Euclidean space or into real matrices is differentiable at a point when each of its components or entries is, and its derivative there is the point or matrix of the componentwise derivatives.The Exponential Series Converges Absolutely, and Its Sum Is a Map on ℝ
lemmalem:exponential-series-2026aAnalysisFor every real u the terms u^(k-1)/(k-1)! form a sequence whose series converges absolutely with first term 1, and the sums of these series form a map from the reals to the reals.Power Series: the Sequence of Terms, the Coefficients 1/(k-1)!, and the Sum as a Map on the Set of Convergence
helperhlp:power-series-maps-2026aAnalysisFor a real sequence (c_k), the terms c_k u^(k-1) and the coefficients 1/(k-1)! form sequences of reals, and on a set where the power series converges its sum is a map into the reals.The Reciprocal and the Quotient of Real-Valued Maps with a Nonvanishing Denominator Are Maps
helperhlp:reciprocal-quotient-maps-2026aAnalysisFor real-valued maps f and chi on a set E with chi nowhere zero, the maps t to 1/chi(t) and t to f(t)/chi(t) from E to the reals exist and are unique.Finite Sums of Reals: Congruence, the Product Map (x,y) ↦ f(x)h(y), and the Sequence of Diagonal Sums
helperhlp:finite-sums-congruence-products-2026aAlgebraA finite sum depends only on the values of the summand on the index set; the map (x,y) to f(x)h(y) on a Cartesian product exists; and the sums of a_i b_j over the pairs in [n]x[n] with i+j=n+1 form a sequence of real numbers.Natural Numbers and Factorials Read in the Reals: the Order Carries Over, One Is Least, and Factorials Are Positive, Recursive and Nondecreasing
helperhlp:naturals-factorials-in-reals-2026aAlgebraRead in the real numbers, every natural number is at least 1, and the factorials are at least 1, hence nonzero, satisfy (k+1)! = (k+1) k!, and are nondecreasing.Sequences of Real Numbers Built from Given Ones: Partial Sums, Index Shifts, Predecessor Reindexing, Absolute Values and Termwise Operations
helperhlp:real-sequence-constructions-2026aAnalysisThe partial sums of a real sequence, its index shifts, the reindexing k to k-1 of a map on the natural numbers with zero, its absolute values, and the termwise sums, differences, products, scalar multiples and constants all form sequences of real numbers.- If two series of real numbers converge absolutely, then their Cauchy product, whose n-th term sums the products of terms with indices adding to n+1, converges absolutely, and its sum is the product of the two sums.
Properties of the Natural Logarithm: Values at 1 and e, Products, Quotients, Monotonicity, Continuity, Derivative and the Bound log t at most t - 1
lemmalem:logarithm-properties-2026aAnalysisThe natural logarithm vanishes at 1 and equals 1 at e, turns products into sums and quotients into differences, is strictly increasing and continuous on the positive reals, has derivative 1/t on every subinterval, and satisfies log t at most t - 1.Inverse of a Continuous Strictly Increasing Function on an Interval: Continuity and Derivative
lemmalem:inverse-function-interval-2026aAnalysisA continuous strictly increasing function on an interval maps it bijectively onto an interval; its inverse is strictly increasing and continuous, and is differentiable at f(x) with derivative 1/f'(x) wherever f has a nonzero derivative at x.Substituting Variables and Set Parameters into Predicative Formulas, Extending Assignments, and Finiteness
helperhlp:predicative-substitution-2026aSet TheoryA condition expressed by a predicative formula stays so expressed when its variables are replaced by other variables or by parameters with set values; an assignment of sets extends by one set; and finiteness of one of the variables is expressed by a predicative formula.Elements of a Segment Are Natural Numbers, and Mixed Transitivity of the Order on the Natural Numbers
helperhlp:natural-index-order-2026aSet TheoryEvery element of the natural numbers with zero lying between 1 and a set n, in particular every element of a segment [n], is a natural number; and on the natural numbers a strict and a non-strict inequality in a chain give a strict inequality.Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real
helperhlp:real-type-values-2026bAlgebraDifferences, quotients and absolute values of real numbers taken in ℝ lie in ℝ and match the arithmetic and order of the type Real, with the rules for absolute values, and on reals the order of the extended real line is that of Real.- The real numbers as a Lean type, with the operations and order of ℝ, declared a commutative ring with a compatible total order so that ring and order arithmetic on real numbers can be done by Lean's algebra procedures.
Negatives, Reciprocals and the Strict Order in an Ordered Field, as Values
helperhlp:ordered-field-value-forms-2026aAlgebraIn an ordered field, the negative and the reciprocal lie in the field and satisfy x + (−x) = 0 and x · x⁻¹ = 1, and x < y holds exactly when x ≤ y and not y ≤ x.Predicative Formulas for Bijections from a Segment [n] and for Increasing Listings
helperhlp:segment-listing-predicative-2026aSet TheoryThe conditions that f is a bijection from a segment [n] of the natural numbers onto B, and that x is such a bijection with strictly increasing real values, are expressed by predicative formulas.The Set of Indices n for Which the n-th Map of a Sequence in ℝ^[a,b] Is Integrable with a Prescribed Integral
helperhlp:integral-condition-index-set-2026aAnalysisFor a sequence of real-valued maps on a closed interval [a,b] and a sequence of real numbers, the natural numbers n for which the n-th map is bounded and integrable on [a,b] with integral equal to the n-th number form a set, given by a predicative condition.Darboux Sums of Sums, Scalar Multiples and Dominated Functions, and the Oscillation Bound
lemmalem:darboux-sums-operations-2026aOn a fixed partition, the upper sum is subadditive and the lower sum superadditive, scalar multiples scale the sums (exchanging upper and lower for negative scalars), a bound f ≤ g + c passes to the sums with the term c(b − a), and an oscillation at most η on every subinterval bo…A Predicative Formula for the Oriented Riemann Integral, and Maps Given by Integrals
helperhlp:riemann-integral-predicative-2026aAnalysisFor a map g on a subset E of the reals, the relation between g, two points u and v of E and the oriented integral of g from u to v, where defined, is expressed by a predicative formula; hence indefinite integrals u to the integral from c to u, and sequences of integrals, are maps…