📐 Theorem X.4.5（Cantor：完備性の縮小閉集合列による特徴づけ）
- 📐 Theorem X.4.5（Cantor：完備性の縮小閉集合列による特徴づけ） #Card
- 距離の完備性を、直径が0に縮む減少閉集合列の言葉で言い換えると。
距離空間が complete $\iff$ 直径が0に収束する減少非空閉集合列は常に空でない交わりを持つ: $$\operatorname{diam}F_n \to 0,\ F_0\supset F_1\supset\cdots \implies \bigcap_{n<\omega} F_n \neq \emptyset.$$
（交わりは実は単集合、Remark X.4.6：直径0だから。）
証明: 完備なら各 $F_n$ から取った代表点が Cauchy 列 → 収束先は各 $F_n$ に属す（閉性）。逆向きは非完備な Cauchy 非収束列 $(x_n)$ から $F_m:=\operatorname{cl}{x_n:n>m}$ を作ると減少閉集合列で交わりが空（さもなくば cards/topology/cauchy-fundamental-filter の議論で収束してしまう）。
位相版（cards/topology/cantor-condition-countably-compact、Exercise IX.5.11「Cantor 条件」）との対応: あちらは「可算コンパクト ⟺ 減少閉集合列が交わりを持つ」（直径条件なし）、こちらは「完備性 ⟺ 直径→0という条件付き」で交わりを持つ — 完備性は可算コンパクト性の距離縮小版という対比が明確になる。
本ノート RoyalRoad.ChapterX.thm_X_4_5（完備 ⟹ 交叉性質の向きのみ形式化、nonempty_iInter_of_nonempty_biInter 経由、Notes/ChapterX.lean、lake build 済み）