手筋: 減少閉集合列の非空交叉（FIP／Cantor 条件）で存在を捕まえる (Ex IX.5.10 / IX.5.11 / X.10.1 / X.10.8 / X.10.9)
- 手筋: 減少閉集合列の非空交叉（FIP／Cantor 条件）で存在を捕まえる (Ex IX.5.10 / IX.5.11 / X.10.1 / X.10.8 / X.10.9) #Card
- コンパクト性・可算コンパクト性を「開被覆」でなく閉集合の交叉として使い、「下限を達成する点」「一様収束の閾値」「例外集合が空」といった存在を一撃で出す共通骨格は？
核: コンパクト性は開被覆の双対で「閉集合の交叉が空でない」。証明したい存在を「ある減少閉列 $\bigcap_n C_n\neq\emptyset$ の一点」として設計する。
3つの顔（すべて補集合＋ド・モルガン＋対偶で同値）:
- FIP 版（Ex IX.5.10）: $\tau$ コンパクト $\iff$ 有限交叉性を持つ閉集合族は $\bigcap\neq\emptyset$。開被覆 $\mathcal{P}\leftrightarrow$ 閉族 $\mathcal{D}=\mathcal{P}^c$、$\bigcup=X\leftrightarrow\bigcap=\emptyset$。
- Cantor 条件（Ex IX.5.11）: $\tau$ 可算コンパクト $\iff$ 空でない減少閉列 ${C_n}$ は $\bigcap_n C_n\neq\emptyset$。可算開被覆 → 増加開列 $Q_n:=\bigcup_{k\le n}O_k$ → 減少閉列 $C_n:=X\setminus Q_n$。
- 対偶（消滅版）: $\bigcap_n C_n=\emptyset$（減少閉列）$\Rightarrow$ ある $n_0$ で $C_{n_0}=\emptyset$。
設計テンプレート（証人となる減少閉列を作る）:
- 下限の達成（Ex X.10.1）: 閾値 $r_n\downarrow\inf f$、レベル集合 $C_n:={f\le r_n}$（下半連続で閉・減少）→ $\bigcap\neq\emptyset$ が最小点。
- Dini の一様収束（Ex X.10.9）: 誤差 $F_n:={f-f_n\ge\varepsilon}$（連続で閉・単調で減少）、各点収束で $\bigcap=\emptyset$ → 対偶で有限段消滅＝一様収束。
- ベール双対（Ex X.10.8）: $X=\bigcup_n F_n$（閉の可算合併）に完備距離化可能性でベール（Cor X.4.16）→ ある $F_n$ が内点を持つ。「例外集合 $L$ が完全集合＋ベール ⟹ $L=\emptyset$」の追い込みも同系譜。
射程: 古典的 Cantor の共通部分定理（$\mathbb{R}$ の縮小閉区間）の抽象形。cards/topology/finite-intersection-property-compactness・cards/topology/cantor-condition-countably-compact・cards/topology/lsc-attains-infimum-countably-compact・cards/topology/dini-theorem・cards/topology/baire-category-theorem を貫く。「証明したい存在を減少閉列の交叉として実装する」のが共通の発想。ワイエルシュトラス最大値定理・単調収束定理（測度論）の位相的骨格。
Mathlib: IsCompact.nonempty_iInter_of_directed（有向な閉集合族の非空交叉）、IsCompact.elim_finite_subcover、IsCompact.exists_isMinOn（下半連続の最小達成 LowerSemicontinuous）、Dini は tendstoUniformly 系、Baire は dense_iInter_of_isOpen。