跳轉到

3.4 基數與鴿籠原理#

本節目標#

  • 理解等勢（equinumerous）作為「一樣多」的型別論式定義。
  • 認識有限與無限的直覺定義。
  • 掌握鴿籠原理的 Lean 敘述與簡單應用。
  • 認識可數無限： \(\mathbb{N} \to \mathbb{Z}\) 的對應。
  • 了解 Cantor 對角線法的概念與 Lean 中的敘述（不給完整證明）。

等勢（equinumerous）#

問「兩個集合一樣多嗎？」最穩健的方式不是去「數」， 而是配對：若存在一個雙射把兩邊一一套起來，就稱它們等勢。 遠古牧人用石子數羊——每隻羊丟一顆石子、回來時每隻羊撿回一顆—— 正是雙射的思想，不需要知道「5」是什麼。

Lean 中，兩個型別等勢由 Equiv 表示（雙射連同反函數的套裝）：

def Equiv (α : Type u) (β : Type v) where
  toFun : α → β
  invFun : β → α
  left_inv  : invFun ∘ toFun = id
  right_inv : toFun ∘ invFun = id

記號 α ≃ β。集合層次則有 Set.Equinumerous 風格的概念 （Mathlib 以 Equiv 與 Set 結合），核心思想不變：

\[ A \sim B \iff \exists f,\; f \text{ 是 } A \to B \text{ 的雙射} \]

Equiv 比裸的 Function.Bijective 更好用，因為它內建了反函數， 方便計算與重寫；兩者可由 Equiv.ofBijective 互換。

有限與無限的直覺定義#

  • 有限：一個型別 α 有限，若它與某個 Fin n（前 \(n\) 個自然數）等勢。 Mathlib 的 Finite α 即是此意義（存在 \(n\) 與等價 \(\alpha \simeq \text{Fin } n\) ）。
  • 無限：Infinite α，即不有限。直覺上，無限集合可以「不斷拿出新元素」。
  • 集合層次：Set.Finite s（ \(s\) 可與某有限型別配對）、Set.Infinite s。
import Mathlib

example : Finite (Fin 10) := inferInstance
example : Infinite ℕ := inferInstance
example : Set.Finite ({1, 2, 3} : Set ℕ) := Set.toFinite _
example : Set.Infinite (Set.univ : Set ℕ) := Set.infinite_univ

有限與無限的關鍵差異：有限集合與其真子集不可能等勢； 無限集合可以。例如 \(n \mapsto 2n\) 把 \(\mathbb{N}\) 雙射到偶數這個真子集—— 這是 Hilbert 旅館悖論的核心，也是「無限」的組合學定義基礎。

鴿籠原理#

把 \(n+1\) 隻鴿子放進 \(n\) 個籠子，必有兩隻同籠。 Lean 敘述（Fintype 版本）：

theorem pigeonhole {α β : Type*} [Finite α] [Fintype β]
    (f : α → β) : ∃ a b, a ≠ b ∧ f a = f b

即：定義域比對應域「大」的函數必不單射。 Mathlib 對應引理為 Function.Injective.exists_ne_map_eq_of_card_lt、 Fintype.card_le_of_injective（單射給出基數不等式 \(\lvert \alpha\rvert \leq \lvert \beta\rvert\) ）。

簡單應用——抽屜裡 13 個人，必有兩人生日同月：

example : ¬ Function.Injective (fun (_ : Fin 13) => (12 : Fin 12)) := by
  intro hinj
  have hcard : Fintype.card (Fin 13) ≤ Fintype.card (Fin 12) :=
    Fintype.card_le_of_injective _ hinj
  simp at hcard

Fintype.card_le_of_injective 把「單射」轉成「基數不等式」， 而 13 ≤ 12 顯然荒謬。套路：把組合問題翻譯成基數問題。

更口語的版本：

example {α : Type*} [Fintype α] {β : Type*} [Fintype β]
    (h : Fintype.card β < Fintype.card α) (f : α → β) :
    ∃ a b, a ≠ b ∧ f a = f b := by
  by_contra hcon
  push_neg at hcon
  have : Fintype.card α ≤ Fintype.card β :=
    Fintype.card_le_of_injective _ hcon
  omega

可數無限： \(\mathbb{N} \to \mathbb{Z}\) 的對應#

可數無限＝與 \(\mathbb{N}\) 等勢。 \(\mathbb{Z}\) 看起來「比 \(\mathbb{N}\) 多一倍」， 但雙射

\[ 0, 1, -1, 2, -2, 3, -3, \dots \]

說明它們一樣多。Lean 中的實現（示意）：

def zEncode : ℤ → ℕ
  | Int.ofNat n => 2 * n
  | Int.negSucc n => 2 * n + 1

def zDecode : ℕ → ℤ
  | 0 => 0
  | (n + 1) => if (n + 1) % 2 = 1 then Int.ofNat ((n + 1) / 2 - (n + 1) / 2) * 0 + Int.negSucc ((n + 1) / 2 - 1)
               else Int.ofNat ((n + 1) / 2)

實務上 Mathlib 已內建 Int 與 ℕ 等勢的各種工具 （如 Int.equivNat 風格的構造與 Countable 實例）， 我們不需要手寫；重點是理解交錯列舉的技巧： 把負數與非負數「編織」進同一條無窮序列。 一般化後：可數個可數集合的聯集仍是可數的（沿對角線列舉）。

Lean 中的概念：

  • Countable α：存在從 \(\alpha\) 到 \(\mathbb{N}\) 的單射。
  • Set.Countable s： \(s\) 是可數集合。
  • Set.Countable.mono：可數集的子集可數。
  • Set.Countable.of_finite：有限必可數。
example : Countable ℤ := inferInstance
example (s : Set ℤ) : Set.Countable s := Set.to_countable s

Cantor 對角線法#

定理（Cantor, 1891）：不存在從 \(X\) 到其冪集 \(\mathcal{P}(X)\) 的滿射。 特別地， \(\mathbb{N}\) 與 \(\mathbb{R}\) （或 \(\mathcal{P}(\mathbb{N})\) ）不等勢， 無限也分大小。

證明概念：設 \(f : X \to \mathcal{P}(X)\) ，定義「對角線集合」

\[ D = \{x \in X \mid x \notin f(x)\} \]

若 \(D = f(d)\) ，問 \(d \in D\) 嗎？兩種情況都矛盾—— 正是羅素悖論的「良性版本」。列表圖像化：把 \(f(x_1), f(x_2), \dots\) 排成 0/1 表，沿對角線翻轉，得到的新行不在表中。

Lean 敘述（Mathlib 內建，Set.not_injective_of_self_empty 風格的 一般形式為 Cantor.surjection_not_injective / 核心： Set.eq_empty_iff_forall_notMem 配合構造對角集）：

theorem cantor {α : Type*} (f : α → Set α) : ∃ D, ∀ x, f x ≠ D := by
  refine ⟨{x | x ∉ f x}, fun x hx => ?_⟩
  by_cases h : x ∈ f x
  · exact absurd (hx ▸ h) (fun h' => h' h)   -- d ∈ f(d) 但對角集說 d ∉ f(d)
  · -- d ∉ f(d)，但對角集定義說 d 應在其中
    exact (hx ▸ h).elim

（示意骨架，Mathlib 有正式版本 Cantor 相關引理； 完整證明涉及精細的邏輯翻轉，此處只展示「對角集」如何出場。）

Set.Infinite 與對角線法的結論： Set.univ : Set (Set ℕ) 不可數——

example : ¬ Set.Countable (Set.univ : Set (Set ℕ)) := by
  intro hc
  -- 冪集可數 ⟹ 可與 ℕ 配對 ⟹ 與對角線法矛盾
  exact absurd hc (by
    intro h
    exact (Set.countable_iff_exists_injective.mp h) ▸ fun _ => trivial)

（同樣為示意框架；正式證明見 Mathlib 的 Set.Countable 相關檔案。）

小結與練習#

「一樣多」的正確定義是存在雙射，而不是看起來差不多； 有限與無限的分界在於「能否與自己的真子集等勢」； 鴿籠原理把組合直覺變成基數不等式； 可數無限可用交錯列舉處理 \(\mathbb{Z}\) ，但 Cantor 對角線法 說明無限有階梯， \(\mathcal{P}(\mathbb{N})\) 嚴格比 \(\mathbb{N}\) 大。

練習：

  1. 證明 Equiv.refl、Equiv.symm、Equiv.trans 的存在 （即等勢是等價關係；Mathlib 已提供，練習寫出敘述並理解）。
  2. 用 Fintype.card_le_of_injective 證明： 從 Fin 5 到 Fin 3 的任何函數都有兩個輸入映到同一輸出。
  3. 證明偶自然數集合 {n | Even n} : Set ℕ 是無限的 （提示：Set.Infinite.mono 從 Set.univ 出發，或用雙射 n ↦ 2n）。
  4. 寫出交錯列舉的下一步：證明 ℕ × ℕ 可數（Countable (ℕ × ℕ)）， 並想清楚對角線列舉法如何對應到 Lean 的證明策略。
  5. 挑戰（概念題）：寫出「對角線集合 \(D\) 不在 \(f\) 的像中」的 完整 Lean 敘述，並說明每一步的矛盾來自哪裡。