帰納次元

1：$\operatorname{ind}X\le0$ なら、各点 $x$ と近傍 $V$ に対し $x\in U\subset V$ となる開集合 $U$ で $\operatorname{Fr}U=\emptyset$、すなわち開かつ閉なものがある。このような $U$ の全体は開基である。逆も同じ言い換えである。
2：$\operatorname{Ind}X\le0$ なら、$A$ と $V:=X\setminus B$ に対し開かつ閉な $U$ で $A\subset U\subset X\setminus B$ となるものがある。逆に 2 の条件があれば、閉集合 $A$ と開集合 $V\supset A$ に対し、$A$ と $B:=X\setminus V$ に条件を使えばよい。$\square$

$M\cap U$ は $M$ の開集合なので $\operatorname{Fr}_M(M\cap U)=\operatorname{cl}_M(M\cap U)\setminus(M\cap U)$ である。$\operatorname{cl}_M(M\cap U)=M\cap\overline{M\cap U}\subset M\cap\overline{U}$ なので、$\operatorname{Fr}_M(M\cap U)\subset M\cap(\overline{U}\setminus U)=M\cap\operatorname{Fr}U$。$\square$

$\operatorname{ind}X=\infty$ なら示すことはない。$n\ge-1$ について次の主張 $P(n)$ を $n$ の帰納法で示す：「$\operatorname{ind}X\le n$ となる任意の正則空間 $X$ と任意の部分空間 $M$ について $\operatorname{ind}M\le n$」。
$P(-1)$：$X=\emptyset$ なら $M=\emptyset$ である。
$P(n-1)$ を仮定し、$\operatorname{ind}X\le n$（$n\ge0$）とする。$x\in M$ と、$M$ での $x$ の近傍 $V'$ をとる。$V'$ は $M$ の開集合 $M\cap V$（$V$ は $X$ の開集合、$x\in V$）を含む。$\operatorname{ind}X\le n$ より、$X$ の開集合 $U$ で $x\in U\subset V$、$\operatorname{ind}\operatorname{Fr}U\le n-1$ となるものがある。$M\cap U$ は $M$ の開集合で $x\in M\cap U\subset M\cap V\subset V'$ である。lem-inddim-boundary により $\operatorname{Fr}_M(M\cap U)$ は正則空間 $\operatorname{Fr}U$ の部分空間なので、$P(n-1)$ により $\operatorname{ind}\operatorname{Fr}_M(M\cap U)\le n-1$ である。よって $\operatorname{ind}M\le n$ で、$P(n)$ が成り立つ。$\square$

主張 $P(n)$：「$\operatorname{Ind}X\le n$ となる任意の正規空間 $X$ と任意の閉集合 $M$ について $\operatorname{Ind}M\le n$」を $n$ の帰納法で示す。$P(-1)$ は明らかである。
$P(n-1)$ を仮定し、$\operatorname{Ind}X\le n$（$n\ge0$）とする。$A$ を $M$ の閉集合、$V'$ を $A$ を含む $M$ の開集合とし、$V'=M\cap V$（$V$ は $X$ の開集合）と書く。$M$ は閉なので $A$ は $X$ の閉集合で、$W:=V\cup(X\setminus M)$ は $A$ を含む $X$ の開集合である。$\operatorname{Ind}X\le n$ より、$X$ の開集合 $U$ で $A\subset U\subset W$、$\operatorname{Ind}\operatorname{Fr}U\le n-1$ となるものがある。$M\cap U$ は $M$ の開集合で、$A\subset M\cap U\subset M\cap W=M\cap V=V'$ である。$\operatorname{Fr}_M(M\cap U)$ は $M$ の閉集合なので $X$ の閉集合であり、lem-inddim-boundary により正規空間 $\operatorname{Fr}U$ の閉集合である。$P(n-1)$ により $\operatorname{Ind}\operatorname{Fr}_M(M\cap U)\le n-1$ である。よって $\operatorname{Ind}M\le n$。$\square$

正規空間は正則なので $\operatorname{ind}X$ は定義される。主張 $P(n)$：「$\operatorname{Ind}X\le n$ となる任意の正規空間 $X$ について $\operatorname{ind}X\le n$」を帰納法で示す。$P(-1)$ は明らかである。$P(n-1)$ を仮定し $\operatorname{Ind}X\le n$ とする。点 $x$ と近傍 $V$ をとり、$x\in V_0\subset V$ となる開集合 $V_0$ をとる。一点集合 $\{x\}$ は閉なので、$\operatorname{Ind}X\le n$ を閉集合 $\{x\}$ と開集合 $V_0$ に使うと、開集合 $U$ で $x\in U\subset V_0$、$\operatorname{Ind}\operatorname{Fr}U\le n-1$ となるものがある。$\operatorname{Fr}U$ は正規空間なので $P(n-1)$ により $\operatorname{ind}\operatorname{Fr}U\le n-1$ であり、$\operatorname{ind}X\le n$ である。$\square$

$n=-1$ なら $X=\emptyset$ である。$n\ge0$ とし、点 $x$ と近傍 $V$ をとる。$x$ の開近傍 $W$ で $\operatorname{ind}W\le n$ となるものをとる。正則性により、開集合 $V'$ で $x\in V'\subset\overline{V'}\subset V\cap W$ となるものがある（正則空間 の記事の閉近傍による言い換え）。$\operatorname{ind}W\le n$ を $W$ での $x$ の近傍 $V'$ に使うと、$W$ の開集合 $U$ で $x\in U\subset V'$、$\operatorname{ind}\operatorname{Fr}_WU\le n-1$ となるものがある。$W$ は開集合なので $U$ は $X$ の開集合である。$\overline{U}\subset\overline{V'}\subset W$ なので、$W$ での閉包は $\overline{U}\cap W=\overline{U}$ であり、$\operatorname{Fr}U=\overline{U}\setminus U=\operatorname{Fr}_WU$ となる。よって $\operatorname{ind}\operatorname{Fr}U\le n-1$ で、$U\subset V$ である。$\square$

$n$ の帰納法で示す。$n=0$ では $\mathbb{R}^0$ は 1 点、$S^0=\{\pm1\}$ は 2 点の離散空間で、$\operatorname{ind}$ は $0$ である。
$n\ge1$ とし、$n-1$ で正しいとする。
$\mathbb{R}^n$ について：点 $x$ と近傍 $V$ に対し、開立方体 $C:=\prod_i(x_i-\varepsilon,x_i+\varepsilon)$ を $C\subset V$ となるようにとる。$\operatorname{Fr}C$ は閉立方体 $\overline{C}$ の表面で、中心 $x$ からの放射状の射影 $y\mapsto x+(y-x)/\|y-x\|$ により $x$ を中心とする単位球面と同相である。実際、この写像は連続で、$x$ から出る各半直線は表面とちょうど 1 点で交わる（半直線 $x+tu$ が表面に達するのは $t=\varepsilon/\max_i\lvert u_i\rvert$ のときだけ）ので全単射であり、コンパクト空間から Hausdorff 空間への連続な全単射として同相写像である。帰納法の仮定と位相不変性により $\operatorname{ind}\operatorname{Fr}C=\operatorname{ind}S^{n-1}\le n-1$ であり、$\operatorname{ind}\mathbb{R}^n\le n$。
$S^n$ について：各点 $p\in S^n$ の開近傍 $S^n\setminus\{-p\}$ は、$-p$ からの立体射影により $\mathbb{R}^n$ と同相なので、$\operatorname{ind}(S^n\setminus\{-p\})\le n$ である。$S^n$ は距離空間なので正則であり、lem-inddim-local により $\operatorname{ind}S^n\le n$。
最後の主張は thm-inddim-subspace による。$\square$

prop-inddim-zero の 2 を使う。$A,B$ を互いに素な閉集合とし、交わらない開集合 $U,W$ で $A\subset U$、$B\subset W$、$U\cup W=X$ となるものを作る。このとき $U=X\setminus W$ は開かつ閉である。
正規空間では、互いに素な閉集合 $P,Q$ に対し、開集合 $U'\supset P$、$W'\supset Q$ で $\overline{U'}\cap\overline{W'}=\emptyset$ となるものがとれる（$P$ と $Q$ を開集合 $O_1,O_2$ で分け、閉集合 $P$ と $X\setminus O_1$、$Q$ と $X\setminus O_2$ をさらに分けて、閉包が $O_1$、$O_2$ に入る開集合をとる）。これを「閉包ごと分ける」と呼ぶ。
段 0． $A$ と $B$ を閉包ごと分けて、開集合 $U_0\supset A$、$W_0\supset B$ で $\overline{U_0}\cap\overline{W_0}=\emptyset$ となるものをとる。
段 $k$（$k\ge1$）． 開集合 $U_{k-1},W_{k-1}$ で $\overline{U_{k-1}}\cap\overline{W_{k-1}}=\emptyset$ となるものができているとする。$\overline{U_{k-1}}\cap F_k$ と $\overline{W_{k-1}}\cap F_k$ は $F_k$ の互いに素な閉集合なので、$\operatorname{Ind}F_k\le0$ と prop-inddim-zero により、$F_k$ で開かつ閉な集合 $G$ で
$$ \overline{U_{k-1}}\cap F_k\subset G\subset F_k\setminus\overline{W_{k-1}} $$
となるものがある。$G$ と $F_k\setminus G$ は $F_k$ の閉集合なので $X$ の閉集合である。
$$ P:=\overline{U_{k-1}}\cup G,\qquad Q:=\overline{W_{k-1}}\cup(F_k\setminus G) $$
は閉集合で、互いに素である（$\overline{U_{k-1}}\cap\overline{W_{k-1}}=\emptyset$、$\overline{U_{k-1}}\cap(F_k\setminus G)=\emptyset$、$G\cap\overline{W_{k-1}}=\emptyset$、$G\cap(F_k\setminus G)=\emptyset$）。$P$ と $Q$ を閉包ごと分けて、開集合 $U_k\supset P$、$W_k\supset Q$ で $\overline{U_k}\cap\overline{W_k}=\emptyset$ となるものをとる。
作り方から、$U_0\subset U_1\subset\cdots$、$W_0\subset W_1\subset\cdots$、$U_k\cap W_k=\emptyset$、$F_k\subset U_k\cup W_k$ である。$U:=\bigcup_kU_k$、$W:=\bigcup_kW_k$ は開集合で、$A\subset U$、$B\subset W$ である。$U_k\cap W_l\subset U_m\cap W_m=\emptyset$（$m:=\max\{k,l\}$）より $U\cap W=\emptyset$ であり、各点はある $F_k$ に入るので $U\cup W=X$ である。$\square$

要点：点ごとに $A$ か $B$ の一方と交わらない開かつ閉な近傍をとり、可算個に減らして互いに交わらないように差をとる。

可分距離空間は第 2 可算なので Lindelöf であり（第2可算公理 の記事の命題「三つの帰結」と定理「距離空間における同値性」）、その閉集合も Lindelöf である。prop-inddim-lindelof により $\operatorname{Ind}F_k\le0$、thm-inddim-sum により $\operatorname{Ind}X\le0$、thm-inddim-ind-le-large-ind により $\operatorname{ind}X\le0$。可算な距離空間は一点集合（$\operatorname{ind}=0$ の閉集合）の可算個の和である。$\square$