📐 Proposition IX.1.2（Hausdorff ⟺ 対角集合が閉）／Lemma IX.1.3・Corollary IX.1.4
- 📐 Proposition IX.1.2（Hausdorff ⟺ 対角集合が閉）／Lemma IX.1.3・Corollary IX.1.4 #Card
- Hausdorff性を対角集合の閉性で言い換えると。連続写像の一致集合について何が言えるか。
$$\xi \text{ が Hausdorff} \iff \triangle(X)={(x,x):x\in X} \text{ が } \xi\times\xi\text{-閉}.$$
証明: $(x_0,x_1)\in\lim_{\xi\times\xi}\mathcal{G}$ は $x_0,x_1\in\lim_\xi\mathcal{F}$（共通の $\mathcal{F}$）と同値（射影経由）なので、対角閉性はまさに Hausdorff の定義。恒等写像 $i\in C(\xi,\xi)$ のグラフが $\xi\times\xi$-閉 $\iff$ $\xi$ が Hausdorff。
Lemma IX.1.3（一致集合の閉性）: $f,g\in C(\xi,\theta)$、$\theta$ が Hausdorff なら ${f=g}$ は $\xi$-閉（対角積写像 $f\triangle g$ の連続性経由）。
Cor IX.1.4: $f_0,f_1\in C(\xi,\tau)$（$\tau$ Hausdorff）が $\xi$-稠密集合上で一致するなら $f_0=f_1$（一意接続の原理）。
本ノート RoyalRoad.ChapterIX.prop_IX_1_2（Mathlib t2_iff_isClosed_diagonal を直接引用、Notes/ChapterIX.lean、lake build 済み）