Rudin's "Principles of Analysis" Rosetta Stone

Alex Nelson thmprover _AT_ gmail.com <[email protected]> Sat, 25 Nov 2023 19:41:59 -0800
Newsgroups gmane.comp.mathematics.mizar
Message-ID <CAA+9CX3zggkfp=cZWepyS7xz6W3-mk-tiX=WTUsCS=EXopt5=w@mail.gmail.com>
--00000000000052c549060b05f835
Content-Type: text/plain; charset="UTF-8"

Hello,

I would like to bring to your attention an effort I stumbled across (of
which I have not yet participated in), an attempt to identify the
definitions and theorems from Rudin's "Principles of Mathematical Analysis"
with their counterparts in Mizar:
https://en.wikibooks.org/wiki/Mizar_Commentary_on_Walter_Rudin%27s_Principles_of_Mathematical_Analysis

Now, if only someone would do Dieudonne's treatise on analysis... ;)

Best,
Alex

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

<div dir=3D"ltr">Hello,<br><br>I would like to bring to your attention an e=
ffort I stumbled across (of which I have not yet participated in), an attem=
pt to identify the definitions and theorems from Rudin&#39;s &quot;Principl=
es of Mathematical Analysis&quot; with their counterparts in Mizar:=C2=A0<a=
 href=3D"https://en.wikibooks.org/wiki/Mizar_Commentary_on_Walter_Rudin%27s=
_Principles_of_Mathematical_Analysis">https://en.wikibooks.org/wiki/Mizar_C=
ommentary_on_Walter_Rudin%27s_Principles_of_Mathematical_Analysis</a><div><=
br></div><div>Now, if only someone would do Dieudonne&#39;s treatise on ana=
lysis... ;)<br><br>Best,<br>Alex</div></div>

--00000000000052c549060b05f835--