Can't look right now, but you should search for a theorem of the form A = (/) <-> ( F " A ) = (/) .
On Wed, Mar 4, 2020, 11:30 AM 'Stanislas Polu' via Metamath < [email protected]> wrote: > I'm now looking to prove that `( abs " ( F " RR ) ) =/= (/)` given `F : RR > --> RR`. From my exploration of the definition of --> I believe this should > be enough but I don't see an easy path towards that? Would anybody have an > example in mind that could give me a little bit of inspiration? > > Thanks for the continued support! > > -stan > > On Wed, Mar 4, 2020 at 6:29 PM Benoit <[email protected]> wrote: > >> Stan: you're right about the need to prove this (if using explicit >> substitution): look for the utility theorems exchanging [. / ]. with other >> symbols (quantifiers, operations). As said by Jim and Thierry, who are >> more experienced in proof building, implicit substitution might be easier >> to use. I think it is instructive to compare the details of both proving >> styles on a specific example (e.g. ralbidv, suggested by Thierry, would be >> analogous to exchanging [. / ]. with A.). >> >> Still, I think adding what I called rspesbcd could prove useful (if it is >> not already in set.mm under another label; I cannot search now, but it >> probably is already somewhere). >> >> 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/ebdd296f-6bcd-49e0-88c8-c7fef3628cdd%40googlegroups.com >> <https://groups.google.com/d/msgid/metamath/ebdd296f-6bcd-49e0-88c8-c7fef3628cdd%40googlegroups.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_0zFiVT5n-7%2BYh-YL2mDCLMom6R66gq7gbMT7tgJzTzadQ%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CACZd_0zFiVT5n-7%2BYh-YL2mDCLMom6R66gq7gbMT7tgJzTzadQ%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/CAFXXJStosWZ0BEO7zjpeW90VMNT3pf-Kr6nUaqLefJyA%3Dgwa2Q%40mail.gmail.com.
