跳轉到

7.3 連續函數#

本節目標#

  • 理解 ε-δ 定義的數學意義，並建立「輸入誤差控制輸出誤差」的視覺直覺。
  • 認識 Mathlib 的 Continuous 定義（開集合的原像）及其與 ε-δ 的等價性。
  • 掌握一點版本 ContinuousAt。
  • 練習範例：多項式連續、 \(f(x) = 1/x\) 在 \(x \ne 0\) 連續。
  • 學會 Continuous.comp 與複合函數的連續性。

ε-δ 定義#

設 \(f : \mathbb{R} \to \mathbb{R}\) ， \(a\) 是一點。我們說 \(f\) 在 \(a\) 點連續：

\[ \forall \varepsilon > 0,\ \exists \delta > 0,\ \forall x,\ |x - a| < \delta \implies |f(x) - f(a)| < \varepsilon \]

與上一節的 ε-N 對照著讀：

序列極限 ε-N 連續 ε-δ
對手給 誤差容許量 \(\varepsilon\) 誤差容許量 \(\varepsilon\)
我們給 門檻 \(N\) （在時間軸上） 半徑 \(\delta\) （在空間軸上）
保證 \(n \ge N \implies \|a_n - L\| < \varepsilon\) \(\|x-a\| < \delta \implies \|f(x)-f(a)\| < \varepsilon\)

視覺直覺：把 \(\varepsilon\) 想成「在 \(y = f(a)\) 上下畫出寬度 \(2\varepsilon\) 的水平帶」， 連續的意思是：總能找到寬度 \(2\delta\) 的垂直帶，使得圖形進入垂直帶的部分 完全落在水平帶內。也就是：

只要輸入的誤差夠小，輸出的誤差就能壓到任意小。 輸入的小擾動不會造成輸出的突跳。

直觀的反例是階梯函數（符號函數）在 \(a = 0\) ：取 \(\varepsilon = 1/2\) ， 不論 \(\delta\) 多小，垂直帶內總有 \(x > 0\) 與 \(x < 0\) 兩側， 輸出分別是 \(1\) 與 \(-1\) ，無法同時落在 \((-1/2, 1/2)\) 的水平帶內——在 \(0\) 不連續。

Mathlib 的 Continuous：開集合的原像#

Mathlib 對全域連續的定義不是 ε-δ，而是拓樸的：

\(f\) 連續 \(\iff\) 每個開集的原像都是開集。

#check @Continuous
-- Continuous {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
--   (f : X → Y) : Prop
-- 結構：∀ U, IsOpen U → IsOpen (f ⁻¹' U)

為什麼這個定義與 ε-δ 等價？（ \(\mathbb{R}\) 的情形）

  • 「 \(\varepsilon\) -水平帶」就是開區間 \((f(a) - \varepsilon,\ f(a) + \varepsilon)\) ， 它是開集。
  • 若 \(f\) 連續，原像 \(f^{-1}(\text{開帶})\) 是開集，且包含 \(a\) ， 於是存在以 \(a\) 為中心的開區間 \((a - \delta, a + \delta) \subseteq f^{-1}(\text{開帶})\) ——這個 \(\delta\) 正是 ε-δ 定義要的。
  • 反過來，逐點 ε-δ 可以推出每個開集的原像是開集（每點都能放大一點 \(\delta\) -球）。

為什麼 Mathlib 選開集版本？ 因為它更一般：不需要度量、不需要序， 甚至不需要 \(\mathbb{R}\) 。同一個 Continuous 同時適用於 \(\mathbb{R}^n\) 、函數空間、圓圈、任何拓樸空間——定理只證一次。

要從 Continuous 取出 ε-δ 資訊，Mathlib 提供橋樑引理：

#check @ContinuousAt
-- ContinuousAt f a : Tendsto f (𝓝 a) (𝓝 (f a))

#check @ContinuousAt.mono_iff
#check @Metric.continuousAt_iff
-- Metric.continuousAt_iff :
--   ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ x, dist x a < δ → dist (f x) (f a) < ε

Metric.continuousAt_iff 就是我們熟悉的 ε-δ， 與 7.2 的 Metric.tendsto_atTop 同一系列。

ContinuousAt：一點版本#

一點連續 ContinuousAt f a 就是「在 \(a\) 點的 ε-δ 性質」， 用濾波器說是 Tendsto f (𝓝 a) (𝓝 (f a))——把 7.2 的 「尾段濾波器 → 鄰域濾波器」換成「鄰域 → 鄰域」而已。

兩者的關係與常用引理：

-- 全域連續 ⟹ 逐點連續
example (f : ℝ → ℝ) (hf : Continuous f) (a : ℝ) : ContinuousAt f a :=
  hf.continuousAt

-- 逐點連續的拆開形式
example (f : ℝ → ℝ) (a : ℝ) (h : ContinuousAt f a) :
    ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| < δ → |f x - f a| < ε := by
  rw [Metric.continuousAt_iff] at h
  simpa [Real.dist_eq] using h

範例一：多項式連續#

多項式由常數、恆等函數經加法與乘法組成， 而這些基本件的連續性 Mathlib 都有：

#check @continuous_const   -- 常數函數連續
#check @continuous_id      -- 恆等函數連續
#check @Continuous.add     -- 連續 + 連續 = 連續
#check @Continuous.mul     -- 連續 × 連續 = 連續
#check @Continuous.const_mul

於是 \(f(x) = x^2 + 3x + 1\) 的連續性是一行組合：

example : Continuous (fun x : ℝ => x ^ 2 + 3 * x + 1) := by
  apply Continuous.add
  · exact (Continuous.mul continuous_id continuous_id).add
      (Continuous.const_mul continuous_id 3)
  · exact continuous_const

更省事的是多項式專用策略：

example : Continuous (fun x : ℝ => x ^ 2 + 3 * x + 1) := by
  fun_prop   -- 或 continuity / polyrith 風格的自動化

數學上的意義：多項式到處連續，因為它由連續的基本件 用「保持連續的運算」（ \(+,\ \times\) 、複合）組合而成。 這正是 7.2 末尾說的「Tendsto.mul 成立是因為乘法連續」的續篇。

範例二： \(f(x) = 1/x\) 在 \(x \ne 0\) 連續#

\(f(x) = 1/x\) 在整個 \(\mathbb{R}\) 上不是連續函數（ \(0\) 處無定義行為）， 但在任何 \(a \ne 0\) 的一點上是連續的。

數學證明骨架：給 \(\varepsilon > 0\) 。因為 \(a \ne 0\) ， \(|f|\) 在 \(a\) 附近有下界：取 \(\delta_1 = |a|/2\) ， 則 \(|x| \ge |a|/2\) ，故 \(|1/x| \le 2/|a|\) 。再控制

\[ \left|\frac{1}{x} - \frac{1}{a}\right| = \frac{|x - a|}{|x|\,|a|} \le \frac{2\,|x-a|}{|a|^2} \]

取 \(\delta = \min(\delta_1,\ \varepsilon |a|^2 / 4)\) 即可。

在 Lean 中，除法的連續性有現成引理：

#check @Continuous.inv    -- f 連續且不觸零 ⟹ 1/f 連續
#check @ContinuousAt.inv
-- ContinuousAt.inv : ContinuousAt f x → f x ≠ 0 → ContinuousAt (fun y => (f y)⁻¹) x

example (a : ℝ) (ha : a ≠ 0) : ContinuousAt (fun x : ℝ => 1 / x) a := by
  have h : ContinuousAt (fun x : ℝ => x) a := continuous_id.continuousAt
  exact (h.inv (sub_self a ▸ ha)).congr_of_eventuallyEq <| by
    filter_upwards [] with x
    field_simp

（核心是 ContinuousAt.inv：恆等函數在 \(a\) 連續、 \(a \ne 0\) ， 故倒數函數在 \(a\) 連續；congr_of_eventuallyEq 處理 \(1/x\) 與 \(x^{-1}\) 的改寫。若引理簽名不同，用 exact? 尋找 Continuous.div、continuousOn_inv 等近親。）

這個例子教了我們一件事：連續是局部的性質。 \(f = 1/x\) 「整體不連續」只是因為 \(0\) 這一點壞掉； 在定義域的每個好點上它都好好的。Mathlib 因此也有 ContinuousOn f s（在集合 \(s\) 上連續）的版本：

example : ContinuousOn (fun x : ℝ => 1 / x) {x : ℝ | x ≠ 0} := by
  intro x hx
  exact (continuous_id.continuousAt (a := x)).inv (ne_of_apply_ne _ hx) |>.congr_of_eventuallyEq <| by
    filter_upwards [] with y; field_simp

中間值定理預告#

連續函數最重要的定理之一是中間值定理（IVT）：

若 \(f\) 在 \([a, b]\) 上連續，且 \(f(a) < y < f(b)\) ， 則存在 \(c \in (a, b)\) 使 \(f(c) = y\) 。

直覺：連續函數的圖形是一筆畫，從 \(f(a)\) 走到 \(f(b)\) 必然穿過中間的每個高度。 注意證明本質上用到實數完備性（7.1 的 supremum！）—— 在 \(\mathbb{Q}\) 上不成立：考慮 \(f(x) = x^2\) 在 \([1, 2]\) 上取 \(y = 2\) ， 無有理數解。

Mathlib 中的形式：

#check @IntermediateValue.intermediate_value_Icc
-- 或常見名稱：exists_mem_Icc_of_continuous_of_mem_Icc

完整敘述與證明我們留到下一章（需要區間拓樸的準備）， 這裡先記住：IVT 是完備性公理的果實。

Continuous.comp：複合保持連續#

定理： \(g \circ f\) 連續，若 \(f\) 連續且 \(g\) 連續。

直覺（用 ε-δ 語言）：要讓 \(g(f(x))\) 靠近 \(g(f(a))\) 到 \(\varepsilon\) 以內， 先用 \(g\) 的連續性取得 \(\delta_1\) （控制 \(f(x)\) 與 \(f(a)\) 的距離）， 再用 \(f\) 的連續性取得 \(\delta\) （控制 \(x\) 與 \(a\) 的距離）。兩層緩衝疊起來。

#check @Continuous.comp
-- Continuous.comp : Continuous g → Continuous f → Continuous (g ∘ f)

#check @ContinuousAt.comp

example : Continuous (fun x : ℝ => Real.sin (x ^ 2 + 1)) := by
  exact Real.continuous_sin.comp (by fun_prop)

架構總覽——連續性像積木一樣層層堆疊：

基本件：continuous_const、continuous_id、Real.continuous_sin、…
運算：  Continuous.add  .mul  .neg  .inv  .comp
組合：  任意「由連續基本件用連續運算造出」的函數都連續

這種「生成式證明」（proof by generation）是 Mathlib 處理連續性的日常手法， 也是 fun_prop / continuity 這些自動化 tactic 的原理。

小結與練習#

本節要點：

  1. ε-δ 定義：對手給 \(\varepsilon\) ，我們給 \(\delta\) ；輸入小擾動不得造成輸出突跳。
  2. Mathlib 的 Continuous 用「開集的原像是開集」定義，與 ε-δ 等價且更一般。
  3. ContinuousAt f a 是一點版本，等價於 Tendsto f (𝓝 a) (𝓝 (f a))； Metric.continuousAt_iff 是回 ε-δ 的橋。
  4. 多項式連續由 continuous_const、continuous_id、.add、.mul 組合而成； \(1/x\) 在 \(x \ne 0\) 連續由 ContinuousAt.inv 給出。
  5. Continuous.comp：複合保持連續，ε-δ 直覺是「兩層緩衝」。
  6. 中間值定理預告：連續 + 完備性 ⟹ 穿過所有中間值。

練習：

  1. 用 Metric.continuousAt_iff 手寫 ε-δ，證明 \(f(x) = 2x\) 在任意點 \(a\) 連續 （提示：取 \(\delta = \varepsilon / 2\) ）。
  2. 用 Continuous.mul 與 Continuous.neg 證明 \(f(x) = -x^3\) 連續。
  3. 證明 \(f(x) = 1 / (x^2 + 1)\) 在整個 \(\mathbb{R}\) 上連續 （提示：Continuous.inv 需要驗證分母不為零，by nlinarith 可幫忙）。
  4. 說明 \(f(x) = |x|\) 在 \(0\) 點連續，但 \(g(x) = x / |x|\) （ \(x \ne 0\) ）無法延拓成 \(0\) 點連續的函數；各用一句 ε-δ 語言解釋。
  5. 用 Continuous.comp 證明：若 \(f\) 連續，則 \(f \circ f\) 連續； 並在 Lean 中對 \(f(x) = \sin x\) 驗證。
  6. （預習）查一下 Real.continuous_sqrt，思考為什麼 \(\sqrt{x}\) 在 \(x = 0\) 是連續「但不是用兩側 ε-δ 直接給出」的有趣例子。