📐 Proposition VIII.3.2（Heine–Borel：区間のコンパクト性）
- 📐 Proposition VIII.3.2（Heine–Borel：区間のコンパクト性） #Card
- $\mathbb{R}$ の区間がコンパクトである条件と、証明の二分法の骨子は。
$\mathbb{R}$ の区間がコンパクト $\iff$ 閉かつ有界。
証明の骨子（二分法、witness-selection の一種）: $\mathcal{U}\in\beta[a,b]$ を取り、$[a,\frac{a+b}2]$ か $[\frac{a+b}2,b]$ のどちらかが $\mathcal{U}$ に入るのでそちらを選び続けて縮小区間列 $[a_k,b_k]$（$\mathcal{U}$ に属す）を作る。$b_k-a_k\to 0$ より $x:=\sup a_k=\inf b_k$ が定まり、$[a_k,b_k]\in\mathcal{N}\nu(x)^{#}$ から $\mathcal{U}\geq\mathcal{N}\nu(x)$、よって $x\in\lim_\nu\mathcal{U}$。
- 非閉（$[a,b[$）: $]b-\varepsilon,b[$ を含む超フィルターは $b\notin[a,b[$ に収束 → コンパクトでない。
- 非有界（$[a,+\infty[$）: $[n,+\infty[$ を含む超フィルターはどこにも収束しない。
isCompact_Icc（IsCompact (Set.Icc a b)）、Heine–Borel は Metric.isCompact_iff_isClosed_bounded 等。
本ノート RoyalRoad.ChapterVIII.prop_VIII_3_2_Icc / prop_VIII_3_2（区間版と一般 Heine–Borel、Notes/ChapterVIII.lean、lake build 済み）