Sierpinski.Basics
- Sets
- Classes
- Axiom of Extensionality
- Automation
- Axiom of Empty Set
- Axiom of Big Union
- Axiom of Power Set
- Axiom of Replacement
- Function Replacement
- Image
- Conditional Function Replacement
- Comprehension
- Axiom of Well-Foundedness
- Provisional Unordered Pair
- Provisional Singleton Set
- Union
- Adjunction
- Explicit Set Notation
- Indexed Union
- Indexed Intersection
- Intersection
- Set Difference
- Description
- Numerals
- Cartesian Product
- Disjoint Union
- Encodings
Sierpinski.Cardinality
- Bijection
- Bijection Relation
- Injection
- Injection Relation
- Power Set
- Cartesian Product
- Disjoint Union
- Surjection
- Small Classes as Sets
Sierpinski.Ordinals
- Isomorphism
- Isomorphism Relation
- Ordinals
- Ordinals are well-ordered
- Alternative characterisation
- Isomoprhic ordinals are equal
- More on ordinals
- Encode Relation
- Transport Relation