Set-Theory

KO | EN

gitlite — search

#javascript #python #react #go #machine-learning #rust #linux #docker #macos #java #windows #security #ios #openai

(★ 60)

A formalization of the textbook Elements of Set Theory

Set-Theory 최신버젼 다운로드

최종 버전 다운로드 (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

[中文](./README.zh-CN.md) 👈

# 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

Set-Theory

Set-Theory 최신버젼 다운로드

오늘의 추천 프로젝트

Was this content helpful?

Recent Feedback

Set-Theory

Set-Theory 최신버젼 다운로드

오늘의 추천 프로젝트

Was this content helpful?

Recent Feedback

Download README