Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Restricting a Continuous Map to a Smaller Subset Preserves Continuity
lemmalem:continuous-restriction-metric-2026aAnalysisIf a map on a subset A of a metric space is continuous at a point, or on A, then its restriction to a smaller subset B is continuous at that point relative to B, or on B.- Defines an interval of the real line as a subset containing every number between two of its points, and fixes the notation for bounded intervals and rays.
Locality of Predicative Formulas: Truth Depends Only on the Values of the Free Variables
helperhlp:predicative-formula-locality-2026aSet TheoryUnder any assignment of sets to set variables, with its class parameters fixed, a predicative formula has a truth value that depends only on the sets assigned to its free set variables.Splitting an Operation over the Segment [m+n] into [m] and a Shifted Copy of [n]
lemmalem:segment-operation-splitting-2026aAnalysisFor an associative and commutative operation and a map a on [m+n], the operation over [m+n] equals the operation over [m] combined with the operation over [n] of j to a(m+j); the same holds for the operations from 1 in either reading.- The two projections of a Cartesian product, the evaluation map of a set of maps, and the curried form of a map on a product exist as maps and are unique.
The Operator-Norm Distance between Real Matrices Is a Map
lemmalem:matrix-distance-map-2026aLinear AlgebraFor m, n in N there is exactly one map from pairs of real m x n matrices to the reals whose value at (A, B) is the operator norm of A - B.Existence and Uniqueness of the Block Matrix with Two Row Blocks and Two Column Blocks
lemmalem:block-matrix-existence-2026aLinear AlgebraGiven real matrices A, B, C and D of sizes m x m, m x n, n x m and n x n, there is exactly one real (m+n) x (m+n) matrix whose four blocks of entries are those of A, B, C and D.Absolute Value and Squaring as Maps on the Reals, and Entrywise Absolute Values and Squares of a Real Matrix
helperhlp:real-function-maps-2026aLinear AlgebraThe absolute value and the square are maps from R to R. Composing a real m x n matrix with them gives the real m x n matrices |A| and A^{o2} of entrywise absolute values and entrywise squares, each unique.The Invertible Matrices and the Positive Semidefinite Matrices Form Sets
helperhlp:matrix-condition-sets-2026aLinear AlgebraFor n in N, the invertible real n x n matrices form a subset GL_n(R) of the square matrices, and the positive semidefinite symmetric n x n matrices form a subset S_+(n) of S(n), each with the evident membership. Both conditions are expressed by predicative formulas, so set-builde…Images of Typed Terms: the Set of Values Is a Set, Finite when Is Finite, and a Typed Term
helperhlp:image-typed-terms-2026aSet TheoryFor a term t of type B under a guard extended by u in D, the class of the values of t at the elements u of the set D is a set contained in B, with the expected elements. It is itself a typed term under the original guard, so equating a set variable with it is expressed by a predi…The Open Sets of a Metric Space Form a Set, Given by a Predicative Formula
helperhlp:metric-topology-set-2026aTopologySet TheoryBeing an open subset of a metric space is expressed by a predicative formula, so the open subsets form a set, the metric topology, whose elements are exactly the open subsets.One Threshold for Finitely Many Monotone Conditions and for Tails
helperhlp:common-threshold-2026aAnalysisSet TheoryIf a monotone condition P(p, N), expressed by a predicative formula, has a threshold N for each p in a finite set I, then one N serves for every p in I; in particular finitely many tail conditions have a common threshold.The Sequences k ↦ of a Sequence in ℝ^I, and the Map of Their Limits
helperhlp:sections-limit-maps-2026aAnalysisTopologyFor a sequence of real-valued maps on a set I, each evaluation at a point of I is a real sequence, and if all these sections converge there is exactly one map in ℝ^I to which they converge pointwise, in either framework of convergence.Limits of Matrix Operations, and the Closed Complete Sets of Symmetric and of Positive Semidefinite Matrices
lemmalem:matrix-limits-closed-sets-2026aAnalysisLinear AlgebraIn the operator-norm distance, sums, scalar multiples, products, matrix-vector products and transposes of convergent sequences of real matrices converge to the corresponding operation on the limits. The symmetric matrices and the positive semidefinite matrices form closed subsets…Splitting the Segment [m+n] into [m] and a Shifted Copy of [n]
lemmalem:segment-split-2026aSet TheoryFor natural numbers m and n, the segment [m+n] contains [m], and j maps to m+j bijectively from [n] onto the rest of [m+n]; so each k in [m+n] lies either in [m] or is m+j for exactly one j in [n], namely j = k - m.Subsets of a Metric Space: the Restricted Metric, Sequences, Limits in Closed Subsets and Completeness of Closed Subsets
lemmalem:metric-subspace-closed-complete-2026aAnalysisTopologyThe restriction of a metric to a subset is a metric, and a sequence in the subset converges to a point of it, or is Cauchy, in the subset exactly when it does so in the whole space. A limit of a sequence in a closed subset lies in the subset, so a closed subset of a complete metr…Standard Basis Vectors of ℝ^q: Coordinates, Orthonormality and Unit Length
lemmalem:standard-basis-vectors-rn-2026aLinear AlgebraThe dot product of the k-th standard basis vector of R^q with a point w is the k-th coordinate of w; consequently the standard basis vectors are orthonormal and each has Euclidean norm 1.The Operator Norm of a Symmetric Matrix: Quadratic Forms, Eigenvalues and the Semidefinite Ordering
lemmalem:operator-norm-symmetric-matrix-2026aLinear AlgebraFor a symmetric real matrix the operator norm is the supremum of the absolute quadratic form over the unit ball and the largest absolute eigenvalue of an orthogonal diagonalization; it is the least nonnegative lambda with -lambda I below A below lambda I, it squares under squarin…The Operator Norm of Entries, Transposes, Multiples of the Identity, Orthogonal Factors and Diagonal Matrices
lemmalem:operator-norm-special-matrices-2026aLinear AlgebraEntries of a real matrix are recovered from standard basis vectors and are bounded by the operator norm, which is in turn bounded by the root of the sum of squared entries and by the sum of absolute entries; the norm is unchanged by transposition and by orthogonal factors, equals…Rules for the Operator Norm: Bound, Least Constant, Definiteness, Homogeneity, Triangle Inequality and Products
lemmalem:operator-norm-rules-real-matrix-2026aLinear AlgebraThe operator norm of a real matrix is nonnegative, bounds the length of Ax by its multiple of the length of x, is the least such constant, vanishes exactly at the zero matrix, is absolutely homogeneous, satisfies the triangle inequality and is submultiplicative.