📐 Proposition IX.3.3・IX.3.4（Hausdorff コンパクト ⟹ 正則 ⟹ 正規）
- 📐 Proposition IX.3.3・IX.3.4（Hausdorff コンパクト ⟹ 正則 ⟹ 正規） #Card
- Hausdorff かつコンパクトな位相が自動的に regular・normal になることの証明の共通パターンは。
$\xi$ が Hausdorff かつコンパクトなら regular（Prop IX.3.3）かつ normal（Prop IX.3.4）。
共通の証明パターン（「点と閉集合」または「2閉集合」の分離）: Hausdorff 性から各 $x\in C$（コンパクト集合の各点）ごとに disjoint な開集合対が取れる → $C$ のコンパクト性で有限本に間引く → 有限個の共通部分を取れば残り側の近傍が構成できる。
$$\bigcap_{x\in F}P_x \in \mathcal{O}\xi(x_0)\ \text{（有限交叉なので開）}, \qquad \bigcup{x\in F}O_x \supset C\ \text{（有限部分被覆）}.$$
「コンパクト性 = 無限個の分離条件を有限個に圧縮する道具」という直感がそのまま証明になっている。コンパクト・ハウスドルフ空間が自動的に正規空間になるという、位相空間論で最重要な事実の一つ。
本ノート RoyalRoad.ChapterIX.prop_IX_3_3 / prop_IX_3_4（Hausdorff コンパクト ⟹ 正則・正規、inferInstance で得られる Mathlib のインスタンス、Notes/ChapterIX.lean、lake build 済み）