古典的な位相空間の定義（VII.7 Supplement）

• 古典的な位相空間の定義（VII.7 Supplement） #Card
  • 開集合系 $(X,\mathcal{O})$ による古典的定義と、それが定める収束 $\tau_\mathcal{O}$ は。

Back

古典的定義: $\mathcal{O} \subset 2^X$ が $$\emptyset, X \in \mathcal{O}, \quad \mathcal{A}\subset\mathcal{O}\implies\bigcup\mathcal{A}\in\mathcal{O}, \quad \mathcal{A}\subset_{\mathrm{fin}}\mathcal{O}\implies\bigcap\mathcal{A}\in\mathcal{O}$$ を満たすとき $(X,\mathcal{O})$ を位相空間、$\mathcal{O}$ を開集合系と呼ぶ。対応する収束: $$x \in \lim{}{\tau\mathcal{O}} \mathcal{F} \iff \mathcal{O}(x) \subset \mathcal{F}. \tag{VII.7.1}$$

Proposition VII.7.1: $\mathcal{O}{\tau\mathcal{O}} = \mathcal{O}$（構成が往復して元に戻る）— 本書の「収束による位相の定義」と「開集合系による古典的定義」が完全に同値であることの正当化。Mathlib の TopologicalSpace はこちら（開集合系）を出発点に採用。

Meaning

VII.7 Supplement の冒頭で著者は、伝統的に位相は開集合系または閉包演算で定義されると述べる（Sierpiński, Kuratowski, Engelking 等を引用）。開集合系 $(X,\mathcal{O})$ から $x \in \lim_{\tau_\mathcal{O}} \mathcal{F} \iff \mathcal{O}(x) \subset \mathcal{F}$ で収束を定め、Proposition VII.7.1 により $\mathcal{O}{\tau\mathcal{O}} = \mathcal{O}$ —— 古典的定義と本書の収束言語が往復する。

出典: refs/math/topology/royal-road-to-topology/pdfs/chp7-2024-topological-structures.pdf p.145–146

Lean

TopologicalSpace（isOpen_univ, IsOpen.union, IsOpen.inter が公理）。