编辑“︁Lean集合”︁

= Lean集合 =  
'''Lean集合'''是Lean定理证明器中的基础数据结构之一，用于存储唯一元素的容器。它基于数学中的集合理论，支持常见的集合操作，如并集、交集、差集等。本章节将详细介绍Lean集合的定义、基本操作、实际应用以及高级特性。  

== 介绍 ==  
在Lean中，集合（`Set`）是一种表示数学集合的数据结构。它类似于列表，但集合中的元素是唯一的，且不保证顺序。Lean的`Set`类型定义在标准库`Mathlib`中，依赖于谓词逻辑来表示集合成员关系。  

集合的核心特征是：  
* '''唯一性'''：集合中的元素不会重复。  
* '''无序性'''：元素的存储顺序无关紧要。  
* '''动态性'''：集合可以动态增删元素。  

数学上，集合 <math>S</math> 可以表示为：  
<math>S = \{x \mid P(x)\}</math>  
其中 <math>P(x)</math> 是一个谓词，描述元素 <math>x</math> 是否属于集合 <math>S</math>。  

== 基本操作 ==  

=== 创建集合 ===  
在Lean中，可以通过`Set`构造函数或字面量语法创建集合：  

<syntaxhighlight lang="lean">  
-- 使用Set构造函数  
def mySet : Set Nat := {1, 2, 3}  

-- 使用谓词定义集合  
def evenNumbers : Set Nat := {n | n % 2 = 0}  
</syntaxhighlight>  

=== 成员检查 ===  
检查元素是否属于集合：  
<syntaxhighlight lang="lean">  
#eval 1 ∈ mySet  -- 输出: true  
#eval 4 ∈ mySet  -- 输出: false  
</syntaxhighlight>  

=== 集合运算 ===  
Lean支持常见的集合运算：  
<syntaxhighlight lang="lean">  
def setA : Set Nat := {1, 2, 3}  
def setB : Set Nat := {3, 4, 5}  

-- 并集  
#eval setA ∪ setB  -- 输出: {1, 2, 3, 4, 5}  

-- 交集  
#eval setA ∩ setB  -- 输出: {3}  

-- 差集  
#eval setA \ setB  -- 输出: {1, 2}  
</syntaxhighlight>  

== 高级特性 ==  

=== 集合的证明 ===  
Lean的集合与定理证明紧密结合。例如，可以证明两个集合相等：  
<syntaxhighlight lang="lean">  
example : {1, 2, 3} = {3, 2, 1} := by  
  simp only [Set.insert_empty_eq_singleton, Set.singleton_union]  
</syntaxhighlight>  

=== 有限与无限集合 ===  
Lean区分有限集合（`Finset`）和无限集合（`Set`）。`Finset`提供了更高效的运算：  
<syntaxhighlight lang="lean">  
import Mathlib.Data.Finset.Basic  

def finiteSet : Finset Nat := {1, 2, 3}  
#eval finiteSet.card  -- 输出: 3  
</syntaxhighlight>  

== 实际案例 ==  

=== 案例1：过滤唯一元素 ===  
假设我们需要从一个列表中提取唯一元素：  
<syntaxhighlight lang="lean">  
def uniqueElements (lst : List Nat) : Set Nat := lst.toSet  

#eval uniqueElements [1, 2, 2, 3]  -- 输出: {1, 2, 3}  
</syntaxhighlight>  

=== 案例2：集合覆盖问题 ===  
解决一个简单的集合覆盖问题：  
<syntaxhighlight lang="lean">  
def universe : Set Nat := {1, 2, 3, 4, 5}  
def subsets : List (Set Nat) := [{1, 2}, {3, 4}, {4, 5}]  

-- 检查是否覆盖全集  
def isCovered : Bool := subsets.foldl (· ∪ ·) ∅ = universe  
#eval isCovered  -- 输出: false  
</syntaxhighlight>  

== 可视化 ==  
使用Mermaid展示集合关系：  
<mermaid>  
vennDiagram  
    title 集合运算示例  
    setA ["1", "2", "3"]  
    setB ["3", "4", "5"]  
    setA ∩ setB ["3"]  
    universe ["1", "2", "3", "4", "5"]  
</mermaid>  

== 总结 ==  
Lean集合是功能强大的数据结构，适用于数学证明和编程任务。通过本章的学习，您应掌握：  
* 集合的基本定义与操作。  
* 如何用Lean进行集合运算和证明。  
* 实际场景中集合的应用方法。  

下一步可以学习[[Lean中的函数]]或[[Lean定理证明]]以深入理解Lean的其他核心概念。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean数据结构]]