README.zh-CN.md

Set-Theory

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

系统要求

Coq 8.13.2

编译

make

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

• 元语言自然数(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

• 序类型乘法
• 序类型算术定律

EST8_5.v

• 良序结构上的序类型算术

EST8_6.v

• 序数算术（基于序类型算术）
  • 加法，乘法

EST8_7.v

• 序数算术（基于递归定义）
  • 加法，乘法，乘方
• 迭代幂次，ε数

EX{n}.v

• 第n章习题的解答