Formalised Set Theory: Well-Orderings and the Axiom of Choice

Browse the main library:

• A (Basic ZF)
• B (Relations and Functions)
• C (Ordinal Theory)
• D (Order Isomorphy)
• E (Induction and Recursion)
• F (Order Types and Hartogs Numbers)
• G (The Well-Ordering Theorem)

Browse the appendix:

• Z1 (Zermelo's 1904 proof, implemented by Jonas Kaiser/Danko Ilik)
• Z2 (Zermelo's 1908 proof, implemented by Chad Brown)
• EQ (equality/equivalence of both constructed orderings)

Documentation generated by Coqdoc. Click the respective index.html for an overall index of definitions and lemmas.