Hello,
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
The Mizar formalization turned out to usually be better than Munkres.
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.)
I think it might be useful for students learning Mizar who want to find results in point-set topology, I hope you find it useful too :)
Best,
Alex