Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Inversions of a Permutation Form a Finite Set, and the Sign Map Exists
lemmalem:sign-permutation-existence-2026aAlgebraCombinatoricsFor a permutation of [n], the pairs i<j whose order it reverses form a finite set, and there is exactly one real-valued map on S_n sending each permutation to -1 raised to the number of these pairs.- For distinct p and q in [n], the transposition of p and q is the permutation of [n] that swaps p and q and fixes every other point.
- The identity is its own inverse; a one-sided inverse of a square matrix is its inverse; inverses of inverses, products and transposes are given by the usual formulas; and Ax = b has the unique solution A^{-1}b.
Criteria for Invertibility of a Square Real Matrix
theoremthm:invertible-matrix-criteria-2026aLinear AlgebraFor a square real matrix A, the following are equivalent: Ax = 0 only for x = 0; x -> Ax is injective; x -> Ax is surjective; A has a right inverse; A has a left inverse; A is invertible.A Homogeneous Linear System with More Unknowns than Equations Has a Nonzero Solution
lemmalem:homogeneous-system-nontrivial-2026aLinear AlgebraIf an m x n real matrix has fewer rows than columns, then Ax = 0 has a solution x different from 0.Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes
lemmalem:matrix-algebra-rules-2026aLinear AlgebraThe matrix product is associative, distributive and compatible with scalars, with identity matrices as neutral elements; the matrix-vector product is linear; the transpose reverses products; Ax.w = x.(A^T w); and |Ax|^2 is at most the sum of the squared entries times |x|^2.The Matrix Product, Matrix-Vector Product, Transpose, Trace, Identity Matrix and Standard Basis Vectors Exist and Are Unique
lemmalem:matrix-operations-existence-2026aLinear AlgebraThe maps giving the matrix product, the matrix-vector product, the transpose and the trace exist and are unique, as do the identity matrix and the standard basis vectors of R^n.The Summation Map on Real-Valued Maps over a Finite Set, and the Dot Product, Euclidean Norm and Euclidean Distance as Maps
lemmalem:euclidean-maps-2026aAnalysisLinear AlgebraSummation over a finite set is a map from the real-valued maps on that set to the reals; consequently the dot product, the Euclidean norm and the Euclidean distance on R^n are maps, each uniquely determined by its values.The Distance on the Real Numbers Is a Map with Values the Absolute Differences
lemmalem:real-line-distance-map-2026aAnalysisThe distance on the real numbers is a map from pairs of reals to reals whose value at (s, t) is |s - t|, and its elements are exactly the pairs ((s, t), |s - t|) with s and t real.Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field
lemmalem:value-formulas-predicative-2026aSet TheoryA condition on the value of a function or of a binary operation inside a predicative formula is expressed by an explicit predicative formula, and so are negatives, sums, products, differences, absolute values, distances, reciprocals and quotients in an ordered field.Iterated Operations and Operations over Finite Sets Take Values in the Underlying Set
lemmalem:finite-operation-closure-2026aSet TheoryAn iterated operation along [n], an iterated operation over a finite set, and in particular a finite sum or product in a commutative ring, lies in the underlying set.Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima
lemmalem:ordered-field-closure-2026aAlgebraNegatives, differences, reciprocals, quotients, absolute values, powers, images of natural numbers, halves and the minimum of two positive elements of an ordered field all lie in the field, with the basic facts about halves and minima.Iterated Operations over Finite Sets Are Given by a Predicative Formula
lemmalem:finite-set-operation-predicative-2026aSet TheoryThe statement that a set is the iterated operation of a map over a finite set is expressed by a predicative formula in the set, the finite set and the map, with the underlying set, the operation, the natural numbers, their order and their addition as class parameters.Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set
lemmalem:iterated-operation-maps-2026aAlgebraThe partial iterates of a sequence, the images of the natural numbers with zero in a commutative ring, the powers of an element, and the iterated operation over a finite set of a map with an extra argument are each the values of exactly one map.Addition and Multiplication of Real Numbers Are Binary Operations: Values and Membership
lemmalem:real-number-operations-2026aAlgebraThe sum and the product of two real numbers are real numbers; addition and multiplication are binary operations on the reals whose values are this sum and product; and ((x, y), z) belongs to either operation exactly when x and y are real and z is their sum, respectively their pro…The Relation, Operations, Order and Embedding Defining the Rational Numbers Exist
lemmalem:rational-number-operations-2026aAlgebraThe relation of equal ratios on pairs of an integer and a natural number exists and is unique; the sum, product, negation and order on the rational numbers are a binary operation, a map and a relation with their defining values; and the embedding of the integers is the unique map…Closed Subsets of Compact Sets Are Compact, and Compact Subsets of a Metric Space Are Closed and Bounded
lemmalem:compact-subsets-2026aTopologyIn a topological space a closed subset of a compact subset is compact; in a metric space every compact subset is closed and bounded.- The dot product of two points of R^n is the sum of the products of their components.
Rules for Pointwise Operations on Real-Valued Maps: a Commutative Ring, Scalar Multiples and Evaluation
lemmalem:pointwise-operations-rules-2026aAnalysisThe real-valued maps on a set form a commutative ring under pointwise operations; scalar multiples obey the usual rules, and evaluation at a point commutes with differences and finite sums.- Defines the pointwise sum, product, scalar multiple, negative and difference of real-valued maps on a set, and the constant maps.