Completely metrizable theorem

[StevenClontz]

Whether the metric fan is completely metrizable came up in our call today. Indeed, for any almost-discrete metrizable space we can choose a metric where the distance between any two isolated points is greater than some fixed $\epsilon>0$, so any Cauchy sequence is either eventually constant or converges to the one non-isolated point. (Constructively: given some metric $d(x,y)$, take $d\prime(x,y)$ that equals 1 when $x$ and $y$ are both isolated and $\min(1,d(x,y))$ otherwise.) Since this is a theorem we can add later, I see no need to add a trait now.

Originally posted by @danflapjax in https://github.com/pi-base/data/issues/804#issuecomment-2423719412

[prabau]

This is pending the introduction of "almost discrete". See #807.

[StevenClontz]

Added a question at https://math.stackexchange.com/questions/4987308/are-almost-discrete-metrizable-spaces-always-completely-metrizable

[StevenClontz]

From that conversation, I'd pitch these theorems:

• Almost discrete + first countable => metrizable
• Almost discrete => strong Choquet
• metrizable + strong Choquet => completely metrizable

I think http://at.yorku.ca/b/ask-a-topologist/2002/0254.htm says P63 implies strong Choquet, so we could weaken the assumptions of T132.