📐 Exercise IX.5.10（コンパクト性の有限交叉性質 (FIP) による特徴づけ）
- 📐 Exercise IX.5.10（コンパクト性の有限交叉性質 (FIP) による特徴づけ） #Card
- コンパクト性を「開被覆」でなく「閉集合族」の言葉で言い換えると。
位相 $\tau$ がコンパクト $\iff$ 有限交叉性質（finite intersection property, FIP）を持つ任意の閉集合族は空でない交わりを持つ: $$\forall \mathcal{D}\subset\mathcal{C}_\tau,\ \left(\forall \mathcal{D}0\subset{\mathrm{fin}}\mathcal{D},\ \bigcap\mathcal{D}_0\neq\emptyset\right) \implies \bigcap\mathcal{D}\neq\emptyset.$$
導出: 開被覆の定義 $\bigcup\mathcal{P}=X$（有限部分被覆なし）を $\mathcal{D}:=\mathcal{P}^c$（補集合の族）に双対化するだけ（ド・モルガンの法則、$\bigcap\mathcal{D}=\emptyset \iff \bigcup\mathcal{P}=X$）。
cards/topology/finite-subcover-characterization（Cor VIII.3.8）の対偶版。超フィルターの言葉（cards/topology/compact-convergence-definition）・開被覆の言葉・FIP の言葉、3つの同値な顔を持つのがコンパクト性。
本ノート RoyalRoad.ChapterIX.exercise_IX_5_10（isCompact_of_finite_subfamily_closed の対偶方向を含む両向き証明、Notes/ChapterIX.lean、lake build 済み）