$T_0/T_1/T_2$ を位相の言葉に翻訳する（Proposition IX.1.1）
- $T_0/T_1/T_2$ を位相の言葉に翻訳する（Proposition IX.1.1） #Card
- cards/topology/t0-convergence・cards/topology/free-convergence-t1・cards/topology/hausdorff-convergence-t2（第III章、任意の収束向け）が位相の場合にどう具体化されるか。
- $T_0$: 異なる2点の一方だけを含む開集合が存在。
- $T_1$（free）: 各単集合が閉（Definition III.1.13 から直接）。
- $T_2$（Hausdorff）: $\mathcal{N}\xi(x_0)#\mathcal{N}\xi(x_1)\implies x_0=x_1$。
Prop IX.1.1: 位相 $\xi$ が Hausdorff $\iff$ $x_0\neq x_1$ に対し disjoint な開集合 $O_0\ni x_0,\ O_1\ni x_1$ が存在（近傍フィルターが開集合の基を持つことから直接）。
遺伝性: Hausdorff・$T_1$ は任意の収束で遺伝的（Prop III.1.16）、位相性は部分位相で保たれる（Cor VII.3.8）ので、Hausdorff 位相・free 位相の部分空間は同じ性質を持つ。
Meaning
Section titled “Meaning”IX.1 冒頭の狙いは、収束論で導入した $T_0/T_1/T_2$ を古典位相の語彙へ「戻す」ことにある。とくに Hausdorff 性は、開集合の分離条件と近傍フィルターの mesh 条件の同値として提示され、分離公理を点の直感と filter 計算の両方で扱える形に整える。
出典:
refs/math/topology/royal-road-to-topology/pdfs/chp9-2024-topological-concepts.pdfp.162
本ノート RoyalRoad.ChapterIX.prop_IX_1_1（Hausdorff の3条件 TFAE: T2Space ⟺ disjoint 開集合対 ⟺ 近傍フィルターの mesh から一致）・prop_IX_1_hierarchy（$T_4⟹T_3⟹T_2⟹T_1⟹T_0$）・t1_iff_singleton_closed（$T_1$ ⟺ 単集合閉）、Notes/ChapterIX.lean、lake build 済み）