IsarMathLib icon indicating copy to clipboard operation
IsarMathLib copied to clipboard

A topological space is uniformizable iff it is completely regular.

Open SKolodynski opened this issue 4 years ago • 0 comments

The dependency for this statement is to define the natural topology on the real numbers. This is probably best done through metric spaces. Since pseudometrics play a role in the proof one probably should start from that.

SKolodynski avatar Dec 25 '20 14:12 SKolodynski