Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- There is a set containing the empty set and containing, along with each of its elements u, the set whose elements are those of u together with u itself.
- If a class assigns to each set at most one set through its ordered pairs, then the sets assigned to the elements of any given set form a set.
- For every set there is a set whose elements are exactly the sets all of whose elements belong to it.
- For every set there is a set whose elements are exactly the elements of its elements.
- The elements of a set that belong to a given class form a set.
- Seven class-existence axioms: the membership relation, intersections, complements and domains of classes, products with the universe, and two permutations of the entries of triples define classes.
The Characteristic Property of Ordered Pairs and Nested Tuples of Sets
lemmalem:ordered-pair-nbg-2026aSet TheoryTwo ordered pairs of sets are equal exactly when their first components and their second components are equal, and likewise two nested tuples of the same length are equal exactly when their entries agree.- The Kuratowski ordered pair of two sets x and y is the set {{x},{x,y}}; nested tuples of n sets are built by pairing the tuple of the first n-1 entries with the last.
The Empty Set, the Unordered Pair and the Singleton
definitiondef:empty-set-pair-singleton-nbg-2026aSet TheoryThe empty set is the unique set with no elements; the unordered pair of two sets is the unique set whose elements are exactly those two; the singleton of a set is the pair of the set with itself.Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique
lemmalem:empty-set-pair-unique-nbg-2026aSet TheoryEvery element of a class is a set; there is exactly one set with no elements, and every class with no elements equals it; and for any two sets there is exactly one set whose elements are exactly those two.- There is a set with no elements.
- For any two sets there is a set whose elements are exactly those two sets.
- Two classes with the same elements are equal.
Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations
definitiondef:formula-class-theory-nbg-2026aLogicSet TheoryA metatheoretic definition of the formulas of class theory, built from membership and equality between class and set variables, of their free variables, of predicative formulas (no quantifier over a class variable), and of defined set symbols as abbreviations.- The primitive notions of class theory are class and membership; a set is a class that is an element of some class, and a proper class is a class that is not a set.
Definition of Sequences by Recursion on the Natural Numbers
lemmalem:sequence-recursion-natural-numbers-2026aSet TheoryGiven a starting point and a rule producing the next term from the index and the current term, there is exactly one sequence with that first term that obeys the rule.The Integer Lattice Admits an Enumeration by the Natural Numbers
lemmalem:integer-lattice-enumeration-2026aSet TheoryThe integer lattice of Euclidean space is countable and not finite, and therefore admits a bijection from the natural numbers onto it.- A subset of the natural numbers that is not finite is the set of terms of a strictly increasing sequence, which is a bijection onto it; consequently every countable set that is not finite is in bijection with the natural numbers.
- The set of natural numbers is not finite, and neither is any set that receives an injective map from it.
- The restriction of a map to a subset of its domain is the map on that subset taking the same values.