手筋: フィルターの押し出し／引き戻しで連続像の性質を運ぶ (Cor VIII.1.10 / 可算コンパクト・Lindelöf 保存 / Prop VIII.3.3)
- 手筋: フィルターの押し出し／引き戻しで連続像の性質を運ぶ (Cor VIII.1.10 / 可算コンパクト・Lindelöf 保存 / Prop VIII.3.3) #Card
- 「連続写像 $f$ は adherence／コンパクト性／可算コンパクト性／Lindelöf 性を像へ保つ」型の主張を、公式暗記なしで定義から一撃で示す手筋は？
核: 証人フィルターを $f$ で運ぶ。2つの補題だけを使う。
- 連続性は $\lim$ を保つ: $x\in\lim_\xi\mathcal{F}\implies f(x)\in\lim_\tau f[\mathcal{F}]$（cards/topology/continuous-map）。
- 像は mesh を保つ: $F\cap H\neq\emptyset\implies f[F]\cap f[H]\neq\emptyset$（$f[F\cap H]\subset f[F]\cap f[H]$）。ゆえに $\mathcal{F}#\mathcal{H}\implies f[\mathcal{F}]#f[\mathcal{H}]$。
adh の保存（Cor VIII.1.10）: $x\in\operatorname{adh}\xi\mathcal{H}$ を与える証人 $\mathcal{F}#\mathcal{H},\ x\in\lim\xi\mathcal{F}$ を取り、1・2 で $f(x)\in\operatorname{adh}_\tau f[\mathcal{H}]$。
コンパクト性階層の連続像による保存（テンプレート）: $B=f(A)$ 上のフィルター $\mathcal{G}$（該当クラス）に対し
- 逆像 $\mathcal{H}:=f^{-1}[\mathcal{G}]$ を作る → $A$ と mesh、
- $A$ の（可算）コンパクト性で $x_0\in\operatorname{adh}_\xi\mathcal{H}\cap A$、
- Cor VIII.1.10 と $f[\mathcal{H}]\geq\mathcal{G}$・adh の反単調性 (VIII.1.3) で $f(x_0)\in\operatorname{adh}_\tau\mathcal{G}\cap B$。
射程: compact（全フィルター）・countably compact（可算基）・Lindelöf（可算完備）はすべて連続写像で保存——保存の可否は「$f^{-1}$ がそのフィルタークラスを保つか」に尽きる（逆像は可算基を可算基に、可算交叉と可換ゆえ可算完備性を可算完備性に写す）。積で保存されない事実（逆像1本で済まない）との対比が鮮明。測度論では「可測写像による押し出し測度・分布の像」に同じ骨格。
Mathlib: Filter.map / Filter.comap、Continuous.isCompact_image（= IsCompact.image）、Filter.Tendsto。可算性クラスは Filter.IsCountablyGenerated が comap で保たれること。