Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
A Finite Set of Real Numbers Has Exactly One Increasing Listing
lemmalem:finite-subset-increasing-listing-2026aAnalysisA set of real numbers with N elements is listed by exactly one bijection from [N] that is strictly increasing.Predicative Formulas for Upper and Lower Darboux Sums, and the Maps and Sets of Darboux Sums over All Partitions
helperhlp:darboux-sums-predicative-2026aAnalysisThe relation between the endpoints, a bounded map on the closed interval, a partition and its upper (or lower) Darboux sum is expressed by a predicative formula; hence the partition-to-sum maps exist and the classes of all upper and all lower sums are sets of real numbers.Sequences of Real-Valued Maps: the Map of Pointwise Limits on a Subset, and the Sequence of Pointwise Partial Sums
helperhlp:sequence-of-maps-limits-sums-2026aAnalysisFor a sequence of real-valued maps on D, the pointwise limits on a subset S where they exist form a unique map on S, and the pointwise partial sums form a unique sequence of maps on D whose value sequences at each point are the partial-sum sequences of the value sequences.The Map of Consecutive Differences of a Finite List of Reals Exists, and Its Sum Telescopes
helperhlp:telescoping-difference-map-2026aAnalysisFor a map d on [n+1] with real values, the consecutive differences k ↦ d(k+1) − d(k) form a unique map on [n], and their sum is d(n+1) − d(1).Extending a Map by One Point, and Extending a Bijection by One Point
helperhlp:map-one-point-extension-2026aSet TheoryA map on A extends uniquely to A together with one new point p, with a prescribed value at p; if the map is a bijection onto C and the new value lies outside C, the extension is a bijection onto C together with that value.Rules for the Riemann Integral: Sums, Scalar Multiples, Monotonicity, Bounds and Constants
lemmalem:riemann-integral-rules-2026aAnalysisThe Riemann integral on a closed interval is additive and homogeneous, monotone, bounded by the bounds of the integrand times the length of the interval, and gives c(b-a) for the constant c.- For a differentiable map phi on [a,b] with continuous derivative and values in an interval J, and a continuous f on J, the map f(phi(t))phi'(t) is integrable on [a,b] and its integral equals the oriented integral of f from phi(a) to phi(b).
- For differentiable F and G on [a,b] with continuous derivatives, FG' and F'G are integrable and the integral of FG' equals F(b)G(b) - F(a)G(a) minus the integral of F'G.
Riemann's Criterion for Integrability, and the Integral Lies between Lower and Upper Sums
lemmalem:riemann-criterion-2026aAnalysisA bounded function on [a,b] is Riemann integrable exactly when, for every positive epsilon, some partition has upper and lower sums less than epsilon apart; and the integral of an integrable function lies between the lower and the upper sum of every partition.Bounds for Darboux Sums, Monotonicity under Refinement, the Supremum of the Lower Sums and the Infimum of the Upper Sums, and Concatenation of Partitions
lemmalem:darboux-sum-bounds-2026aAnalysisDarboux sums lie between m(b-a) and M(b-a), lower sums increase and upper sums decrease under refinement, every lower sum is at most every upper sum, the least upper bound of the lower sums and the greatest lower bound of the upper sums exist and are ordered, and sums over a conc…The Increasing Listing of a Partition: Endpoints, Lengths, Covering, Unions, Inserting a Point, Concatenation and Uniform Partitions
lemmalem:partition-enumeration-2026aAnalysisA partition of [a,b] is listed by exactly one strictly increasing bijection x_1<...<x_{n+1} from [n+1], starting at a and ending at b; the gaps are positive and add up to b-a, the intervals [x_i,x_{i+1}] cover [a,b], unions of partitions are common refinements, and inserting one…The Uniform Cauchy Criterion for Sequences of Real-Valued Maps
lemmalem:uniform-cauchy-criterion-2026aAnalysisA sequence of real-valued maps converges uniformly on a set if and only if it is uniformly Cauchy there; the uniform limit is then the map of pointwise limits, and it is the only pointwise limit.Irreflexivity of the Strict Order and Subtracting Zero in ℝ
helperhlp:real-strict-irreflexive-sub-zero-2026aFor every real number x, x < x fails and x − 0 = x.The Negative of Zero in ℝ, and Multiplying an Inequality on the Left by a Nonnegative Real
lemmalem:real-negative-zero-left-scaling-2026aIn the real numbers the negative of 0 is 0, and multiplying both sides of an inequality on the left by a nonnegative real preserves it.Addition on ℝ Is an Associative and Commutative Binary Operation
helperhlp:real-arithmetic-supplement-2026aAlgebraRestates associativity and commutativity of addition on the reals in the predicate form of the definition of associative and commutative binary operations.- For a map F from a class A to a class B and a in A, the value F(a) is a set, (a, F(a)) lies in F, and F(a) lies in B; in particular the distance d(x, y) of two points of a metric space is a real number.
Predicative Formulas for the Derivative Condition and for Powers
helperhlp:derivative-power-predicative-2026aAnalysisBeing a derivative of a real map on an interval at a point, under the guard that the map, the point and the number have their types, and the relation z = t^m between a real number, an exponent in the natural numbers with zero and the power, are each expressed by a predicative for…Continuity of Identity Maps, Compositions and Reciprocals
lemmalem:continuous-identity-composition-reciprocal-2026aAnalysisThe identity map of a subset of a metric space is continuous on it; a composition of maps continuous at corresponding points, relative to their domains, is continuous there; and the reciprocal of a nonvanishing real function on a subset of the real line is continuous wherever the…Continuity of Real Functions on Subsets of ℝ in ε-δ Form
helperhlp:real-continuity-epsilon-delta-2026aAnalysisFor a map from a subset of the real line into the real line, continuity at a point relative to the subset, and continuity on the subset, are restated with absolute differences in place of the distance.- Elementary identities for differences and quotients of real numbers, the comparison of two reals through their difference, and the signs and absolute values of reciprocals and quotients, stated for ℝ in the form the calculus proofs use them.