# 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章习题的解答