距離化可能空間

$a\in A$ と $r>0$ に対し、制限距離による $A$ の開球は
$$ B_{d|_A}(a,r)=A\cap B_d(a,r) $$
である。よって制限距離の開球は相対位相で開である。逆に、相対位相の開集合 $U=A\cap V$ と $a\in U$ をとる。$V$ は $X$ で開だから、ある $r>0$ について $a\in B_d(a,r)\subset V$ である。したがって
$$ a\in B_{d|_A}(a,r)\subset U $$
となり、相対位相の各開集合は制限距離の開球の和集合である。二つの位相は一致する。$\square$

非負性、対称性、および $\delta(x,y)=0$ と $x=y$ の同値は $d$ の対応する性質から従う。三角不等式を示す。非負実数 $s,t$ について
$$ \min\{s+t,1\}\le \min\{s,1\}+\min\{t,1\} $$
が成り立つ。実際、右辺が $1$ 以上なら明らかであり、右辺が $1$ 未満なら $s<1$、$t<1$ で右辺は $s+t$ に等しい。$d$ の三角不等式とこの評価から
$$ \begin{aligned} \delta(x,z) &=\min\{d(x,z),1\}\\ &\le\min\{d(x,y)+d(y,z),1\}\\ &\le\delta(x,y)+\delta(y,z) \end{aligned} $$
を得る。よって $\delta$ は距離である。
$0< r<1$ に対しては
$$ B_\delta(x,r)=B_d(x,r) $$
である。実際、$\delta(x,y)< r<1$ なら $d(x,y)<1$ かつ $\delta(x,y)=d(x,y)< r$ であり、逆向きは明らかである。各点で半径 $1$ 未満の開球だけを使っても距離位相の開基になるので、$d$ と $\delta$ は同じ位相を誘導する。最後の主張は、距離化可能空間に適合する距離 $d$ を一つ選び、この構成を適用すれば従う。$\square$

1 から 2：$B_d(x,\varepsilon)$ は $d$ の位相で開集合なので、1 により $d'$ の位相でも開集合である。$x$ を含むので、$d'$ の距離位相の定義により $B_{d'}(x,\delta)\subset B_d(x,\varepsilon)$ となる $\delta>0$ がある。後半も同様である。
2 から 1：$U$ を $d$ の位相で開集合とし、$x\in U$ をとる。$B_d(x,\varepsilon)\subset U$ となる $\varepsilon>0$ があり、2 の前半により $B_{d'}(x,\delta)\subset B_d(x,\varepsilon)\subset U$ となる $\delta>0$ がある。よって $U$ は $d'$ の位相で開集合である。$d$ と $d'$ を入れ替えれば逆も成り立つ。$\square$

いずれかの $X_n$ が空なら $X$ は空で距離化可能なので、以下すべての因子を空でないとする。各 $\delta_n$ は prop-metrizable-space-bounded-metric により $X_n$ の位相に適合する距離で、$0\le\delta_n\le1$ である。したがって $D$ の級数は絶対収束し $0\le D\le1$ である。非負性と対称性は項ごとに従う。$D(x,y)=0$ ならすべての $n$ で $\delta_n(x_n,y_n)=0$、従って $x_n=y_n$ なので $x=y$ である。逆は明らかである。各 $\delta_n$ の三角不等式を重み $2^{-n}$ で足せば $D$ の三角不等式を得る。よって $D$ は距離である。
次に位相の一致を示す。まず $D$ の開球が各点で直積位相の近傍を含むことを示す。$x\in X$ と $\varepsilon>0$ をとる。$\varepsilon>1$ なら $B_D(x,\varepsilon)=X$ なのでよい。$0<\varepsilon\leq1$ とし、
$$ \sum_{n>N}2^{-n}<\frac{\varepsilon}{2} $$
となる $N$ をとる。有限個の座標を制限した直積位相の基本近傍
$$ U:=\bigcap_{n=1}^{N}\pi_n^{-1} \left(B_{\delta_n}\left(x_n,\frac{\varepsilon}{2}\right)\right) $$
を考える。$y\in U$ なら
$$ \begin{aligned} D(x,y) &=\sum_{n=1}^{N}2^{-n}\delta_n(x_n,y_n) +\sum_{n>N}2^{-n}\delta_n(x_n,y_n)\\ &<\frac{\varepsilon}{2}\sum_{n=1}^{N}2^{-n} +\sum_{n>N}2^{-n} <\varepsilon \end{aligned} $$
だから $U\subset B_D(x,\varepsilon)$ である。従って $D$ の距離位相は直積位相より細かくない。
逆に、$x$ を含む直積位相の基本近傍
$$ V=\bigcap_{n\in F}\pi_n^{-1}(V_n) $$
をとる。ここで $F$ は有限集合で、各 $V_n$ は $x_n$ を含む $X_n$ の開集合である。$F=\emptyset$ なら $V=X$ なのでよい。各 $n\in F$ について $r_n>0$ を
$$ B_{\delta_n}(x_n,r_n)\subset V_n $$
となるように選び、
$$ \eta:=\frac12\min_{n\in F}(2^{-n}r_n)>0 $$
とおく。$D(x,y)<\eta$ なら、各 $n\in F$ について
$$ 2^{-n}\delta_n(x_n,y_n)\le D(x,y)<\eta<2^{-n}r_n $$
なので $y_n\in V_n$ である。よって $B_D(x,\eta)\subset V$ となる。従って直積位相は $D$ の距離位相より細かくない。二つの位相は一致する。$\square$

各 $X_s$ に $1$ 以下の適合距離 $\rho_s$ を選ぶ（prop-metrizable-space-bounded-metric）。$x,y\in X$ に対し、ある $s$ で $x,y\in X_s$ なら $\rho(x,y):=\rho_s(x,y)$、そうでなければ $\rho(x,y):=1$ とおく。非負性・対称性・$\rho(x,y)=0\iff x=y$ は明らかである。三角不等式 $\rho(x,z)\le\rho(x,y)+\rho(y,z)$ は、三点が同じ成分にあれば $\rho_s$ の三角不等式であり、そうでなければ右辺のどちらかの項が $1$ で左辺は $1$ 以下なので成り立つ。
位相の一致：$x\in X_s$、$0< r\le1$ なら $B_\rho(x,r)=B_{\rho_s}(x,r)$ である（他の成分の点は距離 $1$ なので入らない）。$U$ が直和位相で開で $x\in U\cap X_s$ なら、$U\cap X_s$ は $X_s$ で開なので $B_{\rho_s}(x,r)\subset U\cap X_s$ となる $r\in(0,1]$ があり、$B_\rho(x,r)\subset U$ である。逆に $V$ が $\rho$ の位相で開なら、各 $s$ と $x\in V\cap X_s$ について $B_\rho(x,r)\subset V$ となる $r\in(0,1]$ があり、$B_{\rho_s}(x,r)=B_\rho(x,r)\subset V\cap X_s$ なので $V\cap X_s$ は $X_s$ で開である。$\square$

距離化可能空間では、各点 $x$ における半径 $1/m$ の開球 $(m\ge1)$ が可算な基本近傍系になるので、第1可算公理を満たす。そこで $[0,1]^I$ が零点 $0=(0)_{i\in I}$ で第1可算でないことを示す。
$0$ の可算な基本近傍系 $(U_m)_{m\ge1}$ があると仮定する。各 $m$ について、有限個の座標だけを制限する直積位相の基本近傍 $W_m$ を
$$ 0\in W_m\subset U_m $$
となるようにとり、$W_m$ が制限する有限座標集合を $F_m\subset I$ とする。$J:=\bigcup_mF_m$ は可算なので、$I$ の非可算性から $j\in I\setminus J$ をとれる。
$$ O:=\{x\in[0,1]^I\mid x_j<1/2\} $$
は $0$ の開近傍である。基本近傍系の仮定により、ある $m$ で $U_m\subset O$ となる。ところが $j\notin F_m$ なので $W_m$ は第 $j$ 座標を制限しない。第 $j$ 座標だけを $1$、他を $0$ とした点は $W_m\subset U_m$ に属するが $O$ には属さず、矛盾する。従って $[0,1]^I$ は第1可算でなく、距離化可能でない。これは thm-metrizable-space-countable-product の「可算積」を任意積へ置き換えられないことを示す。$\square$