📐 Theorem X.4.15（Baire category theorem）／Corollary X.4.16
- 📐 Theorem X.4.15（Baire category theorem）／Corollary X.4.16 #Card
- ベールのカテゴリー定理の主張と証明の骨子、閉集合による合併への言い換えは。
Thm X.4.15: 完備距離化可能空間で、可算個の開稠密集合の交わりは稠密。
証明の骨子（縮小球の入れ子構成）: 各 $Q_n$（開稠密）に対し帰納的に $x_n,r_n\to0$ を選び $\operatorname{cl}B(x_{n+1},r_{n+1})\subset Q_n\cap B(x_n,r_n)$。cards/topology/cantor-theorem-complete-metric（Cantor の定理）から $\bigcap_n\operatorname{cl}B(x_n,r_n)\neq\emptyset\subset\bigcap Q_n$。
Cor X.4.16（閉集合版、対偶）: $X=\bigcup_{n<\omega}F_n$（$F_n$ 閉）なら、ある $n$ で $\operatorname{int}F_n\neq\emptyset$（$Q_n:=X\setminus F_n$ に適用）。
「完備距離化可能空間は自分自身の中で第一類（meager）にならない」（cards/topology/density-related-terms の言葉で）という定理。$\mathbb{Q}$ の非完備距離化可能性（cards/topology/completely-metrizable-topology）はこの定理の直接の帰結。測度論のベール性・零集合と第一類集合の対比の位相的な基礎。
dense_iInter_of_isOpen（BaireSpace 型クラス）。
本ノート RoyalRoad.ChapterX.thm_X_4_15 / cor_X_4_16（開稠密版＋閉集合版の系、Notes/ChapterX.lean、lake build 済み）