📐 Theorem X.7.8（Urysohn の補題）
- 📐 Theorem X.7.8（Urysohn の補題） #Card
- 正規空間の disjoint 閉集合が関数的分離できることの主張と、証明の骨子（有理数添字の入れ子開集合族）は。
Urysohn の補題: 正規位相空間の disjoint な閉集合 $A_0,A_1$ は関数的分離可能（cards/topology/functionally-separated-sets）。
証明の骨子: $[0,1]\cap\mathbb{Q}={r_n}$（$r_0=0,r_1=1$）に対し帰納的に開集合族 ${U_r}$ を構成、$A_0\subset U_0$、$U_1=X\setminus A_1$、かつ $$r<t \implies \operatorname{cl}\xi U_r \subset U_t \tag{X.7.1}$$ （各段で Exercise IX.5.9「正規性の近傍閉包条件」を使い中間の $U{r_{n+1}}$ を挿入）。
$$f(x) := \inf{r : x\in U_r}\quad(x\notin A_1),\qquad f(x):=1\ (x\in A_1)$$
とすると $f\in C$、$f=0$ on $A_0$、$f=1$ on $A_1$。位相的正規性から関数的分離性が「無料で」出るという、正則性の場合（cards/topology/functionally-regular-topology とは独立の公理が必要）との対比が本質。
exists_continuous_zero_one_of_isClosed（Urysohn’s lemma）。
本ノート RoyalRoad.ChapterX.thm_X_7_8（Notes/ChapterX.lean、lake build 済み）