SKolodynski / IsarMathLib

IsarMathLib is a library of formalized mathematics for Isabelle/ZF.
https://isarmathlib.org
Other
16 stars 2 forks source link

A topological space is uniformizable iff it is completely regular. #16

Open SKolodynski opened 3 years ago

SKolodynski commented 3 years ago

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.