# Set-Theory

**Repository Path**: jimhacker/Set-Theory

## Basic Information

- **Project Name**: Set-Theory
- **Description**: Coq encoding of ZFC and formalization of the textbook Elements of Set Theory
- **Primary Language**: Unknown
- **License**: MIT
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2021-03-24
- **Last Updated**: 2021-03-24

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# Set-Theory

本项目为集合论教材Elements of Set Theory - Herbert B. Enderton的Coq形式化。基本按教材顺序编写，而没有考虑模块化。仅适合作为集合论教学的辅助，而不适合作为一个通用的数学库。

## 系统要求
```
Coq 8.13.1
```

## 编译
```
./build_all.sh
```

## ZFC0.v
- 元理论
  - 排中律
  - 希尔伯特ε算子
- 外延公理
- 空集公理
- 并集公理
- 幂集公理
- 替代公理

## ZFC1.v
- 配对，单集
- 二元并，集族的并

## ZFC2.v
- 集合建构式
- 任意交，二元交
- 有序对，笛卡尔积

## ZFC3.v
- 无穷公理
- 希尔伯特ε算子蕴含选择公理

## EST2.v
- 补集
- 真子集
- 集合代数定律

## EST3_1.v
- 关系，函数
- 逆，复合

## EST3_2.v
- 单射，满射，双射
- 函数的左右逆
- 限制，像
- 函数空间
- 无限笛卡尔积
- 选择公理等效表述1：函数存在右逆当且仅当它是满射
- 选择公理等效表述2：任意多个非空集合的笛卡尔积非空

## EST3_3.v
- 二元关系
- 等价关系，等价类，商集
- 三歧性，线序

## EST4_1.v
- 自然数
- 归纳原理
- 传递集
- 皮亚诺结构
- 递归定理

## EST4_2.v
- 元语言自然数(nat)的嵌入与投射
- 自然数算术：加法，乘法，乘方

## 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
- 序数操作的性质
- Veblen不动点定理
  - 不动点的枚举是规范操作
  - 存在不动点的不动点

## EST8_3.v
- 序类型
- 序类型加法

## EST8_4.v
- 序类型乘法
- 序类型算术定律

## EX{n}.v
- 第n章习题的解答