3.2 集合運算#

本節目標#

理解交集、聯集、補集、差集在 Lean 中的定義。
學會用「元素層次的展開」證明集合恆等式。
認識分配律與 De Morgan 律的集合版本及對應 API。
初步接觸 indexed union / intersection \(\bigcup_{i \in I}\) 。
練習：證明 \((A \cup B)^c = A^c \cap B^c\) 。

基本運算的定義#

所有運算都在述詞層次定義，每個定義都可以逐點展開：

運算	數學記號	Lean 定義（逐點）
交集	\(A \cap B\)	`x ∈ A ∧ x ∈ B`
聯集	\(A \cup B\)	`x ∈ A ∨ x ∈ B`
補集	\(A^c\)	`x ∉ A`
差集	\(A \setminus B\)	`x ∈ A ∧ x ∉ B`
全集	\(U\)	`Set.univ = fun _ => True`
空集	\(\varnothing\)	`Set.empty = fun _ => False`

import Mathlib

variable {α : Type*} (A B : Set α)

example : A ∩ B = {x | x ∈ A ∧ x ∈ B} := rfl
example : A ∪ B = {x | x ∈ A ∨ x ∈ B} := rfl

這兩個用 rfl 就能通過——因為運算就是這些述詞的簡寫。

逐點展開的證明套路#

證明集合恆等式的標準流程：

ext x：化約到元素層次。
展開運算的定義（simp [Set.mem_union, Set.mem_inter_iff] 等）。
剩下的就是純邏輯命題，交給 tauto 或 constructor + intro。

以聯集為例，Set.mem_union 的內容：

theorem Set.mem_union {s t : Set α} {x : α} : x ∈ s ∪ t ↔ x ∈ s ∨ x ∈ t := Iff.rfl

聯集的引理配套：Set.mem_union_left、Set.mem_union_right、 Set.union_eq 等；交集對應 Set.mem_inter_iff、Set.mem_inter。

分配律#

數學中的分配律：

\[ A \cap (B \cup C) = (A \cap B) \cup (A \cap C) \]

先手動證明一遍，體會「化約到邏輯」的過程：

example (A B C : Set α) : A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) := by
  ext x
  simp only [Set.mem_inter_iff, Set.mem_union]
  constructor
  · rintro ⟨hA, hB | hC⟩
    · exact Or.inl ⟨hA, hB⟩
    · exact Or.inr ⟨hA, hC⟩
  · rintro (⟨hA, hB⟩ | ⟨hA, hC⟩)
    · exact ⟨hA, Or.inl hB⟩
    · exact ⟨hA, Or.inr hC⟩

rintro ⟨hA, hB | hC⟩ 一口氣完成「拆合取、再拆析取」，這是述詞邏輯證明的常用技巧。實務上也可以一行的版本：

example (A B C : Set α) : A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) := by
  ext x; simp [and_or_left]

De Morgan 律的集合版本#

補集把命題邏輯的 De Morgan 律搬到集合層次：

\[ (A \cup B)^c = A^c \cap B^c, \qquad (A \cap B)^c = A^c \cup B^c \]

在 Lean 中，補集 Aᶜ 逐點定義為 x ∉ A，因此這兩條正好對應邏輯引理 not_or（ \(\neg(p \lor q) \iff \neg p \land \neg q\) ）與 not_and_or（ \(\neg(p \land q) \iff \neg p \lor \neg q\) ）。

example (A B : Set α) : (A ∪ B)ᶜ = Aᶜ ∩ Bᶜ := by
  ext x
  simp [Set.mem_compl_iff, Set.mem_union, Set.mem_inter_iff]
  exact not_or

example (A B : Set α) : (A ∩ B)ᶜ = Aᶜ ∪ Bᶜ := by
  ext x
  simp [Set.mem_compl_iff, Set.mem_inter_iff, Set.mem_union]
  exact not_and_or

Mathlib 其實已內建：Set.compl_union、Set.compl_inter、以及把補集與差集連結的 Set.diff_eq_compl_inter（A \ B = Aᶜ ∩ B... 精確形式見 Set.compl_inter 系列）。查 API 的好方法：先寫出逐點命題，再猜引理名稱，或用 exact?。

差集#

差集 \(A \setminus B\) 逐點為 \(x \in A\) 且 \(x \notin B\) ：

example (A B : Set α) : A \ B = A ∩ Bᶜ := by
  ext x
  simp [Set.mem_diff, Set.mem_inter_iff, Set.mem_compl_iff]
  tauto

差集常見性質：

example (A B : Set α) : A \ B ⊆ A := Set.diff_subset A B
example (A : Set α) : A \ A = ∅ := by
  ext x; simp [Set.mem_diff]

Indexed union 與 intersection 初步#

給定索引集 \(I\) 與一族集合 \(\{A_i\}_{i \in I}\) ，定義

\[ \bigcup_{i \in I} A_i = \{x \mid \exists i \in I,\; x \in A_i\}, \qquad \bigcap_{i \in I} A_i = \{x \mid \forall i \in I,\; x \in A_i\} \]

Lean 中以 Set.iUnion（⋃ i, s i）與 Set.iInter（⋂ i, s i）表示：

variable {I : Type*} (s : I → Set α)

example : (⋃ i, s i) = {x | ∃ i, x ∈ s i} := rfl
example : (⋂ i, s i) = {x | ∀ i, x ∈ s i} := rfl

同樣「定義即展開」。基本使用：

example (i : I) : s i ⊆ ⋃ i, s i :=
  fun x hx => Set.mem_iUnion_of_mem i hx

example : ⋂ i, s i ⊆ s 0 := by
  intro x hx
  exact hx 0

Set.mem_iUnion_of_mem 是「族中某個集合的元素必在聯集中」的便捷引理；反方向，聯集中的元素給出某個見證索引（Set.mem_iUnion 展開為 ∃ i, x ∈ s i，用 rcases 拆出 \(i\) ）。

與有限運算的交換關係（對應邏輯中 \(\exists/\forall\) 與 \(\lor/\land\) 的分配）：

example (A B : Set α) : (⋃ i, (if i = 0 then A else B)) ⊆ A ∪ B := by
  intro x hx
  simp only [Set.mem_iUnion] at hx
  rcases hx with ⟨i, hi⟩
  by_cases h : i = 0
  · simp [h] at hi; exact Or.inl hi
  · simp [h] at hi; exact Or.inr hi

小結與練習#

集合運算全部定義在述詞層次，因此每個集合恆等式都能透過 ext + 邏輯引理化約成命題邏輯問題。indexed 運算則對應 \(\exists\) / \(\forall\) 量化。記住口訣：先 ext，再展開，後邏輯。

練習：

證明吸收律：A ∩ (A ∪ B) = A。
證明：A \ B 與 B \ A 互斥，即 (A \ B) ∩ (B \ A) = ∅。
證明聯集的另一分配律：A ∪ (B ∩ C) = (A ∪ B) ∩ (A ∪ C)。
用 not_and_or 手動證明 \((A \cap B)^c = A^c \cup B^c\) 。
證明無限聯集的上界性質： example (s : I → Set α) (i : I) : s i ⊆ ⋃ j, s j。
挑戰：證明 \((A \cup B)^c = A^c \cap B^c\) （本節主題的完整版，先 ext x，再 constructor 拆雙向，用 not_or）。