编辑“︁Lean集合论库”︁（章节）

= Lean集合论库 =

'''Lean集合论库'''（Mathlib's Set Theory Library）是[[Lean定理证明器]]中用于形式化集合论基础的核心数学库。它为初学者和研究者提供了从朴素集合论到高级拓扑概念的严格形式化工具，完全兼容[[ZFC公理系统]]。

== 核心概念 ==

=== 集合的定义 ===
在Lean中，集合被定义为某种类型<math>\alpha</math>的谓词（即<code>α → Prop</code>）：
<syntaxhighlight lang="lean">
def Set (α : Type u) := α → Prop
</syntaxhighlight>

基本操作通过以下公理实现：
* 空集：<code>∅</code> 或 <code>Set.empty</code>
* 全集：<code>Set.univ</code>
* 成员关系：<code>∈</code>（定义为中缀符号）
* 子集关系：<code>⊆</code>

=== 集合运算 ===
库中实现了完整的布尔代数运算：
<syntaxhighlight lang="lean">
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
</syntaxhighlight>

== 重要结构 ==

=== 有限集 ===
使用<code>Finset</code>类型处理有限集合：
<syntaxhighlight lang="lean">
import Mathlib.Data.Finset.Basic

def primesUnder10 : Finset ℕ := {2, 3, 5, 7}
#eval primesUnder10.card -- 输出: 4
</syntaxhighlight>

=== 无限集 ===
通过基数理论处理无限集合：
<syntaxhighlight lang="lean">
theorem nat_infinite : ¬ (Set.Finite Set.univ : Set ℕ) := 
  Set.infinite_univ
</syntaxhighlight>

== 应用案例 ==

=== 关系证明 ===
证明德摩根定律的形式化版本：
<syntaxhighlight lang="lean">
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
</syntaxhighlight>

=== 拓扑学基础 ===
定义开集的基本性质：
<syntaxhighlight lang="lean">
def isOpen (S : Set ℝ) : Prop := 
  ∀ x ∈ S, ∃ ε > 0, Metric.ball x ε ⊆ S
</syntaxhighlight>

== 可视化表示 ==

<mermaid>
graph TD
    A[Set α] --> B[Finite]
    A --> C[Infinite]
    B --> D[Finset]
    C --> E[Countable]
    C --> F[Uncountable]
    E --> G[ℕ]
    F --> H[ℝ]
</mermaid>

== 进阶主题 ==

=== 选择公理 ===
库中完整实现了选择公理的多个等价形式：
<syntaxhighlight lang="lean">
#check Classical.choice       -- 选择函数
#check Zorn.lemma             -- 佐恩引理
#check Cardinal.choose_spec   -- 基数选择
</syntaxhighlight>

=== 基数算术 ===
处理无限集合的大小比较：
<syntaxhighlight lang="lean">
example : Cardinal.mk ℕ = Cardinal.aleph0 := rfl
example : Cardinal.mk ℝ = Cardinal.c := rfl
</syntaxhighlight>

== 学习建议 ==
1. 从<code>Mathlib.Data.Set.Basic</code>开始学习基础操作
2. 通过<code>Mathlib.Topology.Basic</code>理解拓扑应用
3. 参考<code>Mathlib.SetTheory.Cardinal.Basic</code>研究无限集合

该库完整覆盖了从本科到研究级的集合论内容，所有定义都经过机器验证，是学习形式化数学的理想工具。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean与数学库]]