Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- The operator norm of a real m x n matrix A is the supremum of the lengths of Ax over the closed unit ball of R^n, the value at A of the supremum map on m x n matrices.
Perturbations of an Invertible Matrix: the Invertible Matrices Form an Open Set and Inversion Is Continuous
lemmalem:matrix-inverse-continuous-2026aAnalysisLinear AlgebraA square matrix B closer to an invertible matrix A than 1/||A^{-1}|| in operator-norm distance is invertible, with an explicit bound on the distance between the inverses. Hence the invertible matrices form an open set and inversion is continuous.The Set of Lengths ‖Ax‖ over the Unit Ball Has a Supremum, and the Supremum Map Exists
lemmalem:operator-norm-existence-real-matrix-2026aLinear AlgebraFor a real m x n matrix A, the lengths of Ax over the closed unit ball of R^n form a nonempty set of reals bounded by the square root of the sum of the squared entries, so it has a supremum, and A maps to that supremum by a map on all m x n matrices.The Real Matrices with the Operator-Norm Distance Form a Complete Metric Space with Entrywise Convergence
theoremthm:real-matrices-complete-metric-space-2026aAnalysisLinear AlgebraFor all sizes, the operator-norm distance is a complete metric on the real matrices, bounding the differences of entries, of norms and of matrix-vector products, and convergence and the Cauchy property in it are entrywise.- The distance between two real m x n matrices is the operator norm of their difference; for square matrices of order n it is written d_n.
- The factorials of the natural numbers with zero are the values of exactly one map F from the natural numbers with zero to themselves, and F satisfies the factorial recursion. The recursion is stated so that inductions involving n! can run over a predicative formula with F as a pa…
Powers and Images of Natural Numbers in a Commutative Ring Lie in the Ring
lemmalem:ring-power-image-closure-2026aSet TheoryIn a commutative ring R, every power x^n of an element x of R with exponent in the natural numbers with zero, and the image n_R of every natural number with zero, lies in R.Permutations of [n] are Maps [n] → [n], and Values of the Determinant are Real Numbers
helperhlp:permutation-maps-determinant-values-2026aStates that every σ ∈ S_n is a map [n]→[n] and that det A ∈ ℝ for every real n×n matrix A.- For a map F: A → B between classes, the first component of a pair in F lies in A, and the restriction of F to a subclass C of A is a map C → B with the same values on C.
The Segments [n]: Each Is a Set, and 1 Lies in [n] for n ∈ ℕ
helperhlp:natural-number-segments-2026aSet TheoryFor every natural number with zero n, the segment [n] is a set contained in the natural numbers with zero, and for every natural number n it contains 1.- For elements x, y and z of a commutative ring, the closure of sums and products, the associative and commutative laws of addition and multiplication, the neutral laws of 0 and 1 on both sides, and the distributive laws on both sides.
- The real numbers form a field and an ordered ring, their order is a partial order, multiplication is associative and commutative, 0 is a neutral element of addition, x < y implies x ≤ y, (x − y) + y = x and x^2 = x · x.
Conditions Expressed by a Predicative Formula, and Guards
definitiondef:predicative-condition-guard-2026bSet TheoryWith parameters of fixed values, a condition on finitely many set variables is expressed by a predicative formula if some predicative formula holds exactly when the condition does; a guard is a predicative formula in the given variables and parameters.- A metatheoretic definition: a term under a guard gives, for every assignment of sets to the variables x_1, ..., x_k satisfying the guard, a class depending only on those sets, and it has type A if this value is always a set in A and its equation with a further set variable, conjo…
Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them
helperhlp:typed-terms-predicative-2026bSet TheoryTerms built from variables, set parameters, values of maps and ordered pairs, each lying in a stated class whenever a predicative guard holds, can be equated with a set variable by a predicative formula under the guard. Hence equations and memberships between such terms under the…The Positive Semidefinite Square Root of a Positive Semidefinite Matrix
definitiondef:psd-square-root-real-matrix-2026aLinear AlgebraThe square root of a positive semidefinite real symmetric matrix A is the unique positive semidefinite symmetric matrix whose square is A.Every Positive Semidefinite Matrix Has Exactly One Positive Semidefinite Square Root
lemmalem:psd-square-root-existence-2026aLinear AlgebraA positive semidefinite real symmetric matrix A has exactly one positive semidefinite symmetric B with BB = A; it is obtained from any orthogonal diagonalisation of A by taking square roots of the diagonal, it commutes with A, and it is positive definite when A is.Positive Semidefinite and Positive Definite Matrices by Their Eigenvalues
lemmalem:psd-eigenvalue-criteria-2026aLinear AlgebraA real symmetric matrix is positive semidefinite exactly when its eigenvalues are nonnegative, and positive definite exactly when they are positive, or equivalently when it is positive semidefinite and invertible; a positive definite matrix has a quadratic form bounded below by a…The Spectral Theorem for Real Symmetric Matrices
theoremthm:spectral-theorem-real-symmetric-2026aLinear AlgebraEvery real symmetric matrix is Q diag(lambda) Q^T for an orthogonal Q and a nonincreasing lambda; in any such factorisation the columns of Q are eigenvectors with the eigenvalues lambda_k, these are all the eigenvalues, and the quadratic form lies between lambda_n |x|^2 and lambd…Eigenvalues: the Determinant Criterion, Diagonal Matrices, Orthogonal Similarity and Orthogonality of Eigenvectors of Symmetric Matrices
lemmalem:eigenvalue-criteria-real-matrix-2026aLinear AlgebraA real number is an eigenvalue of a square real matrix A exactly when A minus it times the identity is singular, equivalently has determinant zero; diagonal matrices obey the expected algebra and have exactly their diagonal entries as eigenvalues; conjugating by an orthogonal mat…