Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Maps Used to Build the Integral: Fibres of a Map, Pointwise Combinations with Finite Image, Tail Extrema of a Sequence of Maps, the Integer Part, and Indicators
helperhlp:integral-construction-terms-2026aAnalysisStates that the fibre map of a map, pointwise combinations of maps with finite image, the tail infima and suprema of a sequence of extended-real-valued maps with their limits inferior and superior, the integer part composed with a real-valued map, and the indicator map exist as m…Finite Sums: Vanishing Terms, Finite Additivity of Measures, and Finite Sums of Series in [0,∞]
lemmalem:finite-sums-measures-series-2026aAnalysisTerms equal to the neutral element may be dropped from a sum over a finite set, a measure is additive over a pairwise disjoint family indexed by a finite set, and a finite sum of series in [0,∞] is the series of the finite sums.The Integer Part as the Greatest Integer Below, the Integer Part of a Double, and Powers of Two
lemmalem:integer-part-properties-2026aAlgebraAn integer lies below a real number exactly when it lies below its integer part; the integer part of a double lies between twice the integer part and that plus one; and every natural number m satisfies m < 2^m and 0 < 2^{-m} < 1/m.Greatest Elements as Suprema, Suprema and Infima of Nested Sets in [−∞,∞], and a Scaling Criterion for Order in [0,∞]
lemmalem:extended-real-suprema-comparison-2026aAnalysisA greatest element of a subset of a partially ordered set is its supremum; suprema and infima in the extended real line are monotone under inclusion; and an element of [0,∞] whose products with all reals strictly between 0 and 1 lie below a bound lies below it itself.Tail Extrema, Limit Inferior and Limit Superior of a Sequence in [−∞,∞]
definitiondef:extended-limit-inferior-2026aAnalysisDefines the tail infima and tail suprema of a sequence in the extended real line, and its limit inferior and limit superior as the supremum of the tail infima and the infimum of the tail suprema.Basic Properties of the Integral of Nonnegative Measurable Maps
lemmalem:lebesgue-integral-nonnegative-basic-2026aAnalysisProbabilityThe integral of a nonnegative measurable map agrees with the simple integral on nonnegative simple functions, gives the measure on indicators, is monotone and positively homogeneous, and vanishes on the zero map.Properties of Simple Functions and of the Simple Integral
lemmalem:simple-function-integral-2026aAnalysisProbabilityIndicators of measurable sets are simple with simple integral the measure of the set; simple functions are closed under sums, products, multiples, maxima and minima; and the simple integral is computed by any disjoint representation, is additive, positively homogeneous and monoto…- The indicator function of a subset A of a set X is the real-valued map on X equal to 1 on A and 0 off A.
Lebesgue Outer Measure: Bounds from Covers by Open Intervals
helperhlp:lebesgue-outer-cover-bounds-2026aThe Lebesgue outer measure of a subset of the real line lies in [0,∞], is at most the total length of each of its covers by open intervals, is at least every common lower bound of these total lengths, and is approximated from above by them.Countability as a Predicative Condition, and Finite Powers of a Set as a Typed Term
helperhlp:countable-predicative-2026aSet TheoryThe condition that a set is countable is given by a predicative formula, also when applied to a typed term; and for a set S, the set of maps from [n] to S is a typed term in a variable n with values in the natural numbers.Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms
helperhlp:measurable-set-terms-2026aSet TheoryPreimages of a set under a map, unions and intersections of a family of sets over a fixed index set, suprema and infima in the extended real line, and the sets where an extended-real-valued map lies above or below a level are typed terms when their arguments are, so equating a se…- For a countable set S and a natural number k, the set of k-tuples in S, the maps from [k] to S, is countable.
- The preimage under a map commutes with unions and with intersections over a nonempty index set, takes the complement of a set to the complement of its preimage, and takes the whole target set to the whole domain.
The Borel σ-Algebra of the Real Line Is Generated by the Closed Rays, and by the Open Left Rays
lemmalem:borel-real-ray-generators-2026aAnalysisThe Borel sigma-algebra of the real line is generated by the closed right rays [a,∞), and also by the open left rays (−∞,a), a real.The Families of Rays of the Real Line Are Sets of Subsets of the Real Line
helperhlp:real-ray-families-2026aAnalysisFor each of the four kinds of rays of the real line, the rays of that kind with real endpoint form a set, a subset of the power set of the real line, whose members are exactly those rays.Preimages under a Map: Membership, the Preimage Map, Sequences of Preimages, and the Set of Sets with Preimage in a Given Set
helperhlp:preimage-sets-2026aAnalysisMembership in a preimage u^{-1}(V) means lying in S with value in V; V -> u^{-1}(V) is a map from P(T) to P(S), and so k -> u^{-1}(V_k) is a sequence for a sequence (V_k); and the sets B with u^{-1}(B) in a given set form a set.Sums, Products, Transposes, Dot Products and Norms of Measurable Vector- and Matrix-Valued Maps
lemmalem:measurable-vector-matrix-operations-2026aAnalysisSums, scalar multiples and dot products of measurable vector-valued maps, sums, scalar multiples, products, transposes and matrix-vector products of measurable matrix-valued maps, and the Euclidean and operator norms of such maps are measurable.Vector- and Matrix-Valued Measurable Maps: Components, Entries and Continuous Images
lemmalem:measurable-components-2026aAnalysisA map into Euclidean space or into real matrices is measurable exactly when its component or entry maps are, and a continuous function of finitely many measurable real-valued maps is measurable.Suprema, Pointwise Limits and the Convergence Set of Measurable Real-Valued Maps
lemmalem:measurable-real-limits-2026aAnalysisProbabilityThe supremum and infimum of a pointwise bounded sequence of measurable real-valued maps, and the pointwise limit of a pointwise convergent one, are measurable, and the set where such a sequence converges is measurable.Unions and Intersections over a Countable Index Set in a σ-Algebra
lemmalem:sigma-algebra-countable-operations-2026aAnalysisA σ-algebra contains the union, and for a nonempty index set the intersection, of any family of its members indexed by a countable set.