Completely regular or Uniformizable

CompletelyRegularSpace in Mathlib.Topology.CompletelyRegular

A space in which points and closed sets can be separated by a function.

Namely, given a closed set AA and a point bAb \notin A, there is a continuous function f:X[0,1]f:X \rightarrow [0,1] such that f(A)={0}f(A) = \{0\} and f(b)=1f(b)=1.

Defined in 14.8 of MR MR2048350.

Equivalently, the topology is induced by a uniformity. See Theorem 38.2 in MR MR2048350 and Wikipedia Uniform_space.