中文
Set-Theory
This project is a Coq formalization of the textbook Elements of Set Theory - Herbert B. Enderton. It is basically written in the order of the textbook, without considering modularity. It is suitable as an aid to the learning of set theory, not as a general mathematical library.
Requirement
Coq 8.13.2
Build
make
Meta.v
- Law of excluded middle
- Church's iota operator
- Informative excluded middle
- Decidable inhabitance of type
ZFC0.v
- Axiom of extensionality
- Axiom of empty set
- Axiom of union
- Axiom of power set
- Axiom schema of replacement
ZFC1.v
- Pair
- Singleton
- Binary union
- Union of a family of sets
ZFC2.v
- Set comprehension
- Intersaction, binary intersaction
- Ordered pair
- Cartesian product
ZFC3.v
- Axiom of infinity
- Axiom of choice
EST2.v
- Complement
- Proper subset
- Algebra of sets
EST3_1.v
- Relation, function
- Inverse, composition
EST3_2.v
- Injection, surjection, bijection
- Left inverse and right inverse of function
- Restriction, image
- Function space
- Infinite Cartesian product
EST3_3.v
- Binary relation
- Equivalence relation, equivalence class, quotient set
- Trichotomy, linear order
EST4_1.v
- Natural number
- Induction principle
- Transitive set
- Peano structure
- Recursion theorem
EST4_2.v
- Embedding of type-theoretic nat
- Natural number arithmetic: addition, multiplication, exponentiation
EST4_3.v
- Linear ordering of ω
- Well ordering of ω
- Strong induction principle
EST5_1.v
- Integer
- Integer arithmetic: addition, additive inverse
EST5_2.v
- Multiplication of integers
- Order of integers
- Embedding of the natural numbers
EST5_3.v
- Rational number
- Rational number arithmetic: addition, additive inverse, multiplication, multiplicative inverse
EST5_4.v
- Order of rational numbers
- Embedding of the integers
- Algebra regarding to inverse
EST5_5.v
- Real number (Dedekind cut)
- Order of real numbers
- Completeness of the real numbers
- Real number arithmetic: addition, additive inverse
EST5_6.v
- Absolute value of real number
- Multiplication of non-negative real numbers
- Multiplicative inverse of positive real number
EST5_6.v
- Arithmetic of rational numbers: multiplication, multiplicative inverse
- Embedding of the rational numbers
- Density of the real numbers
EST6_1.v
- Equinumerous
- Cantor's theorem
- Pigeonhole principle
- Finite cardinal
EST6_2.v
- Infinite cardinal
- Cardinal arithmetic: addition, multiplication, exponentiation
EST6_3.v
- Dominate
- Schröder–Bernstein theorem
- Order of cardinals
- Aleph Zero
EST6_4.v
- Systematic discussion on AC
- Uniformization
- Infinite Cartesian product of nonempty sets is nonempty
- Choice function
- Cardinal comparability
- Zorn's lemma
- Tukey's lemma
- Hausdorff maximal principle
- Aleph Zero is the least infinite cardinal
- Dedekind infinite
- Infinite sum of cardinals
- Infinite product of cardinals
EST6_5.v
- Countable set
- Countable union of countable sets is countable
EST6_6.v
- Algebra of infinite cardinals
- Cardinal multiplied by itself equals to itself
- Absortion law of cardinal addition and multiplication
EST7_1.v
- Partial order, linear order
- Minimal, minimum, maximal, maximum
- Bound, supremum, infimum
EST7_2.v
- Well order
- Transfinite induction principle
- Transfinite recursion theorem
- Transitive closure of set
EST7_3.v
- Order structure
- Isomorphism
- Epsilon image
EST7_4.v
- Ordinal
- Order of ordinals
- Burali-Forti's paradox
- Successor ordinal, limit ordinal
- Transfinite induction schema on ordinals
EST7_5.v
- Hartog's number
- Equivalence among well order theorem, AC and Zorn's lemma
- von Neumann cardinal assignment
- Initial cardinal, successor cardinal
EST7_6.v
- Transfinite recursion schema on ordinals
- von Neumann universe
- Rank
- Axiom of regularity
EST8_1.v
- Ordinal class
- Ordinal operations
- Subclass separation
- Normal operation
- Aleph number
- Beth number
EST8_2.v
- Properties of ordinal operations
- Veblen fixed-point theorem
- Enumeration of fixed-point is normal operation
- There exist fixed-point of fixed-point
EST8_3.v
- Order types
- Addition of order types
EST8_4.v
- Multiplication of order types
- Laws of order type arithmetic
EST8_5.v
- Order type arithmetic on well-ordered structure
EST8_6.v
- Ordinal Arithmetic (defined as order type arithmetic)
- Addition, multiplication
EST8_7.v
- Ordinal Arithmetic (defined by recursion)
- Addition, multiplication, exponentiation
- Tetration, epsilon numbers
EX{n}.v
- Solution to exercises of Chapter n