>
> 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.
