IsarMathLib
IsarMathLib copied to clipboard
A topological space is uniformizable iff it is completely regular.
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.