Hi,
I spent the weekend assembling a "Rosetta Stone", organizing results as
found in Munkres's textbook on topology and their corresponding
formalization in Mizar:
https://pqnelson.github.io/org-notes/comp-sci/theorem-provers/mizar/topology.html
Great.
In topology.html:
"This is called the Uniform Metric on RJ and it induces the Uniform
Topology on RJ.
1. Missing from Mizar — at least, in this particular
formulation. I believe that it could be cobbled together using the
UNIFORM1, UNIFORM2, and UNIFORM3 articles."
See the answer from Henno Brandsma (1970-2022):
https://math.stackexchange.com/questions/3849855/understanding-of-uniform-topology
There are a few results which are not formalized in Mizar, like the
Urysohn metrization theorem, but it is entirely likely (highly
probable) that I have just been unable to find the formalization of
various results --- I have noted them in the Rosetta stone when there
is no analogous result in the MML. (If I have missed something, let me
know, and I will update my notes.)
http://mizar.org/version/current/html/nagata_2.html
:: The {N}agata-Smirnov Theorem. {P}art {II}
:: by Karol P\c{a}k
https://en.wikipedia.org/wiki/Nagata%E2%80%93Smirnov_metrization_theorem
:: Nagata-Smirnov metrization theorem
theorem Th19: :: NAGATA_2:19
for T being non empty TopSpace holds
( ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is
Basis_sigma_locally_finite ) iff T is metrizable )
https://en.wikipedia.org/wiki/Bing_metrization_theorem
:: Bing metrization theorem
theorem :: NAGATA_2:22
for T being non empty TopSpace holds
( ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is
Basis_sigma_discrete ) iff T is metrizable )
Regards,
Roland