Formal systems for the win \o/ -stan
On Thu, Apr 30, 2020 at 10:28 AM Marnix Klooster <[email protected]> wrote: > Hi all, > > For the record, there are two (related) mistakes in my write-up (the > picture in my March 23 email): > > - The properties (0) and (1) of sup are of course only correct for > *upper-bounded* V. > - Therefore in the steps where we use these properties, we need to > know that |f| and |f*g| are upper bounded, so we *do* use the |f|≤1 > assumption. > > And the good news is that I discovered these when studying Stan's > http://us.metamath.org/mpeuni/imo72b2.html. :-) > > Groetjes, > <>< > Marnix > > Op ma 23 mrt. 2020 om 18:38 schreef Marnix Klooster < > [email protected]>: > >> Hi Stan, >> >> If I were to formalize this in Metamath, I'd use the first proof, but in >> a more calculational format. >> >> I've attached it, unfortunately as a picture. >> >> Yes, this is a longer proof, but it seems somehow easier to me. >> >> Hope this helps someone... :-) >> >> [image: image.png] >> >> >> Groetjes, >> <>< >> Marnix >> >> Op do 27 feb. 2020 om 18:08 schreef 'Stanislas Polu' via Metamath < >> [email protected]>: >> >>> Hi all, >>> >>> I'm quite a beginner with Metamath (I have read a bunch of proofs, most >>> of the metamath book, I have implemented my own verifier, but I haven't >>> constructed any original proof yet) and I am looking to formalize the >>> following proof: >>> >>> IMO B2 1972: http://www.cs.ru.nl/~freek/demos/exercise/exercise.pdf >>> Alternative version: >>> http://www.cs.ru.nl/~freek/demos/exercise/exercise2.pdf >>> >>> (More broadly, I think this would be an interesting formalization to >>> have in set.mm given this old but nonetheless interesting page: >>> http://www.cs.ru.nl/~freek/demos/index.html) >>> >>> I am reaching out to the community to get direction on how should I go >>> about creating an efficient curriculum for myself in order to achieve that >>> goal? Any other advice is obviously welcome! >>> >>> Thank you! >>> >>> -stan >>> >>> -- >>> You received this message because you are subscribed to the Google >>> Groups "Metamath" group. >>> To unsubscribe from this group and stop receiving emails from it, send >>> an email to [email protected]. >>> To view this discussion on the web visit >>> https://groups.google.com/d/msgid/metamath/78223c8d-eddf-4f84-970d-6b0cbb20dab9%40googlegroups.com >>> <https://groups.google.com/d/msgid/metamath/78223c8d-eddf-4f84-970d-6b0cbb20dab9%40googlegroups.com?utm_medium=email&utm_source=footer> >>> . >>> >> >> >> -- >> Marnix Klooster >> [email protected] >> > > > -- > Marnix Klooster > [email protected] > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/CAF7V2P9BKgAORpE2j6COqZmqD%2B7R5yHfZPnUg3Qpk4DQ3D0ZXQ%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CAF7V2P9BKgAORpE2j6COqZmqD%2B7R5yHfZPnUg3Qpk4DQ3D0ZXQ%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACZd_0yOUzYYPxS09Pw%3Dup75TAK3w%3D3M0ZE%3DDNWf1yAzNVZB-A%40mail.gmail.com.
