Rosetta Stone for Point-Set Topology Results in Mizar

--000000000000e7da6c060a10d399
Content-Type: text/plain; charset="UTF-8"

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

--000000000000e7da6c060a10d399
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">Hello,<br><br>I spent the weekend assembling a &quot;Roset=
ta Stone&quot;, organizing results as found in Munkres&#39;s=C2=A0textbook =
on topology and their corresponding formalization in Mizar:=C2=A0<a href=3D=
"https://pqnelson.github.io/org-notes/comp-sci/theorem-provers/mizar/topolo=
gy.html">https://pqnelson.github.io/org-notes/comp-sci/theorem-provers/miza=
r/topology.html</a><div><br></div><div>The Mizar formalization turned out t=
o usually=C2=A0be better than Munkres.<br><br>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 t=
he formalization of various results --- I have noted them in the Rosetta st=
one when there is no analogous result in the MML. (If I have missed somethi=
ng, let me know, and I will update my notes.)<br><br>I think it might be us=
eful for students learning Mizar who want to find results in point-set topo=
logy, I hope you find it useful too :)<br><br>Best,<br>Alex</div></div>

--000000000000e7da6c060a10d399--