Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Continuous Functions with Compact Support: the Zero Function, Closure under Operations, Vanishing off the Support, Existence of the Maximum Modulus, and Uniform Continuity
lemmalem:compact-support-continuous-operations-2026aAnalysisTopologySums, scalar multiples, products, absolute values, maxima and minima of continuous compactly supported real functions on a metric space are again continuous with compact support; such a function vanishes off its support, and the set of its absolute values together with 0 has a gr…- The support of a real function on a metric space is the closure of the set where it is nonzero; the function has compact support when this closure is compact.
- A metric space is locally compact if every point is the centre of a compact closed ball of positive radius.
Locally Compact Metric Spaces and Compactly Supported Functions: Standing Notation
settingset:locally-compact-notation-2026aAnalysisTopologyStanding notation for real functions on a metric space: closures, interiors and distances to subsets, compact subsets, pointwise operations including absolute value, maximum and minimum, sequences of functions, and background on normed spaces.- For a doubly indexed array of real numbers each of whose columns is a bounded sequence, one strictly increasing sequence of row indices makes every column converge.
The Dual of a Real Normed Space Is a Real Banach Space; Weak-Star Limits
lemmalem:dual-space-banach-2026aAnalysisThe bounded linear functionals on a real normed space form a real vector space under pointwise operations, the dual norm is a norm on it, and the resulting normed space is complete. Weak-star limits are unique, and convergence in the dual norm implies weak-star convergence.Weak-Star Convergence in the Dual of a Real Normed Space
definitiondef:weak-star-convergence-2026aAnalysisA sequence of bounded linear functionals on a real normed space converges weak-star to a bounded linear functional F if its values at every point converge to the value of F there.- A map from the natural numbers stays a map when its codomain is enlarged, two sequences in a set with the same terms are equal, and the range of a map from the natural numbers consists of its terms.
Sums of Series: a Convergent Series Has a Real Sum, and a Bound on All Partial Sums Bounds the Sum in [0,∞]
helperhlp:series-sum-bookkeeping-2026aThe sum of a convergent real series is a real number, and the sum of a sequence in [0,∞] is at most every element of the extended real line that bounds all of its partial sums.Nonnegative Measurable Maps and Null Sets: Constant Maps, the Pointwise-Sum Operation on 𝓜⁺, and Complements of Measure-Zero Sets
helperhlp:nonnegative-maps-null-sets-2026aAnalysisProbabilityConstant maps into [0,∞] are measurable, the pointwise sum is an associative and commutative binary operation on 𝓜⁺ with the zero map as neutral element, and the complement of a measure-zero set holds almost everywhere.A Term of One Type Whose Values Lie in a Class B Is a Term of Type B
helperhlp:typed-term-retyping-2026aSet TheoryA term of type A under a guard whose values, under every assignment satisfying the guard, lie in a class B is also a term of type B under that guard.The Graph Reading of a Formula Tree Is Predicative and Agrees with Its Reading, So the Reading Is Predicative
helperhlp:formula-syntax-predicative-2026bThe graph reading of a well-scoped formula tree is predicative; it agrees with the reading wherever every value is used properly; so a reading whose values are always used properly is predicative.Formula Trees with Values: Syntax, Two Readings, and Definedness
definitiondef:formula-syntax-predicative-2026bFormula trees whose atoms may name values F(x), x*y or a uniquely described set, with their reading (defined where every value is used properly) and their graph reading, in which each value is replaced by its graph.- For a point of Euclidean space, its restriction to [N] is a point of ℝ^N with the same coordinates, and the finite sum of its coordinates obeys the first and successor steps of the recursion, is a real number, commutes with scalar multiples, and dominates each coordinate when all…
The Norm Distance from the Origin Is the Norm
lemmalem:norm-distance-from-origin-2026aAnalysisLinear AlgebraIn a real normed space, the norm-metric distance from the zero vector to a vector y equals the norm of y.Completeness of ℝ, Infimum Form: A Nonempty Subset of ℝ Bounded Below Has an Infimum
lemmalem:reals-infimum-exists-2026aAnalysisSet TheoryEvery subclass of the real numbers that has an element and is bounded below has an infimum in the real numbers, and that infimum is a set.The Norm of a Negative, and the Norm Distance of a Translate
lemmalem:norm-negative-translate-2026aAnalysisA norm takes the same value at a vector and at its negative, and the norm metric distance from a translate a+w to a is the norm of w.Linear Functionals Respect Differences, and Coefficients Along a Nonzero Vector Are Unique
lemmalem:linear-functional-difference-line-2026aAnalysisA linear functional on a subspace maps differences to differences, and the scalar multiplying a nonzero vector is determined by the product.Rearranging Sums, Differences and Two-Term Combinations in a Real Vector Space
lemmalem:vector-space-rearrangements-2026aAnalysisExchanging middle terms of a double sum, translation invariance and splitting of differences, cancellation, and the rules for two-term linear combinations in a real vector space.- The triangle inequality of a real norm holds for the corresponding elements of the type Real, with the sum and order of Real.