📐 Theorem VIII.3.4（Tikhonov：積のコンパクト性）
- 📐 Theorem VIII.3.4（Tikhonov：積のコンパクト性） #Card
- 収束の積 $\prod \Xi$ がコンパクトであることの必要十分条件と、証明のフィルター論的核は。
$$\prod_{i\in I} \xi_i \text{ がコンパクト} \iff \xi_i \text{ が各 } i \text{ でコンパクト}.$$
$(\Rightarrow)$: 射影 $p_i \in C(\xi,\xi_i)$ に cards/topology/continuous-image-compact を適用（全射像の一種）。
$(\Leftarrow)$: $\mathcal{U}$ を積の超フィルターとすると各 $p_i[\mathcal{U}]$ は $X_i$ 上の超フィルター（超フィルターの押し出しは超フィルター）。各 $\xi_i$ のコンパクト性から $x_i\in\lim_{\xi_i}p_i[\mathcal{U}]$ を選び $\gamma(i):=x_i$ とすると $\gamma\in\lim_\xi\mathcal{U}$ — 各成分の極限点を選ぶだけで積の収束点が構成できる（選択公理は超フィルターの存在に既に埋め込まれている）。
古典的 Tychonoff の定理そのもの。フィルター・超フィルターの言語だと証明が数行に潰れる好例。
isCompact_pi_infinite / CompactSpace.prod / Pi.compactSpace。証明は Mathlib でも超フィルター（Ultrafilter）経由。
本ノート RoyalRoad.ChapterVIII.thm_VIII_3_4（CompactSpace (∀ i, Z i) ↔ ∀ i, CompactSpace (Z i)、各成分非空前提の iff 版、Notes/ChapterVIII.lean、lake build 済み）