3.1 集合即述詞#

本節目標#

理解樸素集合論與型別論觀點下「集合」的差異。
認識 Lean 4 中 Set α 的定義：它其實就是 α → Prop。
學會使用集合建構式 {x | P x} 與 {x ∈ s | P x}。
掌握 ext（外延性）tactic 以及證明子集關係的標準套路。

樸素集合論 vs 型別論觀點#

在中小學與大學初等課程中，我們習慣「樸素集合論」：集合是一堆東西的搜集，元素與集合之間有明確的「屬於」關係 \(x \in A\) ，並且可以任意把東西收集成集合。

但樸素集合論若不加限制，會產生著名的羅素悖論（Russell's paradox）：考慮「所有不包含自己的集合所成的集合」 \(R = \{x \mid x \notin x\}\) ，則

\[ x \in R \iff x \notin x \]

令 \(x = R\) 便得到矛盾。公設化集合論（如 ZFC）正是為了避開這種矛盾而設計的。

在型別論（以及 Lean）中，觀點完全不同：

每個東西都有型別，例如 x : ℕ 表示 \(x\) 是自然數。
集合必須依附於某個型別：Set ℕ 是「自然數的集合」這個型別。
你不能把蘋果和數字混在同一個集合裡，因為它們型別不同。
一個集合就是一個述詞（predicate）：給定 \(x\) ，判斷「 \(x\) 在集合中」這個命題的真假。

換句話說，在 Lean 裡：

\[ \text{Set } \alpha \;=\; \alpha \to \text{Prop} \]

集合不再是「裝東西的袋子」，而是「分類東西的規則」。這個觀點自動避開了羅素悖論：不存在「所有集合的集合」，因為 Set α 中的元素必須屬於型別 α，而 Set α 本身是另一個（更大的）型別。

`Set α` 的定義與 `∈`#

在 Mathlib 中，Set 的定義（簡化後）如下：

def Set (α : Type u) := α → Prop

namespace Set

def instance : Membership α (Set α) :=
  ⟨fun s a => s a⟩   -- `a ∈ s` 就定義成 `s a`

end Set

重點：

s : Set α 其實是一個函數，把每個 a : α 對應到一個命題。
a ∈ s 就是 s a：判斷 \(a\) 是否屬於 \(s\) ，就是把述詞 \(s\) 套用在 \(a\) 上。
這表示許多關於集合的證明，本質上就是關於述詞的邏輯證明。

驗證一下這個等價關係（Mathlib 提供了 Set.mem_def）：

import Mathlib

example (s : Set ℕ) (a : ℕ) : a ∈ s ↔ s a :=
  Iff.rfl

Iff.rfl 能直接通過，代表 a ∈ s 和 s a 在定義上是同一件事。

集合建構式#

數學中常寫 \(\{x \mid P(x)\}\) ，Lean 中直接寫成：

def evens : Set ℕ := {x | Even x}
def big   : Set ℕ := {x | x > 100}

常見的另一種形式 \(\{x \in s \mid P(x)\}\) （「在 \(s\) 之中且滿足 \(P\) 的元素」）：

def smallEvens : Set ℕ := {x ∈ (fun (n : ℕ) => n) | Even x}
-- 慣用寫法：給一個具體的母集
def evenUnder10 : Set ℕ := {n ∈ Finset.range 10 | Even n}  -- 概念示意
-- 最常用的形式：
def evensOf (s : Set ℕ) : Set ℕ := {x | x ∈ s ∧ Even x}

嚴格來說，{x ∈ s | P x} 在 Mathlib 中是 Set.sep（分離公理， separation），它保證新集合是母集的子集——這正是 ZFC 中「從既有集合中篩出子集」的公設化版本：

example (s : Set ℕ) : {x ∈ s | Even x} ⊆ s := Set.sep_subset s _

外延性與 `ext` tactic#

集合相等的定義是外延性的：兩個集合相等，若且唯若它們有相同的元素。

\[ (A = B) \iff (\forall x,\; x \in A \iff x \in B) \]

Lean 中的陳述是 Set.ext：

theorem Set.ext {a b : Set α} (h : ∀ (x : α), x ∈ a ↔ x ∈ b) : a = b

實務上幾乎不用手動套用，而是使用 ext tactic，它會自動：

把目標 A = B 轉成 ∀ x, x ∈ A ↔ x ∈ B。
把雙向 iff 拆成兩個蘊含（配合 constructor）。

example : {x | Even x ∨ Odd x} = Set.univ := by
  ext x
  simp [Nat.even_or_odd x]

注意 ext x 之後，我們證明的是「對任意 \(x\) ， \(x\) 在左集合 \(\iff\) \(x\) 在右集合」—— 集合層次的問題被化約成元素層次的邏輯問題，這是集合論證明的核心套路。

子集關係的證明套路#

子集的定義：

\[ A \subseteq B \iff \forall x,\; x \in A \to x \in B \]

example (A B : Set ℕ) (h : ∀ x, x ∈ A → x ∈ B) : A ⊆ B := h

A ⊆ B 展開後就是 h 的型別，所以直接 := h 就能通過。

標準套路整理：

目標	套路
`A = B`（集合相等）	`ext x; simp [...]` 或 `ext x; constructor <;> intro h; ...`
`A ⊆ B`	`intro x hx`，然後把 `hx` 展開成述詞邏輯來推
`x ∈ {y \\| P y}`	展開為 `P x`（`simp` 或直接 `show`）

完整範例：

example (s : Set ℕ) : {x ∈ s | Even x} ⊆ {x | Even x} := by
  intro x hx
  -- hx : x ∈ {x ∈ s | Even x}
  show Even x   -- 直接展開建構式
  exact hx.2

example (s : Set ℕ) (h : ∀ x, x ∈ s → ¬ Even x) : {x | Even x} ∩ s = ∅ := by
  ext x
  constructor
  · rintro ⟨he, hs⟩
    exact h x hs he
  · intro h0
    exact absurd (Set.mem_empty _ h0) (by simp)

第一個例子中 hx.2 取出分離集合中「滿足述詞」的部分；第二個例子用 ext x 把交集等於空集化約成「 \(x\) 同時在兩邊 \(\to\) 矛盾」。

常見陷阱#

∈ 不是內建的關係：它由 Membership 實例定義，對 Set 而言就是函數套用。
忘記 ext：試圖直接證 A = B 而不化約到元素層次，通常會卡住。
Set α 不是型別：x : Set ℕ 與 x : ℕ 不同層次；要把集合當「論域」用時，考慮 ↥s（subtle coercion）。

小結與練習#

本節建立了核心觀點：在 Lean 中，集合就是述詞。 Set α = α → Prop、a ∈ s 就是 s a、集合相等就是逐點 iff，這三件事構成了之後所有集合運算證明的基礎。

練習：

證明：對任意 s : Set ℕ，有 s ⊆ s（用 fun x hx => hx）。
證明子集關係的傳遞律： example (A B C : Set ℕ) (h1 : A ⊆ B) (h2 : B ⊆ C) : A ⊆ C := by ...。
證明：{x | P x ∧ Q x} ⊆ {x | P x}。
用 ext 證明：{x | P x} = {y | P y}（注意變數名稱只是裝飾）。
挑戰：證明 Set.sep_subset 的內容—— example (s : Set ℕ) (P : ℕ → Prop) : {x ∈ s | P x} ⊆ s := by ...。