跳轉到

7.1 實數的建構#

本節目標#

  • 理解為什麼有理數 \(\mathbb{Q}\) 不夠用：數線上有「空隙」。
  • 認識兩條經典的建構路線：Dedekind cut 與 Cauchy 序列。
  • 了解 Lean/Mathlib 中 Real 的地位：它是公設化給出的型別，完整建構超出本書範圍。
  • 掌握完備性公理（least upper bound property）與 Real.sSup。
  • 認識 Archimedean 性質及其在 Lean 中的形式。

為什麼有理數不夠#

有理數 \(\mathbb{Q}\) 在四則運算下封閉，看起來十分稠密： 任給兩個相異有理數，中間必有另一個有理數（取平均即可）。 直覺上數線「塞滿」了有理數，似乎不會缺什麼。

但古希臘人發現了一個致命的空隙：邊長為 \(1\) 的正方形，其對角線長度 滿足

\[ x^2 = 2 \]

而方程 \(x^2 = 2\) 在 \(\mathbb{Q}\) 中無解。證明是經典的反證法：

假設 x = p/q（p, q 互質）滿足 x² = 2。
則 p² = 2q²，故 p 為偶數，寫 p = 2k。
代入得 4k² = 2q²，即 q² = 2k²，故 q 也是偶數。
p, q 皆為偶數，與互質矛盾。

換句話說，在 \(\mathbb{Q}\) 中，序列 \(1,\ 1.4,\ 1.41,\ 1.414,\ \dots\) （不斷逼近 \(\sqrt{2}\) ）「想收斂」卻沒有極限可收斂—— 極限的候補位置上是空的。這個空隙就是 \(\sqrt{2}\) 。

這種「該收斂卻無處收斂」的現象，正是分析學要解決的核心問題。 解法只有一個：把數線補滿，補出來的東西就是實數 \(\mathbb{R}\) 。

兩條建構路線#

歷史上補滿數線有兩條著名的路：

1. Dedekind cut（戴德金切割）

把每個實數想成「數線上的一次切割」：一個切割是將 \(\mathbb{Q}\) 分成左右兩半 \(A \cup B\) ，其中 \(A\) 的每個元素都小於 \(B\) 的每個元素。 切割 \(\sqrt{2}\) 就是

\[ A = \{q \in \mathbb{Q} \mid q < 0 \text{ 或 } q^2 < 2\} \]

即使 \(\sqrt{2}\) 不在 \(\mathbb{Q}\) 中，這個「左半邊」仍是完全確定的對象。 實數就被定義為所有這種切割的集合。

2. Cauchy 序列（柯西序列）

把實數想成「有理數的極限過程」：一個實數是一列有理數 \(a_1, a_2, a_3, \dots\) ，滿足「項與項之間越靠越近」：

\[ \forall \varepsilon > 0,\ \exists N,\ \forall m, n \ge N,\ |a_m - a_n| < \varepsilon \]

逼近 \(\sqrt{2}\) 的數列 \(1, 1.4, 1.41, 1.414, \dots\) 就「是」實數 \(\sqrt{2}\) 。 （技術上要對序列取等價類，因為不同的序列可以逼近同一個數。）

兩條路殊途同歸，建出的 \(\mathbb{R}\) 彼此同構。 Dedekind cut 直接體現「序」的直覺（完備性公理好講）， Cauchy 序列直接體現「極限」的直覺（分析學好做）。

Lean 中 ℝ 的地位#

在 Mathlib 中，實數是一個公設化的型別 Real：

-- Mathlib 中的實數是某個結構的「抽象」，我們只承諾它滿足哪些性質
#check (Real : Type)
#check (Real.instLinearOrderedField : LinearOrderedField ℝ)

重點觀念：

  • Lean 中 ℝ 不是用 Dedekind cut 或 Cauchy 序列「內建」的； 它由一系列結構 instance（有序體、完備性等）刻畫。
  • 這是典型的以性質定義物件（definition by characterization）做法： 只要一個物件滿足這些公理，關於它的定理就都成立。
  • Mathlib 中其實也做過完整的建構（例如 DedekindCut 相關發展、 Cauchy 序列的 Cauchy filter 完備化），但那需要濾波器、 拓撲等重型機具，超出本書範圍。我們直接使用現成的 ℝ。
-- 我們可以使用實數的運算與序，無須知道它的內部表示
example : (2 : ℝ) < 3 := by norm_num

example (x : ℝ) : x * 1 = x := by ring

這樣的好處：本章的證明只依賴 \(\mathbb{R}\) 的公理性質， 與具體建構無關——這也符合分析學的哲學。

完備性公理：least upper bound property#

\(\mathbb{R}\) 區別於 \(\mathbb{Q}\) 的關鍵公理是完備性：

完備性公理： \(\mathbb{R}\) 的每個非空、有上界的子集 \(S\) ， 都存在最小上界（supremum） \(\sup S\) 。

注意 \(\mathbb{Q}\) 不滿足這條：集合 \(\{q \in \mathbb{Q} \mid q^2 < 2\}\) 非空、有上界， 但它在 \(\mathbb{Q}\) 中沒有最小上界（候補 \(\sqrt{2}\) 不在 \(\mathbb{Q}\) 中）。

在 Lean 中，supremum 寫作 sSup：

-- `sSup S`：集合 S 的最小上界
#check (Real.sSup : Set ℝ → ℝ)

-- 完備性公理的 Mathlib 形式（簡化）：
#check @Real.sSup_nonempty
-- Real.sSup_nonempty : ∀ (s : Set ℝ), s.Nonempty → IsLUB s (sSup s)

其中 IsLUB s x 表示 \(x\) 同時是 \(s\) 的上界且是所有上界中最小的。 Mathlib 將「上界」「最小上界」定義為一般述詞：

-- 上界：∀ y ∈ S, y ≤ x
example (S : Set ℝ) (x : ℝ) (h : UpperBounds S x) :
    ∀ y ∈ S, y ≤ x := fun hy => h hy

-- 最小上界：本身是上界，且 ≤ 任何上界
example (S : Set ℝ) (x : ℝ) (h : IsLUB S x) (u : ℝ)
    (hu : ∀ y ∈ S, y ≤ u) : x ≤ u := h.2 hu

使用範例：證明 \(\sup \{x \in \mathbb{R} \mid x \le 1\} = 1\) 。 思路： \(1\) 是上界（顯然），且 \(1\) 屬於集合，所以任何上界都 \(\ge 1\) 。

example : sSup {x : ℝ | x ≤ 1} = 1 := by
  refine Real.sSup_eq_of_isLUB ⟨1, ?_, ?_⟩
  · -- 1 是上界
    intro y hy
    exact hy
  · -- 任何上界 u 滿足 1 ≤ u，因為 1 在集合裡
    intro u hu
    exact hu 1 (le_refl 1)

（實際寫作時以 Mathlib 現有引理名稱為準；exact? 與 apply? 是尋找這些引理的好幫手。）

直覺：supremum 是「貼著集合上緣的那個數」。 它可以屬於集合（如上例），也可以不屬於 （如 \(\sup \{x \mid x < 1\}\) 對開區間情形……本例剛好屬於； 但 \(\sup \{1 - 1/n \mid n \in \mathbb{N}\} = 1\) 不屬於該集合）。

Archimedean 性質#

完備性的重要推論是 Archimedean 性質：

任給實數 \(x > 0\) 與正數 \(y\) ，必存在自然數 \(n\) 使 \(n \cdot x > y\) 。 直覺：不論 \(y\) 多大、步長 \(x\) 多小，一直加 \(x\) 總有一天超過 \(y\) 。

等價的漂亮形式：對任意實數 \(x\) ，必存在整數 \(n\) 滿足

\[ n \le x < n + 1 \]

即每個實數都「夾」在兩個相鄰整數之間（ \(\lfloor x \rfloor\) 的存在性）。 另一個常用形式： \(\mathbb{N}\) 在 \(\mathbb{R}\) 中無上界—— 這正是 \(\mathbb{Q}\) （以及任何 Archimedean 有序體）與 非標準分析中「無窮大數」的差別所在。

Mathlib 以 typeclass Archimedean 刻畫這個性質，而 ℝ 擁有它：

#check (Real.instArchimedean : Archimedean ℝ)

-- Archimedean 性質：任意正實數，可以用自然數的倍數超越
#check @exists_nat_gt
-- exists_nat_gt : ∀ (x : ℝ), ∃ (n : ℕ), x < ↑n

-- 反向形式：任何 n ≥ 1 的倒數可任意小
example (ε : ℝ) (hε : 0 < ε) : ∃ (n : ℕ), (1 : ℝ) / n < ε := by
  obtain ⟨n, hn⟩ := exists_nat_gt (1 / ε)
  refine ⟨n + 1, ?_⟩
  have hpos : 0 < (n : ℝ) + 1 := by positivity
  calc (1 : ℝ) / (n + 1) ≤ (1 : ℝ) / (1 / ε) := by
        apply div_le_div_right (by norm_num)
        · linarith [hn]
  · rw [div_div_cancel_zero]
    · linarith
    · exact ne_of_gt hε

（第二個例子略去了若干細節步驟，讀者可視為習題； 關鍵是看出 exists_nat_gt 這類引理正是 Archimedean 性質的工具化。）

為什麼重要：下一節的 ε-N 定義中，我們要「取 \(N\) 大到某種程度」， 能這樣做就是因為 Archimedean 性質保證自然數沒有上界、 \(1/n\) 能任意小。沒有它，ε-N 定義會變成空話。

小結與練習#

本節要點：

  1. \(\mathbb{Q}\) 有「空隙」： \(x^2 = 2\) 無有理數解，數線必須補滿。
  2. 補法有二：Dedekind cut（用切割定義實數）與 Cauchy 序列（用極限過程定義實數）。
  3. Lean 中 ℝ 是公設化的：以有序體結構與完備性公理刻畫，不依賴內部表示。
  4. 完備性公理＝每個非空有上界集合有最小上界 sSup。
  5. Archimedean 性質是完備性的推論，是 ε-N 論證的幕後功臣。

練習：

  1. 證明 \(\sqrt{2}\) 是無理數（如正文所示反證法），並用 Lean 以 Rat 寫出關鍵步驟：若 \(p^2 = 2q^2\) 則 \(p, q\) 皆偶數。
  2. 設 \(S = \{q \in \mathbb{Q} \mid q > 0,\ q^2 < 2\}\) 。 說明 \(S\) 在 \(\mathbb{Q}\) 中為何沒有最小上界。
  3. 用 Real.sSup_eq_of_isLUB（或 exact? 找到的等價引理）證明 sSup {x : ℝ | x ≤ 2} = 2。
  4. 用 exists_nat_gt 證明：對任意實數 \(x\) ，存在 \(n : ℕ\) 使 \(x < n\) 且 \(n \le x + 1\) 。
  5. 說明為什麼「 \(\mathbb{N}\) 在 \(\mathbb{R}\) 中有上界」會違反 Archimedean 性質，並用完備性公理推出矛盾 （提示：若 \(\mathbb{N}\) 有上界，考慮 \(\sup \mathbb{N}\) ， 則 \(\sup \mathbb{N} - 1\) 也必須是上界，矛盾）。