Compactness

収束 $\xi$ が compact であるとは、$X$ 上の全てのフィルターが adherent（$\operatorname{adh}_\xi \mathcal{H} \neq \emptyset$）であること。開被覆の有限部分被覆による古典的な定義は、この「フィルターは必ずどこかへ集まる」という性質を位相へ翻訳した帰結として後から出てくる——compact はまず filter の振る舞いとして定義される。この見方は測度論の緊密性（tightness）や関数解析の弱コンパクト性（Banach–Alaoglu）へそのまま一般化する。

書籍別カード

• Royal Road to Topology: cards/topology/compact-convergence-definition — 全フィルター adherent／同値な超フィルター条件 cards/topology/lem-viii-1-2-ultrafilter-adherence。自作形式化 RoyalRoad.ChapterVIII.thm_VIII_3_compact_tfae（CompactSpace ⟺ 全 proper filter adherent ⟺ 全超フィルター収束 ⟺ 有限部分被覆、TFAE, lake build 済み）。

用語対応（terminology-map）

30_Concepts/topology-terminology-map（PR #168、未マージ）「コンパクト性・被覆・連続」節に該当行あり:

compact（cards/topology/compact-convergence-definition） | compact | IsCompact / CompactSpace

同節には compactoid set（cards/topology/compactoid-set、相対コンパクト様の一般化）の行もあり、こちらは Mathlib 本体に対応物がない。