Library Continuum.Basic_Set_Theory
- 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
- Descriprion
- Numerals
- Cartesian Product
- Disjoint Union
Library Continuum.Cardinality
- Bijection
- Bijection Relation
- Injection
- Injection Relation
- Power Set
- Cartesian Product
- Disjoint Union
- Surjection
- Small Classes as Sets
Library Continuum.Ordinals
- Isomorphism
- Isomorphism Relation
- Ordinals
- Order on Ordinals
- Isomorphic Ordinals are Equal
- Encode Relation
- Transport Relation
Library Continuum.Hartogs_Number
Library Continuum.Sierpinskis_Theorem
This page has been generated by coqdoc