Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- 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.The Quotient of a Set by an Equivalence Relation and the Canonical Projection
definitiondef:quotient-set-nbg-2026aSet TheoryDefines the quotient a/R of a set a by an equivalence relation R as the class of its equivalence classes, and the canonical projection sending each element to its class.Reflexive, Symmetric, Antisymmetric and Transitive Relations on a Set
definitiondef:relation-properties-nbg-2026aSet TheoryDefines when a relation on a set is reflexive, symmetric, antisymmetric or transitive.- A class X is a subclass of a class Y, written X ⊆ Y, if every element of X is an element of Y; a subclass that is a set is a subset.
The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set
lemmalem:function-set-nbg-2026aSet TheoryFor sets x and y, a class belongs to y^x exactly when it is a function from x to y, and y^x is a set, being a subclass of the power set of x×y.Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction
lemmalem:function-basic-nbg-2026aSet TheoryCollects the basic algebra of functions between classes: equality by values, composition, identities and their neutrality, the inverse of an injective function and of a bijection, a two-sided-inverse criterion for bijectivity, preservation of injectivity and surjectivity, and res…Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set
lemmalem:cartesian-product-set-nbg-2026aSet TheoryAn ordered pair (u,v) lies in X×Y exactly when u lies in X and v lies in Y, and the Cartesian product of two sets is a set.- Defines y^x, for sets x and y, as the class of all sets f that are functions from x to y.
Injective, Surjective and Bijective Functions between Classes
definitiondef:injective-surjective-bijective-nbg-2026aSet TheoryDefines when a function F:A→B between classes is injective, surjective onto B, or bijective.- Defines the identity id_A on a class A as the class of all ordered pairs (u,u) with u in A.
- Defines a binary operation on a set as a function from its Cartesian square to the set, with the infix notation for its values.
The Restriction of a Function or Relation to a Class
definitiondef:restriction-function-nbg-2026aSet TheoryDefines the restriction F|_A of a class F (typically a function) to a class A as the class of those ordered pairs in F whose first component lies in A.