Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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.- Defines a well-order on a set as a total order on it in which every subset with at least one element has a least element.
- Defines the image R[A] of a class A under a class R, and the preimage F^{-1}[B] of a class B under a class F as the image of B under the inverse relation of F.
Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders
lemmalem:partial-order-nbg-2026aSet TheoryFor a partial order on a set: a subclass has at most one least and one greatest element; the strict relation is characterized by u <= v and u != v, is irreflexive and transitive, and u <= v iff u < v or u = v; for a total order, trichotomy holds and the negation of u <= v is v <…Partial and Total Orders on a Set and the Associated Strict Relation
definitiondef:partial-order-nbg-2026aSet TheoryDefines partial orders (reflexive, antisymmetric, transitive relations on a set), total orders, and the strict relation associated with a partial order.Functions, Values of a Function, and Functions from One Class to Another
definitiondef:function-nbg-2026aSet TheoryDefines a function as a single-valued relation, its value F(u) at a point u of its domain, and functions (maps) F:A→B from a class A to a class B.- Defines a relation as a class of ordered pairs, and the domain, range, inverse and composition of classes regarded as relations, together with relations on a class.
Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection
lemmalem:equivalence-classes-nbg-2026aSet TheoryFor an equivalence relation R on a set a: classes are equal iff their elements are related, distinct classes are disjoint, the nonempty classes cover a and each is the class of any of its elements, the quotient a/R is a set, and the canonical projection is a surjection from a ont…- Defines the Cartesian product X×Y of two classes as the class of all ordered pairs (u,v) with u in X and v in Y.
- Defines an equivalence relation on a set as a reflexive, symmetric and transitive relation on it.