Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Pointwise Operations on Real-Valued Maps Exist and Are Unique
lemmalem:pointwise-operations-existence-2026aAnalysisFor a set I, pointwise sum and product, scalar multiplication, negation and constant maps exist uniquely on the set of real-valued maps on I.Iterated Operations Are Given by a Predicative Formula
lemmalem:iterated-operation-predicative-2026aSet TheoryThe statement that a set is the iterated operation of a list a_1, ..., a_n is expressed by a predicative formula in the set, the length and the list, with the underlying set, the operation, the natural numbers, their order and their addition as class parameters.Multiplication on Omega: Products Lie in Omega, Multiplication Is a Binary Operation with Value the Product, and Membership in the Multiplication
lemmalem:omega-multiplication-values-2026aSet TheoryThe product of two elements of omega lies in omega, the multiplication is a binary operation on omega whose value at (m, n) is m·n, and ((m, n), z) belongs to it exactly when m and n lie in omega and z = m·n.Sets of Maps between Finite Sets, Finite Unions of Finite Sets, and Finite Choice
lemmalem:finite-maps-unions-choice-2026aSet TheoryThe set of maps between two finite sets is finite, and nonempty when the target is; a finite union of finite sets is finite; and a finite family of nonempty sets has a choice map, without any axiom of choice.Images of Finite Sets Are Finite, Bounded Sets of Natural Numbers Are Finite, and Nonempty Finite Totally Ordered Sets Have Extreme Elements
lemmalem:finite-images-extremes-naturals-2026aSet TheoryThe image of a finite set under a map is finite; every nonempty finite subset of a totally ordered set has a greatest and a least element; and a set of natural numbers with zero is finite exactly when it is bounded above.Adding an Element to, Subsets of, and Unions and Cartesian Products of Finite Sets Are Finite
lemmalem:finite-subsets-unions-products-2026aSet TheoryA finite set stays finite when one element is added, its subsets are finite, and the union and the Cartesian product of two finite sets are finite.The Pigeonhole Principle, Uniqueness of the Length of a Finite Set, and the Finiteness of the Empty Set and of Singletons
lemmalem:pigeonhole-finite-sets-2026aCombinatoricsSet TheoryAn injection from [m] to [n] forces m ≤ n, so a finite set is listed by exactly one [n]; the empty set and every singleton are finite.Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness
lemmalem:finite-set-induction-2026aSet TheoryThe segments [n] and the property of being finite are expressed by predicative formulas, and a predicative property that holds for the empty set and survives adding one new element holds for every finite set.- Defines the distance on the complex numbers as the modulus of the difference.
- Defines the distance on the real numbers as the absolute value of the difference.
Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces
settingset:metric-spaces-2026cAnalysisTopologyFixes the notation for metric spaces, their balls and their topology, regards the real and complex numbers as metric spaces with the distance |s-t|, and carries the basic facts on limits, continuity and completeness by reference.- The map sending two complex numbers z and w to the modulus |z - w| is a metric on the complex numbers.
- Defines the limit of a convergent sequence in a metric space as the unique point to which it converges.
Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity
lemmalem:relations-maps-predicative-2026aSet TheoryReplacing set variables by variables of either kind keeps a formula predicative and means what it should when the replacements are sets. Equality with, and membership of, ordered pairs and the properties of being a relation, a function, a map, injective, surjective and bijective…Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols
lemmalem:defined-set-symbols-predicative-2026aSet TheoryAn expression written with abbreviations and quantifying over sets only is predicative; a set described uniquely under a guard can be eliminated existentially or universally; and the empty set, pairs, ordered pairs, unions, power sets, class terms, function values and values of b…The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers
settingset:complex-numbers-nbg-2026cAnalysisAlgebraStanding notation for the complex numbers: the field C of pairs of reals with its imaginary unit i, the real numbers (and through them the naturals, integers and rationals) identified with their images under a |-> (a,0), and the canonical form a + bi with i^2 = -1.Uniqueness of the Complex Numbers: Every Field Generated over an Embedded Copy of the Reals by a Square Root of -1 Is Uniquely Isomorphic to C
theoremthm:complex-numbers-unique-nbg-2026bAlgebraIf a field K contains an injective homomorphic copy of the reals and an element u with u squared equal to -1 such that every element of K has the form a+bu with a, b in that copy, then exactly one map from C to K preserves sums and products, extends the embedding and sends i to u…Conjugation and Modulus of Complex Numbers: Field Automorphism, Real and Imaginary Parts, Multiplicativity, Inverses, Component Bounds, Triangle Inequalities and Finite Sums
lemmalem:complex-conjugate-modulus-nbg-2026bAnalysisAlgebraComplex conjugation is an involutive field automorphism of C fixing exactly the reals; real and imaginary parts are additive and real-homogeneous; the modulus is nonnegative, definite, multiplicative, bounded by and bounding the components, satisfies the triangle and reverse tria…- The modulus of z is the square root of (Re z)^2 + (Im z)^2; for a real number it is its absolute value, so the notation |x| is unambiguous.
- The complex conjugate of z is Re z - (Im z) i.