📐 Exercise X.10.9（Dini の定理）
- 📐 Exercise X.10.9（Dini の定理） #Card
- 単調増加する連続関数列が連続関数に各点収束すれば一様収束することの主張と、Cantor 条件を使った証明の骨子は。
Dini の定理: $\tau$ が可算コンパクト、${f_n}\subset C(\tau,\nu)$ が増加列で $f(x):=\lim_\nu(f_n(x))_n\in C(\tau,\nu)$ なら、$(f_n)_n$ は $f$ に一様収束する。
証明: $F_n:={f_n\geq f-\varepsilon}$ は閉集合の減少列で（各点収束と単調性から）$\bigcap_n F_n=\emptyset$。cards/topology/cantor-condition-countably-compact（Cantor 条件）の対偶から、ある $n_0$ で $F_{n_0}=\emptyset$（以降も空）— すなわち $n\geq n_0$ で $\sup_X|f-f_n|<\varepsilon$。
「各点収束 + 単調性 + コンパクト性 ⟹ 一様収束」という古典的な Dini の定理が、Cantor 条件（減少閉集合列の交わり）というたった一つの補題から一行で従う。次カード（平方根の一様近似）の直接の道具。
本ノート RoyalRoad.ChapterX.exercise_X_10_9（コンパクト空間版、Monotone.tendstoUniformly_of_forall_tendsto、Notes/ChapterX.lean、lake build 済み）