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 and a point , there is a continuous function such that and .
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.
Id | Spaces | Value | Source |
---|---|---|---|
1 | Discrete topology on a two-point set | ||
21 | Weak topology on separable Hilbert space | ||
74 | Niemytzki's tangent disc topology | ||
1103 | Supercontinuum power of a countable discrete space |