📐 Proposition XV.2.7（uniformity が距離から誘導される ⟺ 可算基を持つ）
- 📐 Proposition XV.2.7（uniformity が距離から誘導される ⟺ 可算基を持つ） #Card
- uniformity が距離（擬距離でなく metric）から来るための必要十分条件は。
uniformity が距離 $d$ から誘導される（${{d<2^{-n}}:n<\omega}$ が base）$\iff$ 可算 filter-base を持つ（countably based）。
証明（⟸）: $\mathcal{R}$ が uniformity で ${R_n:n<\omega}$ が filter-base とする。各 $n$ に対し $V_n^3\subset R_n$ なる $V_n\in\mathcal{R}$ を取れば $\bigcap_n V_n=\Delta$。cards/topology/lemma-xv-2-4-metrization-lemma の構成による擬距離が、この分離性のおかげで実は距離になる（$d(x,y)=0\implies x=y$）。