中文 👈

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

choukh / set-theory Goto Github PK

set-theory's Introduction

Set-Theory

Requirement

Build

Meta.v

ZFC0.v

ZFC1.v

ZFC2.v

ZFC3.v

EST2.v

EST3_1.v

EST3_2.v

EST3_3.v

EST4_1.v

EST4_2.v

EST4_3.v

EST5_1.v

EST5_2.v

EST5_3.v

EST5_4.v

EST5_5.v

EST5_6.v

EST5_6.v

EST6_1.v

EST6_2.v

EST6_3.v

EST6_4.v

EST6_5.v

EST6_6.v

EST7_1.v

EST7_2.v

EST7_3.v

EST7_4.v

EST7_5.v

EST7_6.v

EST8_1.v

EST8_2.v

EST8_3.v

EST8_4.v

EST8_5.v

EST8_6.v

EST8_7.v

EX{n}.v

set-theory's People

Contributors

Stargazers

Watchers

Forkers

set-theory's Issues

Recommend Projects

Recommend Topics

Recommend Org