Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Borel Sets of ℝⁿ and of the Real Matrices Are Generated by the Coordinates
lemmalem:borel-euclidean-generators-2026aAnalysisEvery open subset of ℝⁿ is a countable union of open boxes with rational endpoints contained in it, and the Borel σ-algebras of ℝⁿ and of the real p×q matrices are generated by the preimages of Borel subsets of ℝ under the coordinate maps and the entry maps.Measurable Maps: Generators, Composition, Continuous Maps, Restrictions, and Criteria for Real- and [0,∞]-Valued Maps
lemmalem:measurable-maps-2026aAnalysisMeasurability can be tested on a generating family; composites, constant maps, identities, continuous maps between metric spaces and restrictions to measurable sets are measurable; and real- and [0,∞]-valued maps are measurable exactly when their superlevel sets are measurable.Borel Subsets of [0,∞]: Rays, the Point ∞, and Traces on ℝ
lemmalem:borel-extended-nonnegative-2026aAnalysisThe four kinds of rays in [0,∞], the point ∞ and its complement are Borel subsets of [0,∞]; a subset of [0,∞] is Borel exactly when its real part is a Borel subset of ℝ, so every real Borel set of nonnegative numbers is a Borel subset of [0,∞].- Defines the Borel σ-algebra of [0,∞] as the σ-algebra on [0,∞] generated by the rays (a,∞] with a real.
Partial Sums of a Sequence in [0,∞]: First Term, Recursion and Two-Term Sums
helperhlp:extended-partial-sums-2026aThe first partial sum of a sequence in [0,∞] is its first term, each partial sum is the previous one plus the next term, and a sequence vanishing outside its first two terms has sum equal to the sum of those two terms.Total Lengths of Covers by Open Intervals: the Set of Them and the Map of Their Infima
helperhlp:interval-cover-sums-2026aAnalysisFor every subset A of the real line, the total lengths of the covers of A by countably many open intervals form a subset C(A) of [0,∞], and A ↦ inf C(A) is a well-defined map from the power set of ℝ to [0,∞].- The sum of a sequence in [0,∞] given by a typed term is again a typed term, of type [0,∞], under the same guard; and for a map i -> a^(i) from a set D to the sequences in [0,∞], i -> sum of a^(i) is a map from D to [0,∞].
Measure Spaces, Borel Sets and Lebesgue Measure on the Real Line: Standing Notation
settingset:measure-spaces-2026aAnalysisProbabilityStanding notation for measure theory: the extended half-line [0,∞], countable sets and sequences of sets, σ-algebras, Borel sets, measures, null sets, outer measures and Lebesgue measure on the real line, each with its background results by reference.Properties of Lebesgue Outer Measure on the Real Line
lemmalem:lebesgue-outer-measure-2026aAnalysisProbabilityLebesgue outer measure on the real line vanishes on the empty set, is monotone and subadditive for two sets, gives every bounded interval its length, and splits additively along a ray; under dependent choice it is countably subadditive and hence an outer measure.A Closed Interval Covered by Open Intervals Is No Longer than Their Total Length
lemmalem:interval-cover-length-2026aAnalysisProbabilityIf a closed interval [p,q] is covered by finitely many, or by a sequence of, open intervals (a_m,b_m), then q-p is at most the sum of the lengths b_m-a_m, the sum formed in [0,∞].Carathéodory Measurable Sets of an Outer Measure
definitiondef:caratheodory-measurable-2026aAnalysisProbabilityA subset E of X is Carathéodory measurable for an outer measure if it splits every subset of X additively; the measurable sets form a subset of the power set.- Lebesgue measure on the real line is the restriction of Lebesgue outer measure to the Borel sets. That it is a measure is a separate theorem, which assumes the axiom of dependent choice.
Induction for Predicative Formulas, and the Order of ℕ below 1 and below n+1
lemmalem:natural-induction-order-2026aSet TheoryInduction on the natural numbers for any condition expressed by a predicative formula, and two facts on the order of the natural numbers: no natural number lies below 1, and the natural numbers below n+1 are those below n together with n.Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros
lemmalem:extended-nonnegative-facts-2026aAnalysisAn element of [0,∞] that is at most 0 is 0; an element of [0,∞] is below ∞ exactly when it is real; an element below a finite one is finite; and the sum of a sequence of zeros in [0,∞] is 0.Monotone Sequences of Sets, Unions of Traces, and Disjointness of Smaller Sets
lemmalem:set-sequence-facts-2026aAnalysisSet TheoryInclusions between consecutive terms of a sequence of sets extend to all ordered pairs of indices; the union of the traces of a sequence on a set is the trace of its union; an empty intersection is the same as disjointness; and sets contained in pairwise disjoint sets are pairwis…- For a sequence (A_n) of subsets of X, the disjointing sequence B_n = A_n minus the earlier A_k consists of pairwise disjoint subsets B_n of A_n with the same union, every point of A_n lying in some B_m with m at most n; its terms and the auxiliary sets C_n stay in any σ-algebra c…
- For a measurable set Y, the restriction of a measure to the measurable subsets of Y is a measure on Y, and A maps to the measure of A intersected with Y defines a measure on the whole space with total mass the measure of Y; both inherit finiteness or sigma-finiteness as stated.
Uniqueness of Measures Agreeing on a Generating π-System
lemmalem:measure-uniqueness-2026aAnalysisProbabilityTwo measures on a measurable space that agree on a π-system generating the σ-algebra are equal, provided they have the same finite total mass, or the π-system contains a sequence covering the space on whose terms the measures are finite.- A measurable set is null exactly when its measure is zero; subsets and finite unions of null sets are null, and so is a countable union of sets each contained in a member of a given sequence of measurable sets of measure zero. Properties holding almost everywhere are preserved un…
- The integer bracket [s,t] of terms of type N and the rational bracket [s,t] of a term of type Z and a term of type N are terms of type Z and Q under a predicative guard.