Re: Rosetta Stone for Point-Set Topology Results in Mizar

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/topo=
logy.html
  =20
Great.

In topology.html:
       "This is called the Uniform Metric on RJ and it induces the Uniform
   Topology on RJ.=20
           1. Missing from Mizar =E2=80=94 at least, in this particular
   formulation. I believe that it could be cobbled together using the
   UNIFORM1, UNIFORM2, and UNIFORM3 articles."
  =20
See the answer from Henno Brandsma (1970-2022):
https://math.stackexchange.com/questions/3849855/understanding-of-uniform-t=
opology

   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