Thanks Benoit,
> I was thinking of ~suprcl and nearby theorems. For the present proof, the
> wanted supremum is sup ( ( abs " ( F " RR ) ) , RR , < ). But first, try to
> state the theorem. It should be something like
> ${
> $d x y z t u F $. $d x y z t u G $. $d x y z t u M $. <--- probably overkill
> $e |- ( ph -> F : RR --> RR ) $.
> $e |- ( ph -> G : RR --> RR ) $.
> $e |- ( ph -> A. x e. RR A. y e. RR .............. ) $.
> $e |- ( ph -> -. A. z e. RR ( F ` z ) = 0 ) $.
> $e |- ( ph -> M e. RR ) $.
> $e |- ( ph -> A. t e. RR ( abs ` ( F ` t ) ) <_ M ) $.
> $( B2 from IMO 1972 $)
> $p |- ( ph -> A. u e. RR ( abs ` ( G ` u ) ) <_ 1 ) $= ? $.
> $}
I had a similar formalization of the statement in mind. One question
for which I'm looking guidance is on using quantifiers or not.
As an example, I believe the following are all valid but presumably
drastically influence the proof strategy?
> $e |- ( ph -> -. A. z e. RR ( F ` z ) = 0 ) $.
> $e |- ( ph -> E. z e. RR ( F ` z ) =/= 0 ) $.
> $e |- ( ph -> C e. RR )
> $e |- ( 0 < ( abs ` ( F ` C ) ) ) $.
> $e |- ( ph -> C e. RR )
> $e |- ( ( F ` C ) =/= 0 ) $.
I'm very curious to better understand how do people go about making
these choices?
Best,
On Fri, Feb 28, 2020 at 1:22 AM Benoit <[email protected]> wrote:
>>
>> I have stumbled upon the supremum definition but it looks more intricate to
>> use than a manually defining it inline on the real line (unless you’re
>> referring to another definition of the least upper bound). That’s precisely
>> one of the open questions I have about how to go about formalizing this type
>> of proofs!
>
>
> I was thinking of ~suprcl and nearby theorems. For the present proof, the
> wanted supremum is sup ( ( abs " ( F " RR ) ) , RR , < ). But first, try to
> state the theorem. It should be something like
> ${
> $d x y z t u F $. $d x y z t u G $. $d x y z t u M $. <--- probably overkill
> $e |- ( ph -> F : RR --> RR ) $.
> $e |- ( ph -> G : RR --> RR ) $.
> $e |- ( ph -> A. x e. RR A. y e. RR .............. ) $.
> $e |- ( ph -> -. A. z e. RR ( F ` z ) = 0 ) $.
> $e |- ( ph -> M e. RR ) $.
> $e |- ( ph -> A. t e. RR ( abs ` ( F ` t ) ) <_ M ) $.
> $( B2 from IMO 1972 $)
> $p |- ( ph -> A. u e. RR ( abs ` ( G ` u ) ) <_ 1 ) $= ? $.
> $}
>
> Maybe some more experienced contributors prefer another style (e.g.,
> expressions versus functions) ?
> One can also use fewer variables (e.g. replace z, t and u with x). I do not
> know which choice will make the proof simpler.
>
> As suggested above, maybe start with simpler proofs for practice ?
>
> Benoît
>
> --
> 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/79b726e8-f42c-452a-a6d6-95bfb11c4110%40googlegroups.com.
--
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_0zjqPAeZkQEpur9sNsk78xcB80imGTMtk8VdtJP22UPyw%40mail.gmail.com.
