Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Finite Linear Combinations of Continuous Real-Valued Maps on a Metric Space are Continuous
lemmalem:finite-sum-continuous-metric-2026aAnalysisTopologyA finite linear combination, over a nonempty finite index set, of continuous real-valued maps on a metric space is continuous.Weak Convergence of Finite Borel Measures is Preserved by Continuous Maps between Metric Spaces
lemmalem:weak-convergence-continuous-image-metric-2026aTopologyProbabilityPush-forward by a continuous map between metric spaces preserves weak convergence of finite Borel measures.Prokhorov's Theorem on a Metric Space: a Tight Sequence of Borel Probability Measures Has a Weakly Convergent Subsequence
theoremthm:prokhorov-tight-sequence-metric-2026aTopologyProbabilityA tight sequence of Borel probability measures on a metric space has a weakly convergent subsequence (direct half of Prokhorov's theorem).Ulam's Theorem: a Finite Borel Measure on a Complete Separable Metric Space is Tight
theoremthm:ulam-tightness-metric-2026aTopologyProbabilityEvery finite Borel measure on a complete separable metric space is tight (Ulam).A Closed Totally Bounded Subset of a Complete Metric Space is Compact
lemmalem:complete-totally-bounded-compact-metric-2026aAnalysisTopologyA closed, totally bounded subset of a complete metric space is sequentially compact and compact.Limits of a Uniformly Bounded Sequence of Real Functions with a Common Modulus of Continuity: Bounds, Extraction and Uniform Convergence on Sequentially Compact Sets
lemmalem:equicontinuous-sequence-limits-metric-2026aAnalysisTopologyFor a uniformly bounded sequence of real functions on a metric space sharing a modulus of continuity, the pointwise limit superior and inferior keep the bound and the modulus and are attained along subsequences at each point; where they agree on a sequentially compact set, the co…A Smooth Variational Principle of Borwein-Preiss Type with a Gauge on a Complete Metric Space
theoremthm:borwein-preiss-gauge-metric-2026aAnalysisTopologyAn upper semicontinuous function bounded above on a complete metric space, perturbed by a summable series of gauge terms centred at a convergent sequence of points, attains a strict maximum at a point whose value is at least that of any prescribed starting point.The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It
theoremthm:metric-completion-2026aAnalysisTopologyThe metric completion is a complete metric space into which the canonical map is an isometry with dense image; a map into a complete metric space that preserves Cauchy sequences extends uniquely, continuously and with the same Lipschitz constant.- The metric completion is the set of classes of Cauchy sequences under vanishing limit distance, with the limit distance, and the canonical map sends a point to the class of its constant sequence.
Cauchy Sequences in a Metric Space: Constant Sequences, Convergence of Termwise Distances, the Null Relation, and Independence of Representatives
lemmalem:cauchy-sequences-metric-2026aAnalysisTopologyFor Cauchy sequences in a metric space the termwise distances converge; the limit distance is a pseudometric, and vanishing limit distance is an equivalence relation compatible with it.Sequential Weak-Star Compactness of the Noncommutative Laws with a Given Norm Bound
theoremthm:nc-laws-sequential-compactness-2026aTopologyProbabilityWeak-star convergence of laws is tested on monomials and has unique limits; the laws with a given norm bound are closed and sequentially compact.Weak-Star Convergence of Noncommutative Laws
definitiondef:weak-star-convergence-nc-laws-2026aTopologyProbabilityDefines weak-star convergence of a sequence of noncommutative laws as convergence of the values on every polynomial.The Radial Compactification of Euclidean Space: Norm Continuity, a Homeomorphism onto the Open Unit Ball, Radial Cutoffs, and Extension of Test Functions
lemmalem:radial-compactification-euclidean-2026aAnalysisTopologyThe map sending x to x divided by one plus its norm is a homeomorphism of Euclidean space onto the open unit ball; compact sets are carried into balls of radius less than one, radial cutoffs are available there, and multiplying a continuous function by such a cutoff produces a co…The Metric Subspace: Continuity, the Borel Sigma-Algebra, and the Restriction of a Borel Measure
lemmalem:borel-subspace-metric-2026aAnalysisTopologyThe Borel sets of a metric subspace are the traces of the ambient Borel sets; when the subspace is itself Borel they are the ambient Borel sets it contains, the restriction of a Borel measure is a Borel measure on it, and an integral of a function vanishing off the subspace is co…Compact Subsets of a Metric Space are Closed and Borel
lemmalem:compact-subset-closed-borel-metric-2026aAnalysisTopologyA compact subset of a metric space is closed, and therefore belongs to the Borel sigma-algebra, as does its complement.A Uniformly Continuous Map Between Metric Spaces Is Continuous
lemmalem:uniformly-continuous-implies-continuous-2026aAnalysisTopologyA map that is uniformly continuous on a subset of a metric space is continuous at every point of that subset.Extension of a Uniformly Continuous Real Function from a Dense Subset
lemmalem:uniformly-continuous-dense-extension-2026aAnalysisTopologyA uniformly continuous real function on a dense subset of a metric space extends to a uniformly continuous function on the whole space; the extension is unique among continuous functions, and it inherits any modulus and any bound of the original function.The Semicontinuous Envelopes of a Pointwise Maximum and of a Pointwise Minimum
lemmalem:envelope-maximum-metric-2026aAnalysisTopologyThe upper semicontinuous envelope of a pointwise maximum of two functions is the pointwise maximum of their upper envelopes, and dually for minima and lower envelopes.Local Bounds, Semicontinuous Envelopes and Local Extrema Are Unchanged on the Trace of an Open Set
lemmalem:envelopes-open-trace-metric-2026aAnalysisTopologyFor an open set meeting a set in a metric space, restriction to preserves local boundedness, gives the same semicontinuous envelopes at points of , and has the same local maxima and minima there.Semicontinuity and the Semicontinuous Envelopes are Local Notions
lemmalem:semicontinuity-envelope-localisation-2026aAnalysisTopologyWhether a function is semicontinuous at a point, and the values of its semicontinuous envelopes near that point, depend only on the restriction of the function to a closed ball around it.