📐 Proposition VIII.3.3（連続写像はコンパクト性を保つ）
- 📐 Proposition VIII.3.3（連続写像はコンパクト性を保つ） #Card
- $f\in C(\xi,\tau)$ かつ $A$ が $\xi$-compact なら $f(A)$ について何が言えるか。
$$f \in C(\xi,\tau),\ A \text{ が } \xi\text{-compact} \implies f(A) \text{ が } \tau\text{-compact}.$$
証明の骨子: $\mathcal{U}\in\beta f(A)$ を取ると $f^-[\mathcal{U}]#A$、その細分の超フィルター $\mathcal{W}\in\beta(f^-[\mathcal{U}]\vee A)$ に対し $A$-コンパクト性から $A#\lim_\xi\mathcal{W}$。連続性で $f(A)#\lim_\tau f[\mathcal{W}]$。一方 $f[\mathcal{W}]\geq\mathcal{U}$ かつ $\mathcal{W}$ 超フィルターなので $f[\mathcal{W}]\approx\mathcal{U}$（同値）— 従って $\mathcal{U}$ も収束。
古典的な「コンパクト集合の連続像はコンパクト」の証明を、超フィルターの押し出し一本で処理する典型例。
IsCompact.image（Continuous.isCompact_image とも）。
本ノート RoyalRoad.ChapterVIII.prop_VIII_3_3（Notes/ChapterVIII.lean、lake build 済み）