📐 Proposition X.3.8（可算積の距離化可能性）／Example X.3.9（Baire space）
- 📐 Proposition X.3.8（可算積の距離化可能性）／Example X.3.9（Baire space） #Card
- 可算個の距離化可能位相の積が距離化可能であることの構成的証明と、Baire 空間の定義は。
Prop X.3.8: 各 $\tau_n$ が距離 $d_n$（$\leq1$ と仮定してよい）で距離化可能なら、積位相 $\prod_n\tau_n$ は $$d(f,g) := \sum_{n=0}^\infty \frac{1}{2^n}d_n(f(n),g(n))$$ で距離化可能（積収束と $d$-収束が一致することを $\varepsilon/2$ 論法の裾切りで確認）。
Example X.3.9（Baire 空間 $\mathbb{B}$）: $\mathbb{N}^\mathbb{N}$ 上、離散位相 $\iota_\mathbb{N}$ の可算積。$(\varphi_k)_k\to\varphi$ ⟺ 各座標が有限段で真の値に一致（離散距離 $\imath_X$ を使い上記の積距離で距離化）。
測度論への視線: Baire 空間は記述集合論・確率論のパス空間（無限試行列の空間）の標準模型。積測度の台となる位相構造がここで確立される。
Pi.metricSpace、Metric.baireSpace（記述集合論分野に相当）。