📐 Theorem X.9.14（Urysohn の距離化定理）

• 📐 Theorem X.9.14（Urysohn の距離化定理） #Card
  • free・正則・可算 weight な位相が距離化可能であることの証明の骨子は。

Back

Urysohn 距離化定理: free（$T_1$）・regular・可算 weight（second countable）な位相は距離化可能。

証明の骨子: cards/topology/regular-countable-weight-normal（Prop IX.3.11）から正規性を確保 → 可算 base $\mathcal{B}$ のペア $(B,W)$（$\operatorname{cl}B\subset W$）ごとに cards/topology/urysohn-lemma で分離関数 $f_{B,W}$ を取る（可算個）→ この可算族が free 性から点と閉集合を分離 → cards/topology/tikhonov-cube-embedding Cor X.9.11 で 可算次元の Tikhonov 立方体 $I^{\aleph_0}$ に埋め込み（cards/topology/countable-product-metrizable Prop X.3.8 でこれは距離化可能）。

正則・第2可算・$T_1$ という一見弱い3条件だけから、距離という強い構造が一意に（同値の意味で）決まる — 位相空間論の金字塔的定理。$T_{3\frac12}$ を経由せず regular で十分な点が意外（第2可算性が正則性を関数的正則性まで自動的に強化するため、cards/topology/regular-countable-weight-normal の効能）。

Meaning

Theorem X.9.14 は、関数的位相論の流れ（Urysohn 補題での関数分離 → 可算関数族による埋め込み）を「距離化可能」という古典的結論へ着地させる章の到達点として置かれる。著者の観点では、距離化は公理を直接仮定するのでなく、位相が持つ関数分離能力の帰結として現れる。

出典: refs/math/topology/royal-road-to-topology/pdfs/chp10-2024-functional-study-of-topologies.pdf p.228–229

Lean

UrysohnMetrizable 系（TopologicalSpace.PseudoMetrizableSpace の第2可算 + 正則からの導出）。

本ノート RoyalRoad.ChapterX.thm_X_9_14（$T_1$ + 正則 + 第2可算 ⟹ MetrizableSpace、inferInstance、Notes/ChapterX.lean、lake build 済み）