Re: Rosetta Stone for Point-Set Topology Results in Mizar
Alex Nelson thmprover _AT_ gmail.com <[email protected]> Thu, 16 Nov 2023 16:53:52 -0800
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <CAA+9CX3-ZNRJZ-n-Mo_8F1kKFU0B7Y+KW-nG6jSWZg4ZiRuqAg@mail.gmail.com> |
--0000000000009a678d060a4e923d Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Thanks for the feedback, everyone. I stopped this Rosetta stone *right before* the Nagata-Smirnov and Bing metrization theorems, so I'll dedicate some time this weekend to add them to the page. I'll sift through the proof wiki pages to see if I am missing anything, as well. Best, Alex On Wed, Nov 15, 2023 at 4:08=E2=80=AFAM Roland Coghetto roland_coghetto _AT= _ hotmail.com <[email protected]> wrote: > Hi, > > I spent the weekend assembling a "Rosetta Stone", organizing results a= s > found in Munkres's textbook on topology and their corresponding > formalization in Mizar: > > https://pqnelson.github.io/org-notes/comp-sci/theorem-provers/mizar/topol= ogy.html > > Great. > > In topology.html: > "This is called the Uniform Metric on RJ and it induces the Unifor= m > Topology on RJ. > 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." > > 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 > --0000000000009a678d060a4e923d Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable <html><body><div dir=3D"ltr">Thanks for the feedback, everyone.<br><br>I = stopped this Rosetta stone <i>right before</i> the Nagata-Smirnov an= d Bing metrization theorems, so I'll dedicate some time this weekend = to add them to the page.<div><br></div><div>I'll sift through the pro= of wiki pages to see if I am missing anything, as well.<br><br>Best,<br>A= lex</div></div><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"g= mail_attr">On Wed, Nov 15, 2023 at 4:08 AM Roland Coghetto roland_= coghetto _AT_ <a href=3D"http://hotmail.com">hotmail.com</a> <<a href=3D= "mailto:[email protected]">[email protected]= du.pl</a>> wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"= margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-l= eft:1ex">Hi,<br><br> I spent the weekend assembling a "Rosetta Stone", = organizing results as<br> found in Munkres's textbook on topology and their corres= ponding<br> formalization in Mizar:<br> <a href=3D"https://pqnelson.github.io/org-notes/comp-sci/the= orem-provers/mizar/topology.html" rel=3D"noreferrer">https://pqnelson.git= hub.io/org-notes/comp-sci/theorem-provers/mizar/topology.html</a><br><br>= Great.<br><br> In topology.html:<br> "This is called the Uniform Metric on RJ = and it induces the Uniform<br> Topology on RJ. <br> 1. Missing from Mizar — at= least, in this particular<br> formulation. I believe that it could be cobbled together usi= ng the<br> UNIFORM1, UNIFORM2, and UNIFORM3 articles."<br><br> See the answer from Henno Brandsma (1970-2022):<br><a href=3D"https://mat= h.stackexchange.com/questions/3849855/understanding-of-uniform-topology" = rel=3D"noreferrer">https://math.stackexchange.com/questions/3849855/under= standing-of-uniform-topology</a><br><br> There are a few results which are not formalized in Mizar, l= ike the<br> Urysohn metrization theorem, but it is entirely likely (high= ly<br> probable) that I have just been unable to find the formaliza= tion of<br> various results --- I have noted them in the Rosetta stone w= hen there<br> is no analogous result in the MML. (If I have missed somethi= ng, let me<br> know, and I will update my notes.)<br><br><a href=3D"http://= mizar.org/version/current/html/nagata_2.html" rel=3D"noreferrer">http://m= izar.org/version/current/html/nagata_2.html</a><br> :: The {N}agata-Smirnov Theorem. {P}art {II}<br> :: by Karol P\c{a}k<br><br><a href=3D"https://en.wikipedia.org/wiki/Nagat= a%E2%80%93Smirnov_metrization_theorem" rel=3D"noreferrer">https://en.wiki= pedia.org/wiki/Nagata%E2%80%93Smirnov_metrization_theorem</a><br> :: Nagata-Smirnov metrization theorem<br> theorem Th19: :: NAGATA_2:19<br> for T being non empty TopSpace holds<br> ( ( T is regular & T is T_1 & ex Bn being FamilySequence of T st = Bn is<br> Basis_sigma_locally_finite ) iff T is metrizable )<br><br><a href=3D"http= s://en.wikipedia.org/wiki/Bing_metrization_theorem" rel=3D"noreferrer">ht= tps://en.wikipedia.org/wiki/Bing_metrization_theorem</a><br> :: Bing metrization theorem<br> theorem :: NAGATA_2:22<br> for T being non empty TopSpace holds<br> ( ( T is regular & T is T_1 & ex Bn being FamilySequence of T st = Bn is<br> Basis_sigma_discrete ) iff T is metrizable )<br><br> Regards,<br> Roland<br></blockquote></div></body></html> --0000000000009a678d060a4e923d--