Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Intervals of the Real Line as Defined Set Symbols, Typed Terms and Values of Maps
helperhlp:interval-terms-2026aAn interval or ray I(a,b) of the real line is a defined set symbol used properly at real endpoints, I(s,t) is a term of type P(R) for real-valued terms s and t, and i -> I(s_i,t_i) is a map for real-valued maps s and t.- Sums of terms of type N_0 (or N) and differences s - t with t <= s of terms of type N_0 are again terms of type N_0 (or N) under a predicative guard.
Sequences and Maps of Sets: Complements, Traces, Two-Term Sequences, the Disjointing Sequence, and Sequences in a Subset
helperhlp:set-sequences-2026aFrom a sequence of subsets of a set X one forms the sequence of complements and the recursively defined sequences of remainders and disjointed pieces; intersecting with a fixed set gives a map and sequences of traces, and two subsets of X form a sequence with union their union.Predicative Formulas for σ-Algebras, π-Systems and λ-Systems, and the Sets of Them Containing a Given Family
helperhlp:set-system-predicates-2026aBeing a σ-algebra, a π-system or a λ-system on a set X is expressed by a predicative formula, so the σ-algebras, π-systems and λ-systems on X containing a given family of subsets of X each form a set, a subset of the power set of the power set of X.Partial Iterates of a Two-Variable Map, Row by Row and Column by Column
helperhlp:partial-iterate-two-variable-maps-2026aSet TheoryFor a map of two variables into a set with a binary operation, the partial iterates along the natural-number variable, taken row by row or column by column, are the values of exactly one map of two variables, and swapping the two arguments of a map gives exactly one map.Countable Sets: a Bijection from ℕ onto ℕ×ℕ, Finite Sets, Subsets, Surjective Images, Images, Products, and the Integers and Rationals
lemmalem:countable-sets-2026aSet TheoryThe natural numbers, finite sets, subsets and images of countable sets, products of two countable sets, the integers, the rationals and pairs of rationals are countable, and there is a bijection from the natural numbers onto the pairs of natural numbers.- A set is countable if it is empty or there is a surjective map from the natural numbers onto it.
Borel Sets of a Metric Space: Open and Closed Sets, Points, Open Sets of Subspaces, and Subspaces
lemmalem:borel-sets-metric-2026aAnalysisOpen sets, closed sets, points and closed balls of a metric space are Borel; the open sets of a subspace are the traces of open sets of the space; traces of Borel sets on a subspace are Borel in it and generate its Borel sets, and for a Borel subspace these are exactly the Borel…- A λ-system on a set X is a set of subsets of X that contains X, the complement in X of each of its members, and the union of every sequence of pairwise disjoint members.
- A π-system on a set X is a set of subsets of X that contains the intersection of any two of its members.
No Set Is an Element of Itself, Nor Is Its Singleton, and No Set Equals Its Singleton
lemmalem:no-small-membership-cycles-2026aAnalysisFrom the axiom of foundation: no set is an element of itself, the singleton of a set is not an element of it, and no set equals its own singleton.- In [0,∞], suprema commute with adding or multiplying by a constant and with sums of nondecreasing sequences; finite sums are monotone, homogeneous, and commute with suprema of nondecreasing families.
- Defines the sum and the product on [0,∞]: real operations on real arguments, ∞ otherwise, with the convention 0·∞ = ∞·0 = 0.
Sums of Sequences in [0,∞]: Real Series, Linearity, Comparison, Rearrangement, Double Series and Monotone Convergence
lemmalem:extended-nonnegative-series-2026bAnalysisThe sum of a sequence in [0,∞] bounds its finite partial sums and is their least upper bound, agrees with the sum of a convergent real series and is ∞ otherwise, and is additive, positively homogeneous, monotone, invariant under rearrangement, independent of the order of summatio…- The sum of a sequence in [0,∞] is the supremum of its partial sums, formed with the sum of [0,∞]; it always exists in [0,∞].
Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation
lemmalem:extended-nonnegative-arithmetic-2026bAnalysisThe sum and the product on [0,∞] are commutative monoids linked by distributivity; both are monotone, a sum dominates each summand, and real summands cancel.- The order of the extended real line is total, extends that of ℝ and has −∞ as least and ∞ as greatest element; every subset has a supremum and an infimum, computed in ℝ when the set is real and bounded, and suprema can be approximated from below by elements of the set.
- The extended real line adjoins two points, ∞ and −∞, to ℝ, ordered so that −∞ lies below and ∞ above every real number; [0,∞] consists of the nonnegative reals and ∞.
Powers with a Variable Base: a Predicative Formula and the Map (x, m) ↦
helperhlp:power-maps-predicative-2026aAlgebraSet TheoryFor a binary operation with a neutral element, the relation z = x^m between a base, an exponent in the natural numbers with zero and the power is expressed by a predicative formula, and (x, m) ↦ x^m is a map.Vector- and Matrix-Valued Functions on a Compact Interval: Standing Conventions
settingset:matrix-functions-2026aAnalysisLinear AlgebraStanding conventions for functions on a compact interval with values in ℝⁿ or in real matrices: the word "function", the metrics behind continuity, and derivatives and integrals, with the computational toolkit as background.