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.
