集合的运算与性质

Introduction

有了集合的基本概念，我们来学习集合运算。 - **并集** `A ∪ B`：元素属于 A 或属于 B - **交集** `A ∩ B`：元素同时属于 A 和 B 本关目标：证明交集的**交换律**——`A ∩ B = B ∩ A`。在 Lean 中，集合相等 `A = B` 用**外延公理**：两个集合相等当且仅当它们包含完全相同的元素。也就是说，`A = B ↔ (∀ x, x ∈ A ↔ x ∈ B)`。所以证明集合相等，就是对任意 x，证明 x ∈ A ∩ B ↔ x ∈ B ∩ A。展开定义后，本质上就是证明 `∧` 的交换律——你已经会了！

本关学到的新东西

策略 (Tactics)

ext外延性 (extensionality)：把集合等式 A = B 展开为 ∀ x, x ∈ A ↔ x ∈ B

概念 (Concepts)

∪ (并集)A ∪ B = {x | x ∈ A ∨ x ∈ B}。用 left/right 构造，用 rcases 拆

∩ (交集)A ∩ B = {x | x ∈ A ∧ x ∈ B}。用 ⟨⟩ 构造，用 rcases 拆

外延公理两个集合相等 ⟺ 它们包含完全相同的元素

证明目标

当前目标

A B : Set Nat

⊢A ∩ B = B ∩ A

分步提示

1.用 `ext x` 策略。它把集合相等的目标展开为：对任意元素 x，x ∈ A∩B ↔ x ∈ B∩A。
2.现在目标是 `x ∈ A ∩ B ↔ x ∈ B ∩ A`。用 `constructor` 把它拆成两个方向。
3.第一个方向 `x ∈ A ∩ B → x ∈ B ∩ A`：用 `intro h`，然后 `rcases h with ⟨hA, hB⟩` 拆开交集。
4.现在要用 `hA : x ∈ A` 和 `hB : x ∈ B` 证明 `x ∈ B ∩ A`。`∩` 的构造用 `⟨⟩` 角度括号，即 `exact ⟨hB, hA⟩`。
5.第二个方向完全对称：`intro h; rcases h with ⟨hB, hA⟩; exact ⟨hA, hB⟩`。

怎么玩：编辑器里有预写代码。直接点 运行 ▶ 看效果，或修改代码后运行。卡住了看左侧的提示。

Lean 代码编辑器