跳轉到

4.4 集合、函數與實數#

本節目標#

  • 理解 mathlib 的 Set α = α → Prop：集合即述詞
  • 用 funext 證明函數相等，進而證明集合相等
  • 掌握 Injective、Surjective、Bijective 的形式化定義與證明
  • 概觀實數的 Cauchy 序列完備化建構
  • 使用 lattice 的 le_antisymm 與 nlinarith
  • 完整走過一個小定理的開發流程：從 sorry 到完整證明

集合即述詞#

在 ZFC 中集合是原始物件；在 Lean 的型別論裡，集合是一個函數：

import Mathlib.Tactic

-- Set α 的定義（mathlib 原始碼，一字不差）
-- def Set (α : Type*) := α → Prop

variable (α : Type) (s : Set α)

#check s          -- s : Set α
#check s : α → Prop   -- 同一個東西的另一種看法

-- x ∈ s 就是「把述詞 s 套用在 x 上」
-- def Set.instMembership : Membership α (Set α) := ⟨fun s a => s a⟩

-- 交集、聯集、補集直接由邏輯連接詞定義
example (a b : Set α) : Set α := a ∩ b    -- {x | x ∈ a ∧ x ∈ b}
example (a b : Set α) : Set α := a ∪ b    -- {x | x ∈ a ∨ x ∈ b}
example (a : Set α) : Set α := aᶜ         -- {x | x ∉ a}

集合論的許多公理（如外延公理）在此不證自明，因為它們是函數與邏輯的性質：

-- 集合相等 = 逐點相等 = 函數相等（外延性的型別論化身）
example (a b : Set α) : a = b ↔ ∀ x, x ∈ a ↔ x ∈ b := by
  simp [Set.ext_iff]

funext：函數相等#

兩個函數相等，當且僅當在每個輸入上輸出相等：

#check funext
-- funext : (∀ x, f x = g x) → f = g
#check funext_iff
-- funext_iff : f = g ↔ ∀ x, f x = g x

-- 例：證明兩個集合（述詞）相等
example (a : Set α) : a ∩ aᶜ = ∅ := by
  funext x                     -- 把集合相等化為逐點命題 x ∈ a ∩ aᶜ ↔ x ∈ ∅
  constructor
  · rintro ⟨h1, h2⟩            -- h1 : x ∈ a, h2 : x ∉ a
    exact h2 h1                -- 直接矛盾
  · intro h
    exact absurd h (Set.notMem_empty x)

funext x 在 tactic 模式中：目標若是 a = b（兩者為函數），就逐點化。這是函數外延性（function extensionality），它並非 Lean 核心的判定相等，而是一條需要引用的引理。

單射、滿射、雙射#

#check @Function.Injective
-- Injective f : ∀ a b, f a = f b → a = b
#check @Function.Surjective
-- Surjective f : ∀ b, ∃ a, f a = b
#check @Function.Bijective
-- Bijective f : Injective f ∧ Surjective f

範例：證明 \(f(n) = 2n + 1\) 是單射，且不是滿射。

def f (n : ℕ) : ℕ := 2 * n + 1

example : Function.Injective f := by
  intro a b hab
  simp only [f] at hab
  omega    -- 線性算術：由 2a+1 = 2b+1 推出 a = b

example : ¬ Function.Surjective f := by
  intro hsurj
  obtain ⟨k, hk⟩ := hsurj 0     -- 0 必須有原像
  simp [f] at hk                -- 2k + 1 = 0，在 ℕ 中不可能
  omega

經典定理 — Cantor–Bernstein 也內建於 mathlib：

#check @Function.Bijective_iff_hasInverse

實數的建構概觀#

Lean 的 ℝ 採用與 Dedekind 不同的路線：Cauchy 序列完備化（由 mathlib 的 Mathlib/Data/Real/Basic 完成）：

形式上：

#check ℝ                 -- ℝ : Type
#check Real.isComplete   -- 完備性：每個 Cauchy 序列收斂
#check Real.archimedean  -- 阿基米德性質

開發者的實用結論：你通常不需要知道 ℝ 是怎麼造的。mathlib 提供 ℝ 是「完備有序體」這一層抽象介面，就像你用 Vec<T> 不必知道記憶體佈局。但知道建構有助於理解為何某些引理（如 floor、sup 的存在）需要額外的工作。

order lattice 初步#

ℝ（以及多數有序結構）帶有 lattice 結構：每對元素有 min / max，以及 sup / inf 的存在。核心工具是反對稱性：

#check le_antisymm
-- le_antisymm : a ≤ b → b ≤ a → a = b

證明「兩個東西相等」的常用策略：證 ≤ 與 ≥ 兩個方向。這在實分析中無所不在，例如證明 Real.sqrt 的特徵性質。

nlinarith：非線性算術#

omega 只管線性；nlinarith 在 linear_combination / 乘法推理的幫助下處理部分非線性不等式：

example (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : a * b + 1 ≤ a * a + b * b + 1 := by
  nlinarith [sq_nonneg (a - b)]   -- 用 (a-b)² ≥ 0 這個額外事實

example (x : ℝ) (hx : x > 1) : x * x > x := by
  nlinarith [hx]                  -- 從 x > 1 推出 x² > x

nlinarith 的本質：把給定的非線性「事實」做線性組合，推出目標。給的提示越多，成功機率越高。

完整開發流程：從 sorry 到證明#

目標：證明對所有實數 \(x \geq 0\) ，有 \(x \leq x^2 + 1\) 。

第 1 步：骨架 + sorry

example (x : ℝ) (hx : 0 ≤ x) : x ≤ x^2 + 1 := by
  sorry

sorry 是佔位符：編譯通過但帶警告（declaration uses 'sorry'），適合先定義結構。

第 2 步：想數學。 我們要證 \(x^2 - x + 1 \geq 0\) 。配方： \(x^2 - x + 1 = (x - \frac{1}{2})^2 + \frac{3}{4} > 0\) 。

第 3 步：給 nlinarith 餵提示。

example (x : ℝ) (hx : 0 ≤ x) : x ≤ x^2 + 1 := by
  have h1 : (x - 1/2)^2 ≥ 0 := sq_nonneg _
  nlinarith [h1]

失敗了？看錯誤訊息：nlinarith 無法只從 (x - 1/2)² ≥ 0 得到目標。展開： \((x-\frac12)^2 \ge 0\) 給出 \(x^2 - x + \frac14 \ge 0\) ，於是 \(x^2 + 1 \ge x + \frac34\) —— 應該夠了。問題可能出在 1/2 被當成整數除法。改寫：

第 4 步：修正並完成。

example (x : ℝ) (hx : 0 ≤ x) : x ≤ x^2 + 1 := by
  have h1 : (x - 1 / 2 : ℝ) ^ 2 ≥ 0 := sq_nonneg _
  nlinarith [h1]

（關鍵細節：型別歸屬 (... : ℝ) 確保 1/2 是實數 \(\frac{1}{2}\) 而非自然數除法截斷。這是 Lean 初學者最常見的陷阱之一。）

第 5 步：清理。 移除多餘的 have、確認無 sorry 警告、lake build 通過 —— 完成。

這個循環 —— 骨架 → 數學草稿 → 餵提示 → 讀錯誤訊息 → 修正 —— 正是人機協作證明的日常節奏，也是第 5 章讓 LLM 參與證明開發的基礎。

小結與練習#

mathlib 的集合是述詞（Set α = α → Prop），集合相等由 funext 化為逐點邏輯；單射 / 滿射是精確的全稱／存在命題；ℝ 是 Cauchy 完備化的抽象介面；le_antisymm 與 nlinarith 是有序結構下的兩大利器。

練習：

  1. 證明 Set.univ 恆等式：a ∪ aᶜ = univ（用 funext + simp）。
  2. 證明 \(g(n) = 2n\) 不是滿射、是單射（在 ℕ 上）。
  3. 證明：(a b : ℝ) (h : a ≤ b) : min a b + max a b = a + b（先展開 min/max 的定義）。
  4. 用 nlinarith 證明：(a b : ℝ) (ha : 0 < a) (hb : 0 < b) : a * b > 0。
  5. 走完整開發流程：證明 (x : ℝ) : x * x + 3 * x + 2 ≥ 0 不對，改證 (x : ℝ) : (x + 1) * (x + 2) = x * x + 3 * x + 2 := by ring，再用 nlinarith 證明 (x : ℝ) : x ≤ x^2 + 2。