9.1 拓樸空間#

本節目標#

• 理解為什麼要「丟掉距離」：從度量空間抽象到拓樸空間的動機。
• 掌握拓樸的三條公理：任意並、有限交、空集與全集。
• 閱讀 Mathlib 的 class TopologicalSpace 原始定義，理解 IsOpen 是 primitive。
• 建立 nhds（鄰域 filter）的直覺。
• 複習 Continuous 在拓樸語言下的定義。

從距離出發：我們真正用到的是什麼？#

在前面的章節裡，我們談過實數的極限與連續。回頭檢視那些定義——極限的 \(|x - a| < \varepsilon\) 、連續的 \(\varepsilon\) - \(\delta\) 、柯西列的 \(|x_m - x_n| < \varepsilon\) ——你會發現它們都依賴「距離」。但仔細想想，這些定義真正用到的，其實只有一個概念：開區間（或開球）

「 \(x\) 靠近 \(a\) 」翻譯成集合語言就是「 \(x\) 落在某個開集合裡」。既然如此，我們可以大膽地問：

如果我不給你距離，只給你「哪些集合算開的」，極限與連續的理論還能撐起來嗎？

答案是：可以，而且撐得更好。這就是點集拓樸（point-set topology）的出發點。

為什麼要丟掉距離？#

1. 一般化：許多空間天生沒有自然的距離，卻有自然的「鄰近」概念。例如函數空間上的「逐點收斂」，無法由任何距離生成，卻可以由拓樸描述。
2. 本質萃取：定理證明中若只用到開集的性質，就不該假設距離存在；抽象讓定理自動適用於所有實例。
3. 看清結構：丟掉距離後，剩下的骨架（開集如何併、交）正是分析學真正依賴的部分。

這和本書一路走來的方法論一致：從例子萃取公理，再用公理重建理論。Peano 公理化自然數（第 4 章），完備有序體公理化實數，現在輪到公理化「鄰近」。

拓樸公理#

定義（拓樸）。設 \(X\) 是一個集合。 \(X\) 上的一個拓樸（topology）是指 \(X\) 的若干子集構成的族 \(\mathcal{T}\) （其中的元素稱為開集），滿足：

1. \(\varnothing \in \mathcal{T}\) 且 \(X \in \mathcal{T}\) ；
2. （任意並）若 \(\{U_i\}_{i \in I} \subseteq \mathcal{T}\) ，則 \(\bigcup_{i \in I} U_i \in \mathcal{T}\) ；
3. （有限交）若 \(U_1, \dots, U_n \in \mathcal{T}\) ，則 \(\bigcap_{k=1}^{n} U_k \in \mathcal{T}\) 。

\((X, \mathcal{T})\) 稱為一個拓樸空間。

為什麼是這三條？直接從開區間的經驗讀出來：開區間的任意並還是開的（黏起來不會冒出「含在內的端點」）；有限個開集的交還是開的，但這裡「有限」不可省略—— \(\bigcap_{n=1}^{\infty} (-\tfrac{1}{n}, \tfrac{1}{n}) = \{0\}\) ，單點集不是開的；空並是 \(\varnothing\) 、空交是 \(X\) ，所以第 1 條其實是空指標下的特例，習慣上獨立列出。

注意「並可以無限、交只能有限」這個不對稱，是整個點集拓樸的靈魂。後面的緊緻性（9.2 節）正是為了補償「有限交」的限制而生的概念。

Mathlib 的 TopologicalSpace#

Lean 不用「一族的集合」來定義拓樸，而是用一個更經濟的編碼：直接告訴 Lean 哪些集合是開的。定義原文（節錄自 Mathlib）：

/-- A topology on `α`. -/
class TopologicalSpace (α : Type u) where
  /-- `IsOpen s` means `s` is open in `α`. -/
  IsOpen : Set α → Prop
  isOpen_univ : IsOpen Set.univ
  isOpen_inter : ∀ s t, IsOpen s → IsOpen t → IsOpen (s ∩ t)
  isOpen_sUnion : ∀ s, (∀ t ∈ s, IsOpen t) → IsOpen (⋃₀ s)

幾個值得注意的點：

• IsOpen 是 primitive：拓樸不是「一個集合族」的資料結構，而是一個 predicate IsOpen : Set α → Prop，配上三條生成公理；任意並的公理用 ⋃₀（集合的集合之並）。
• 有限交只需二元版本 isOpen_inter：兩兩交封閉，歸納可得任意有限交。
• 「包含 \(\varnothing\) 」在這個編碼下是自由的：IsOpen ∅ 由 ∅ = ⋃₀ ∅（空並）推出。

實務上 Lean 用 instance 隱式取得拓樸，直接寫 IsOpen s 即可。

範例一：離散拓樸#

離散拓樸：宣告每一個子集都是開的。

example : TopologicalSpace ℕ := ⊥   -- 離散拓樸是拓樸格中的最小元

離散空間中每個點自己就是開集，「鄰近」的資訊量為零。在離散拓樸下，所有函數都連續（開集的原像還是開集，因為所有集合都開）；收斂只有平凡解： \(x_n \to a\) 若且為若「最終恆等於 \(a\) 」。離散拓樸確實可由離散度量 \(d(x,y) = [x \neq y]\) 生成，但拓樸語言不必提到這個度量。

範例二： \(\mathbb{R}\) 的標準拓樸#

實數線的標準拓樸： \(U \subseteq \mathbb{R}\) 是開的，若且為若

這正是由度量 \(d(x,y) = |x - y|\) 生成的拓樸。Mathlib 中由度量自動生成拓樸：

-- Real 有 instance：MetricSpace → TopologicalSpace
-- 標準拓樸下，開區間是開集
example : IsOpen (Set.Ioo (0:ℝ) 1) := isOpen_Ioo

關鍵定理：由度量生成的拓樸滿足三條公理（Mathlib 中這是 MetricSpace.toTopologicalSpace instance 的內容）。也就是說：每個度量空間都是拓樸空間，但反之不然。

口訣：度量告訴你「多近」，拓樸只告訴你「附近有誰」。丟掉數字，留下形狀。

鄰域 filter：nhds#

與其問「哪些集合開」，分析學常常換個角度問「點 \(x\) 的附近有什麼」。這就是鄰域：

在 Mathlib 中， \(x\) 的所有鄰域組成一個 filter：nhds x。filter 的直覺是「夠大的集合」之收藏，滿足上封閉與有限交封閉；nhds x 就是「在 \(x\) 附近」的集合。一個方便的刻劃：

theorem mem_nhds_iff {s : Set α} {a : α} :
    s ∈ nhds a ↔ ∃ t, t ⊆ s ∧ IsOpen t ∧ a ∈ t

也就是說：「 \(s\) 在 \(a\) 的鄰域 filter 裡」 \(\iff\) 「 \(s\) 包含一個過 \(a\) 的開集」。用 filter 語言，極限與連續都可以重新表達： \(x_n \to a\) 即「對每個 \(N \in \text{nhds}\ a\) ，序列最終落在 \(N\) 中」；連續則見下節回顧。

連續的拓樸定義（回顧）#

在度量世界，連續是 \(\varepsilon\) - \(\delta\) ： \(\forall \varepsilon > 0,\ \exists \delta > 0,\ |x - a| < \delta \implies |f(x) - f(a)| < \varepsilon\) 。抽象化之後：

定義（連續）。 \(f : X \to Y\) 在 \(a\) 點連續 \(\iff\) 對 \(f(a)\) 的每個鄰域 \(V\) ，原像 \(f^{-1}(V)\) 是 \(a\) 的鄰域。全域連續 \(\iff\) 每個開集的原像是開集。

Mathlib 中的定義：

def Continuous [TopologicalSpace α] [TopologicalSpace β] (f : α → β) : Prop :=
  ∀ s, IsOpen s → IsOpen (f ⁻¹' s)

在濾子語言下，連續的刻劃是 ContinuousAt f a ↔ Filter.Tendsto f (nhds a) (nhds (f a))，與原像開版本等價，而 原像開 版本最適合抽象：完全不提點、不提 \(\varepsilon\) ，只談開集之間的映射。這是 9.2、9.3 節所有定理的敘述基礎。

小結與練習#

本節重點：

練習：

1. 證明：在離散拓樸下，任意函數 \(f : X \to Y\) 都是連續的（ \(Y\) 任意）。
2. 證明： \(\bigcap_{n=1}^{\infty} (-\tfrac{1}{n}, \tfrac{1}{n}) = \{0\}\) ，並說明這為何不違反有限交公理。
3. 在 Lean 中查閱 IsOpen 與 nhds 的定義（#check @IsOpen、#check @mem_nhds_iff），確認本節引用的敘述。
4. 思考題：如果允許可數交也封閉，會得到什麼結構？（這是 Borel 階層的起點。）