Uniformizable Spaces

A topological space is uniformizable (there exists a uniformity that generates the same topology) iff it is completely regular.

Main Results

• UniformSpace.toCompletelyRegularSpace: Uniform spaces are completely regular
• CompletelyRegularSpace.exists_uniformSpace: Completely regular spaces are uniformizable
• CompletelyRegularSpace.of_exists_uniformSpace: Uniformizable spaces are completely regular
• completelyRegularSpace_iff_exists_uniformSpace: A space is completely regular iff it is uniformizable

Implementation Details

Urysohn's lemma is reused in the proof of UniformSpace.completelyRegularSpace.

References

• https://www.math.wm.edu/~vinroot/PadicGroups/519probset1.pdf

instance UniformSpace.toCompletelyRegularSpace {X : Type u_1} [UniformSpace X] : CompletelyRegularSpace X

theorem CompletelyRegularSpace.of_exists_uniformSpace {X : Type u_1} [t : TopologicalSpace X] (h : ∃ (u : UniformSpace X), u.toTopologicalSpace = t) : CompletelyRegularSpace X

theorem CompletelyRegularSpace.exists_uniformSpace {X : Type u_1} [t : TopologicalSpace X] [CompletelyRegularSpace X] : ∃ (u : UniformSpace X), u.toTopologicalSpace = t

theorem completelyRegularSpace_iff_exists_uniformSpace {X : Type u_1} [t : TopologicalSpace X] : CompletelyRegularSpace X ↔ ∃ (u : UniformSpace X), u.toTopologicalSpace = t