跳轉到

9.4 專案：中間值定理#

本節目標#

  • 敘述中間值定理（IVT）並設計證明策略（sup 定義法）。
  • 完整走一遍 Lean 開發流程：敘述 → 骨架 → 填洞 → 完成。
  • 學會查閱並套用 Mathlib 現有的 IVT lemma（intermediate_value_Icc、IsIntermediateValue）。
  • 應用：證明 \(x^3 + x - 1 = 0\) 有實根。
  • 反思：拓樸抽象如何讓一個大定理變成兩行。

敘述：中間值定理#

定理（IVT）。設 \(f : [a, b] \to \mathbb{R}\) 連續， \(u\) 是介於 \(f(a)\) 與 \(f(b)\) 之間的實數（含端點），則存在 \(c \in [a, b]\) 使 \(f(c) = u\) ：

\[ \min(f(a), f(b)) \le u \le \max(f(a), f(b)) \implies \exists\, c \in [a, b],\ f(c) = u. \]

這是分析學最「體感」的定理：氣溫從早上的 \(15°C\) 連續升到中午的 \(28°C\) ，途中必有一刻恰好 \(20°C\) 。畫圖上它等價於「連續函數的圖像不能跳著畫、筆不能離紙」。

Mathlib 把「 \(u\) 落在 \(f\) 在 \([a,b]\) 上取值範圍內」打包成謂詞 IsIntermediateValue（「 \(y \in f\,s\) 的被夾住版本」）；更實用的查詢入口：

#check @intermediate_value_Icc
#check @IsCompact.exists_isIntermediateValue

intermediate_value_Icc 的大意：連續函數在 Icc a b 上的像包含整個閉區間 \([\min f(a)\ f(b),\ \max f(a)\ f(b)]\) 。

證明策略：sup 定義法#

不看 Mathlib，自己證。核心困難：我們只知道 \(f(a) \le u \le f(b)\) ，要憑空造出一個 \(c\) 。這正是完備性的舞臺——用 sup 從集合中「榨」出一個實數。

證明。不妨設 \(f(a) \le u \le f(b)\) （否則對 \(-f\) 套同樣論證）。定義

\[ c = \sup \{ x \in [a, b] : f(x) \le u \}. \]

集合非空（含 \(a\) ）、有上界（ \(\le b\) ），故 \(c\) 存在。宣稱 \(f(c) = u\) ：

  • ** \(f(c) \le u\) **：存在 \(x_n \in S\) 上升逼近 \(c\) ； \(f(x_n) \le u\) ，而 \(f\) 連續，取極限得 \(f(c) \le u\) 。
  • ** \(f(c) \ge u\) **：若 \(f(c) < u\) ，由 \(f\) 在 \(c\) 連續，存在 \(\delta > 0\) 使 \(x \in [c, c + \delta)\) 時 \(f(x) < u\) ，這與 \(c\) 是上確界矛盾（可以再往上跳 \(\delta/2\) ）。

兩個不等式夾出 \(f(c) = u\) 。注意論證的三個支柱：sup 存在（完備性）、連續性搬運不等式（ \(x_n \to c \Rightarrow f(x_n) \to f(c)\) ）、開性製造餘量（ \(f(c) < u\) 時附近也 \(< u\) ）。9.1 節的拓樸語言把第三根支柱抽象成「 \(\{y : y < u\}\) 是開集」。

Lean 開發流程：敘述 → 骨架 → 填洞 → 完成#

第一步：敘述#

把定理寫成 Lean 型別。先練習自己寫，再對照 Mathlib：

theorem my_ivt {f : ℝ → ℝ} (hf : Continuous f) (a b : ℝ) (hab : a ≤ b) {u : ℝ}
    (hau : f a ≤ u) (hub : u ≤ f b) : ∃ c ∈ Set.Icc a b, f c = u := by
  sorry

型別檢查通過、sorry 補洞——這是骨架階段。Lean 的態度：敘述寫錯，後面全白搭，所以先讓編譯器驗收題目。

第二步：填洞（先試 Mathlib 現成定理）#

打開洞之前，先問：Mathlib 有現成的嗎？搜尋策略：exact? 針對目標型別搜尋，或用關鍵字（intermediate_value、exists_isIntermediateValue、Continuous.exists_*）找 lemma 名。找到關鍵 lemma：

theorem intermediate_value_Icc (hf : Continuous f) (hab : a ≤ b) :
    f '' Set.Icc a b = Set.Icc (f a) (f b)   -- 精神版本，實際含 min/max

實際上 Mathlib 對 intermediate_value_Icc 的形式是：像集包含（或等於） \(f(a)\) 與 \(f(b)\) 間的閉區間。套用之：

example {f : ℝ → ℝ} (hf : Continuous f) (a b : ℝ) (hab : a ≤ b) {u : ℝ}
    (hau : f a ≤ u) (hub : u ≤ f b) : ∃ c ∈ Set.Icc a b, f c = u := by
  have h := intermediate_value_Icc hab hf   -- 取得像集的資訊
  -- u 落在像區間內，故可取出前像點
  obtain ⟨c, hc, rfl⟩ := (mem_image _ _ _).mp (by rw [h]; exact ⟨hau, hub⟩)
  exact ⟨c, hc, rfl⟩

（實際套用時，lemma 的確切形式可能要求 min (f a) (f b) ≤ u ≤ max (f a) (f b)，此時先證 min_le_of...、le_max... 兩個排序引理再代入。用 exact? 和 apply? 迭代，是 Mathlib 工作流的日常。）

第三步：自己填（體驗 sup 法）#

若想體驗從零開發，用 Mathlib 的 sup 工具： 

example {f : ℝ → ℝ} (hf : Continuous f) (a b : ℝ) (hab : a ≤ b) {u : ℝ}
    (hau : f a ≤ u) (hub : u ≤ f b) : ∃ c ∈ Set.Icc a b, f c = u := by
  set S : Set ℝ := {x | a ≤ x ∧ x ≤ b ∧ f x ≤ u} with hS
  have hne : S.Nonempty := ⟨a, hau, le_refl a, hab⟩
  have hbd : BddAbove S := ⟨b, by rintro x ⟨-, hx, -⟩; exact hx⟩
  obtain ⟨c, hc⟩ := hbd.exists_isLUB    -- 完備性：sup 存在
  by_cases hle : f c ≤ u
  · by_contra hgu; push_neg at hgu      -- 假設 f c > u
    -- 連續性：c 附近 f x > u，可推 c 不是上界，矛盾
    sorry
  · push_neg at hle                     -- f c > u 的另一半
    sorry

真正填滿每個 sorry 需要連續性的 ε-δ 拆解與 sup 的逼近引理，對初學者是數百行的工程——所以先走第二步的 Mathlib 路，再回頭挑戰第三步。完成的標誌：#print axioms my_ivt 只依賴 propext、Classical.choice、Quot.sound（無 sorryAx），且敘述可被 example 復現套用。

應用： \(x^3 + x - 1 = 0\) 有實根#

數學解。令 \(f(x) = x^3 + x - 1\) 。 \(f(0) = -1 < 0\) ， \(f(1) = 1 > 0\) ， \(f\) 是多項式故連續。由 IVT，存在 \(c \in [0, 1]\) 使 \(f(c) = 0\) ，即方程有實根。（這個根其實是唯一實根，因為 \(f'(x) = 3x^2 + 1 > 0\) ， \(f\) 嚴格遞增——唯一性交給微分，存在性交給 IVT。）

Lean 版——最短的路是直接引 intermediate_value_Icc：

example : ∃ c : ℝ, c^3 + c - 1 = 0 := by
  have key : ∃ c ∈ Set.Icc (0:ℝ) 1, (fun x => x^3 + x - 1) c = 0 := by
    have hf : ContinuousOn (fun x => x^3 + x - 1) (Set.Icc 0 1) := by fun_prop
    have h1 : (fun x => x^3 + x - 1) (0:ℝ) ≤ 0 := by norm_num
    have h2 : (0:ℝ) ≤ (fun x => x^3 + x - 1) (1:ℝ) := by norm_num
    exact intermediate_value_Icc hf h1 h2 |>.intermediate_value
      (Set.nonempty_Icc.mpr ⟨0, le_refl 0⟩) 0 h1 h2
  obtain ⟨c, -, hc⟩ := key
  exact ⟨c, hc⟩

（lemma 名與參數隨 Mathlib 版本浮動；面對版本差異，exact? 是最可靠的指南。重點是套用格式：連續性 + 端點值夾住 0 ⟹ 根存在。）

反思：拓樸讓 IVT 變成兩行#

回顧整章，我們用三個拓樸積木重組了 IVT：

  1. ** \([a,b]\) 連通**（9.3 節，完備性的推論）；
  2. 連通集的連續像是連通的（9.3 節，原像開定義的一行證明）；
  3. ** \(\mathbb{R}\) 的連通子集是區間**（9.3 節）。

於是：

\[ f([a,b]) \text{ 是連通的} \implies f([a,b]) \text{ 是區間} \implies \text{包含 } f(a), f(b) \text{ 之間的一切值}. \]

核心積木是 IsConnected.image：連通集的連續像連通。對照 sup 證明（兩個方向的夾擊、ε-δ 搬運），抽象的收益一目瞭然：

  • 證明一次，處處適用：同樣的鏈條對任意拓樸空間的連通子集都成立，不必重新 ε-δ。
  • 概念分工清晰：完備性藏在「 \(\mathbb{R}\) 連通」這塊積木裡，其餘論證是純拓樸的。
  • 機器可驗收：每塊積木都是 Mathlib 獨立檢驗過的 lemma，IVT 被化約成拼裝問題。

這就是本書反覆出現的主題的終章展示：好的抽象不是把問題變難，而是把困難集中到一個可重用的角落。第 4 章 Peano 公理把自然數收進幾條公理，第 5 章 sup 公理撐起實數，第 9 章拓樸把「鄰近」收進三條公理——每一次抽象，都是為了下一次「兩行證明」。

小結與練習#

本節重點：

步驟 內容
敘述 ∃ c ∈ Icc a b, f c = u，先讓 Lean 驗收題目
策略 sup 定義法：完備性榨出 \(c\) ，連續性夾出 \(f(c) = u\)
Mathlib intermediate_value_Icc、IsIntermediateValue
抽象視角 連通 + 連續像 + 連通子集是區間

練習：

  1. 用 intermediate_value_Icc 在 Lean 中完成 \(x^3 + x - 1 = 0\) 有實根的完整證明（無 sorry）。
  2. 證明：四次方程 \(x^4 + x = 2\) 在 \([1, 2]\) 有根。
  3. 證明 IVT 的唯一性部分：若 \(f\) 嚴格遞增連續，則根唯一。
  4. 用「連續像連通」重推 9.2 節極值定理的關鍵步驟： \(f([a,b])\) 是緊緻區間 \([m, M]\) 。
  5. 挑戰題：完成第三步骨架中的 sorry，親手走完 sup 證明。（提示：對 \(\{y : y < u\}\) 用 isOpen_lt 風格的開性引理。）