Lean集合论库
Lean集合论库[编辑 | 编辑源代码]
Lean集合论库（Mathlib's Set Theory Library）是Lean定理证明器中用于形式化集合论基础的核心数学库。它为初学者和研究者提供了从朴素集合论到高级拓扑概念的严格形式化工具，完全兼容ZFC公理系统。
核心概念[编辑 | 编辑源代码]
集合的定义[编辑 | 编辑源代码]
在Lean中，集合被定义为某种类型的谓词（即α → Prop）：
def Set (α : Type u) := α → Prop
基本操作通过以下公理实现：
- 空集：
∅或Set.empty - 全集：
Set.univ - 成员关系：
∈（定义为中缀符号） - 子集关系：
⊆
集合运算[编辑 | 编辑源代码]
库中实现了完整的布尔代数运算：
example (A B : Set ℕ) : A ∩ B = B ∩ A := by exact Set.inter_comm A B
example (A : Set ℕ) : A ∪ Aᶜ = Set.univ := Set.union_compl_self A
重要结构[编辑 | 编辑源代码]
有限集[编辑 | 编辑源代码]
使用Finset类型处理有限集合：
import Mathlib.Data.Finset.Basic
def primesUnder10 : Finset ℕ := {2, 3, 5, 7}
#eval primesUnder10.card -- 输出: 4
无限集[编辑 | 编辑源代码]
通过基数理论处理无限集合：
theorem nat_infinite : ¬ (Set.Finite Set.univ : Set ℕ) :=
Set.infinite_univ
应用案例[编辑 | 编辑源代码]
关系证明[编辑 | 编辑源代码]
证明德摩根定律的形式化版本：
theorem deMorgan (A B : Set α) : (A ∪ B)ᶜ = Aᶜ ∩ Bᶜ := by
ext x
simp only [Set.mem_compl_iff, Set.mem_union, Set.mem_inter_iff, not_or]
tauto
拓扑学基础[编辑 | 编辑源代码]
定义开集的基本性质：
def isOpen (S : Set ℝ) : Prop :=
∀ x ∈ S, ∃ ε > 0, Metric.ball x ε ⊆ S
可视化表示[编辑 | 编辑源代码]
进阶主题[编辑 | 编辑源代码]
选择公理[编辑 | 编辑源代码]
库中完整实现了选择公理的多个等价形式：
#check Classical.choice -- 选择函数
#check Zorn.lemma -- 佐恩引理
#check Cardinal.choose_spec -- 基数选择
基数算术[编辑 | 编辑源代码]
处理无限集合的大小比较：
example : Cardinal.mk ℕ = Cardinal.aleph0 := rfl
example : Cardinal.mk ℝ = Cardinal.c := rfl
学习建议[编辑 | 编辑源代码]
1. 从Mathlib.Data.Set.Basic开始学习基础操作
2. 通过Mathlib.Topology.Basic理解拓扑应用
3. 参考Mathlib.SetTheory.Cardinal.Basic研究无限集合
该库完整覆盖了从本科到研究级的集合论内容，所有定义都经过机器验证，是学习形式化数学的理想工具。