Urysohnの距離化定理

連続性。各成分 $\pi_n\circ F=f_n$ が連続なので、直積位相の普遍性（直積位相の記事の定理「直積位相の普遍性」）により $F$ は連続である。
単射性。$x\ne y$ とする。$X$ は $T_1$ なので $\{y\}$ は閉であり、$U:=X\setminus\{y\}$ は $x$ を含む開集合である。仮定から $f_n(x)>0$ かつ $X\setminus U=\{y\}$ の上で $f_n=0$ となる $n$ があり、$f_n(x)\ne f_n(y)$、したがって $F(x)\ne F(y)$ である。
像の上への開写像であること。$U\subset X$ を開集合とし、$F(U)$ が $F(X)$ の開集合であることを示す。$z\in F(U)$ をとり、$z=F(x)$、$x\in U$ とする。仮定から $f_n(x)>0$ かつ $X\setminus U$ の上で $f_n=0$ となる $n$ がある。
$$ W:=\pi_n^{-1}\bigl((0,1]\bigr)=\{t\in H\mid t_n>0\} $$
は $H$ の開集合で、$z=F(x)\in W$ である。$F(y)\in W$ なら $f_n(y)>0$ なので $y\in U$ である。よって $W\cap F(X)\subset F(U)$ であり、$z$ は $F(U)$ に含まれる $F(X)$ の開集合 $W\cap F(X)$ の点である。$z$ は任意なので $F(U)$ は $F(X)$ の開集合である。
以上より $F\colon X\to F(X)$ は連続な全単射で開集合を開集合に写すので、同相写像である。$\square$

$X$ は正規性条件を満たす。第 2 可算空間は Lindelöf である（第2可算公理の記事の命題「三つの帰結」）。正則な Lindelöf 空間は、互いに素な閉集合を互いに素な開集合で分離できる（Lindelöf空間の記事の命題「正則なLindelöf空間の分離」）。
関数を並べる。$\{B_i\}_{i\ge1}$ を $X$ の可算な開基とし（開基が有限なら同じ集合を繰り返して並べる）、
$$ P:=\bigl\{(i,j)\bigm|\overline{B_i}\subset B_j\bigr\} $$
とおく。$(i,j)\in P$ なら、$\overline{B_i}$ と $X\setminus B_j$ は互いに素な閉集合なので、Urysohnの補題（値域を取り替えた形）により、$\overline{B_i}$ 上で $1$、$X\setminus B_j$ 上で $0$ をとる連続関数 $g_{ij}\colon X\to[0,1]$ がある（組ごとに 1 つ選ぶ）。$P$ は可算集合 $\{1,2,\dots\}^2$ の部分集合なので高々可算であり、関数 $g_{ij}$（$(i,j)\in P$）を $f_1,f_2,\dots$ と一列に並べる（$P$ が有限なら零関数を補って無限列にする）。
点と閉集合を分離する。$x\in X$、$U$ を $x$ を含む開集合とする。開基なので $x\in B_j\subset U$ となる $j$ がある。正則性条件の言い換えにより、$x\in V\subset\overline{V}\subset B_j$ となる開集合 $V$ がある。再び開基を使って $x\in B_i\subset V$ となる $i$ をとる。$\overline{B_i}\subset\overline{V}\subset B_j$ なので $(i,j)\in P$ であり、$g_{ij}(x)=1>0$、$X\setminus U\subset X\setminus B_j$ の上で $g_{ij}=0$ である。$g_{ij}$ は列 $(f_n)$ のどれかなので、族は点と閉集合を分離する。$\square$

lem-urymet-family により、点と閉集合を分離する連続関数の列 $f_n\colon X\to[0,1]$ をとる。$X$ は $T_1$ なので、lem-urymet-embedding により $F(x)=(f_n(x))_{n\ge1}$ は $X$ から $F(X)\subset H$ への同相写像である。
$H$ の距離 $D$（def-urymet-hilbert-cube）を $F(X)$ に制限すると、$F(X)$ の相対位相に適合する距離になる（距離空間の部分集合では、制限した距離の開球が相対位相を生成する。距離化可能空間の記事の例「Euclid空間と部分空間」とその証明）。これを $F$ で引き戻した
$$ d(x,y):=D\bigl(F(x),F(y)\bigr)=\sum_{n=1}^{\infty}2^{-n}\lvert f_n(x)-f_n(y)\rvert $$
は、$F$ が単射なので $X$ 上の距離であり、$F$ が $X$ から $(F(X),D)$ への同相写像なので、$d$ の開球 $B_d(x,\varepsilon)=F^{-1}\bigl(B_D(F(x),\varepsilon)\cap F(X)\bigr)$ が生成する位相は $X$ の位相と一致する。よって $X$ は距離化可能である。$\square$

1 ⇒ 3 は thm-urymet-main である。
3 ⇒ 2：$H$ は距離 $D$ をもつので、その部分空間は制限した距離で距離化可能である（prf-urymet-main と同じ理由）。$H$ は第 2 可算で、第 2 可算性は部分空間に遺伝し（第2可算公理の記事の命題「部分空間への遺伝」）、第 2 可算空間は可分である（同じ記事の命題「三つの帰結」）。これらは同相で保たれる。
2 ⇒ 1：距離化可能空間は正規空間であり（正規空間の記事の定理「距離空間は正規」）、したがって $T_1$ で正則性条件を満たす（同じ記事の命題「正規空間は正則かつ Hausdorff」）。距離空間では可分性と第 2 可算性が同値である（第2可算公理の記事の定理「距離空間における同値性」）。$\square$