Metrization: Urysohn, Nagata–Smirnov, Bing, Smirnov

Let $X$ be a topological space. A family $\mathcal{D}$ of subsets of $X$ is discrete if every $x\in X$ has a neighbourhood meeting at most one member of $\mathcal{D}$. It is therefore a locally finite family in the sense of Refinements, locally finite families, point-finite families, and star refinements.

An open basis $\mathcal{B}$ (Basis and subbasis for a topology, and the topology generated by a family of sets) is $\sigma$-locally finite if $\mathcal{B}={\bigcup }_{n\in \mathbb{N}}{\mathcal{B}}_n$ for locally finite families ${\mathcal{B}}_n$, and $\sigma$-discrete if the families ${\mathcal{B}}_n$ can be taken discrete. Empty layers are permitted; the word $\sigma$ records the countable indexing convention of Finite, countably infinite, countable, uncountable.

Every discrete family is locally finite. Consequently every $\sigma$-discrete basis is $\sigma$-locally finite.

A topological space $X$ is locally metrizable if every $x\in X$ belongs to an open set $U\subseteq X$ whose subspace topology (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace) is metrizable (Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not). Thus $U$ is an open neighbourhood of $x$ in the convention of Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open; no global metric on $X$ is part of the definition.

For an open cover $\mathcal{U}$ and $x\in X$, write $\mathrm{St}(x,\mathcal{U})=\mathrm{St}(\{x\},\mathcal{U})$, using the star of Refinements, locally finite families, point-finite families, and star refinements. A sequence $({\mathcal{U}}_n{)}_{n\in \mathbb{N}}$ of open covers is normal if ${\mathcal{U}}_{n+1}$ star-refines ${\mathcal{U}}_n$ for every $n$.

It is compatible with the topology if (i) for $x\mathrm{\ne }y$ some $n$ has $y\mathrm{\notin }\mathrm{St}(x,{\mathcal{U}}_n)$, and (ii) for every open neighbourhood $O$ of $x$ (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open) some $n$ has $\mathrm{St}(x,{\mathcal{U}}_n)\subseteq O$. The indexing starts at $0$; an empty space has the legal empty cover at every index.

If a $T_1$ space has a compatible normal sequence of open covers, then it is metrizable.

Assume the Axiom of Choice. Every metric space has a $\sigma$-locally-finite open basis.

Assume the Axiom of Choice. A regular $T_1$ space with a $\sigma$-locally-finite basis has a compatible normal sequence of open covers.

Source convention. In Granath's source, regularity is defined only for a Fréchet space, i.e. a $T_1$ space. The displayed library statement therefore names $T_1$ separately rather than silently importing that convention.

Not proved in this library. This is a source-backed fallback rather than a local proof. The discarded local route chose a shrinking $W(B,x)$ for every point of every basis member and claimed that its families stayed locally finite. That claim is false: with $X=B=\mathbb{R}$ and the one-member locally finite family $\{B\}$, the allowed shrinkings $W(B,x)=(x-1,x+1)$ have infinite local overlap at every point. The standard normal-cover construction needs additional machinery beyond that failed pointwise shrinking.

Why it remains visible. The Nagata--Smirnov comparison below depends on exactly this standard route. Its dependency marker therefore records that the result is externally sourced rather than pretending that the invalid local construction proves it.

Assume the Axiom of Choice. A space is metrizable if and only if it is regular, $T_1$, and has a $\sigma$-locally-finite basis. Here regularity and $T_1$ are separate hypotheses.

Assume the Axiom of Choice. Every metric space has a $\sigma$-discrete open basis.

Not proved in this library. This is a source-backed fallback rather than a local proof. The discarded construction assigns every point to a first centre and then asserts that the resulting cells are open. They need not be: in $\mathbb{R}$, with integer centres at scale $1$ ordered $0,1,-1,2,\dots$, the cell assigned to $1$ is $[1,2)$. Intersecting it with a positive-distance condition does not repair that failure.

Why it remains visible. Bing's standard necessity direction needs a real discrete-open refinement argument. The external-dependency marker is retained on this result and its consequences so that none of them is mistaken for a locally established theorem.

Assume the Axiom of Choice. A space is metrizable if and only if it is regular, $T_1$, and has a $\sigma$-discrete basis.

Assume the Axiom of Choice. Every regular $T_1$ second-countable space is metrizable.

Let $\mathcal{U}$ be a locally finite open cover of $X$. If every $U\in \mathcal{U}$, with its subspace topology, has a $\sigma$-locally-finite open basis ${\bigcup }_n{\mathcal{B}}_{U,n}$, then $X$ has a $\sigma$-locally-finite open basis.

Assume the Axiom of Choice. A space is metrizable if and only if it is paracompact, Hausdorff, and locally metrizable.