Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- Defines the digits 2 to 9 as iterated successors of 1, and defines the value of a decimal numeral such as 156 by Horner's rule in base S(9): a numeral with last digit d denotes the shorter numeral times S(9), plus d.
- From dependent choice: for every family of subsets of a set b indexed by N, each with at least one element, there is a sequence in b whose m-th term lies in the m-th subset.
- If R is a relation on a set b in which every element is related to some element, then from any starting point s in b there is a sequence indexed by N starting at s whose consecutive terms are related by R.
The Principle of Induction for the Natural Numbers Starting at One
theoremthm:induction-natural-numbers-nbg-2026aSet TheoryA class of natural numbers that contains 1 and contains the successor of each of its elements is all of N.Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication
lemmalem:natural-numbers-nbg-2026aSet TheoryThe natural numbers are exactly the successors of elements of omega; 1 is the least natural number and is not the successor of a natural number; the successor is injective; S(n) = n + 1 and n · 1 = n; and N is closed under addition and multiplication.- Defines the set N of natural numbers as omega without 0, and the number 1 as the successor of 0.
Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order
lemmalem:omega-multiplication-nbg-2026aSet TheoryMultiplication on omega satisfies m · 0 = 0 · m = 0, both successor rules and m · 1 = 1 · m = m; it distributes over addition, is associative and commutative, has no zero divisors, and multiplication by a nonzero factor preserves the strict order and can be cancelled.Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order
lemmalem:omega-addition-nbg-2026aSet TheoryAddition on omega satisfies m + 0 = 0 + m = m and both successor rules, is associative, commutative and cancellative, is strictly compatible with the order, m ≤ n exactly when n = m + j for some j, and a sum is zero only when both terms are.- Defines addition on omega by recursion, with m + 0 = m and m + S(n) = S(m + n), and shows that it is a binary operation on omega.
- Given a set a, a starting value c in a and a map g from omega × a to a, there is exactly one map f from omega to a with f(0) = c and f(S(n)) = g(n, f(n)) for every n.
The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor
lemmalem:omega-order-nbg-2026aSet TheoryThe order on omega is a well-order whose strict order is membership; zero is its least element; m < S(n) exactly when m ≤ n, so nothing lies strictly between n and its successor; m < n exactly when S(m) ≤ n; and each n is the set of elements of omega below it.- Defines the order on omega by m ≤ n when m is an element of n or equal to it, and the strict order by m < n when m is an element of n.
Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity
lemmalem:omega-nbg-2026aSet TheoryOmega is a set and the least inductive class; induction from zero holds for every class; the successor never equals zero and is injective; every element of omega is zero or a successor; and elements of omega and their elements are elements of omega and of the element, respectivel…- Defines omega (also written N_0) as the class of sets belonging to every inductive set, and sets 0 to be the empty set.
- Defines a class as inductive when it contains the empty set and contains the successor of each of its elements.
- Defines the successor S(x) of a set x as the union of x with its singleton, the set whose elements are the elements of x together with x itself.
The Equivalence Class of an Element under an Equivalence Relation
definitiondef:equivalence-class-nbg-2026aSet TheoryDefines the equivalence class of an element u of a set a under an equivalence relation R on a as the set of all v in a with u R v, a defined set symbol.A Map Constant on Equivalence Classes Factors Uniquely through the Quotient
lemmalem:quotient-factorization-nbg-2026aSet TheoryIf a map F from a set a to a set b takes equal values on R-related elements, for an equivalence relation R on a, then there is exactly one map G from the quotient a/R to b with G composed with the canonical projection equal to F.Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order
definitiondef:order-bounds-nbg-2026aSet TheoryFor a subset of a partially ordered set, defines upper and lower bounds, boundedness, least and greatest elements, and suprema and infima together with the defined set symbols sup and inf.Images of Sets under Functions Are Sets, and a Function with a Set Domain Is a Set
lemmalem:function-images-sets-nbg-2026aSet TheoryIn NBG, replacement makes the image of a set under a function a set, and a function whose domain is a set is itself a set, being a subclass of the Cartesian product of its domain with its image.