📐 Proposition VIII.3.16（Hausdorff空間ではコンパクト⟹閉）
- 📐 Proposition VIII.3.16（Hausdorff空間ではコンパクト⟹閉） #Card
- Hausdorff 収束空間でコンパクト部分集合が閉集合になることの証明の鍵は。
$\xi$ が Hausdorff、$C$ が $\xi$-compact ならば $C$ は $\xi$-閉。
証明: $\mathcal{F}$ を $C$ 上のフィルターで ${x}=\lim_\xi\mathcal{F}$（$x\in X$）とする。$C$ のコンパクト性から $C\cap\operatorname{adh}\xi\mathcal{F}\neq\emptyset$。Hausdorff 性と $\lim\xi\mathcal{F}\neq\emptyset$ より cards/topology/hausdorff-adherence-equals-limit（Prop VIII.1.3）から $\operatorname{adh}\xi\mathcal{F}=\lim\xi\mathcal{F}={x}$。よって $x\in C$、すなわち $C$ の外の収束フィルターが存在しない＝$C$ が閉。
cards/topology/compact-not-closed-example（Example VIII.3.15）の $$_0$ が Hausdorff でないことがまさにこの定理の適用外である理由。
IsCompact.isClosed（Hausdorff 前提、[T2Space]）。
本ノート RoyalRoad.ChapterVIII.prop_VIII_3_16（Notes/ChapterVIII.lean、lake build 済み）