Wanted to follow-up on the question above that may have been lost in translation, if anyone could shed some light on it:
> One question that remains pertains to DVs: I'm surprised to see the DVs bubble up even if the variable does not appear in the final statement? Why is that the case? Thanks! -stan On Mon, Mar 9, 2020 at 1:41 PM Stanislas Polu <[email protected]> wrote: > Finished proof available here: > https://github.com/metamath/set.mm/compare/develop...spolu:spolu-mathbox?expand=1 > > What an adventure, thank you all for your precious help! > > ``` > $d B c t $. $d B u v $. $d B x $. $d B t y $. $d F c t $. $d F u v $. > $d F x $. $d F t y $. $d G c t $. $d G u v $. $d G x $. $d G t y $. > $d c ph t $. $d ph u v $. $d ph x $. $d ph t y $. $d u y $. > imo72b2.1 $e |- ( ph -> F : RR --> RR ) $. > imo72b2.2 $e |- ( ph -> G : RR --> RR ) $. > imo72b2.4 $e |- ( ph -> B e. RR ) $. > imo72b2.5 $e |- ( ph -> A. u e. RR A. v e. RR ( ( F ` ( u + v ) ) + ( > F ` ( u - v ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` v ) ) ) ) $. > imo72b2.6 $e |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 ) $. > imo72b2.7 $e |- ( ph -> E. x e. RR ( F ` x ) =/= 0 ) $. > $( IMO 1972 B2. $) > imo72b2 $p |- ( ph -> ( abs ` ( G ` B ) ) <_ 1 ) $= > ``` > > One question that remains pertains to DVs: I'm surprised to see the DVs > bubble up even if the variable does not appear in the final statement? Why > is that the case? > > Also, to answer my own question as well as react on Benoit's remark: > > > > One question for which I'm looking guidance is on using quantifiers or > not. > > > That's a very important question, and I hope someone with more > experience will be able to shed some insight. In particular, if one has a > hypothesis, say, "E. x ph", then it is common to see in textbooks things > like "Let y be such that ph(y). Then [subproof], so [conclusion which does > not depend on y]. Therefore, [that conclusion]." I would formalize it in > set.mm by using the "deduction style" and prepending "[. y / x ]. ph" as > an antecedent to each line of the subproof. Maybe there are better > strategies ? > > From the experience formalizing imo72b2, I think that when relying on > natural deduction forms, hypotheses should favor quantifiers (stronger) > while conclusions shouldn't (easier to work with). Going from a lemma > without quantifier to a resolved goal with quantifier is relatively easy > with rspcdv, rspcedvd and the likes. > > -stan > > On Sat, Mar 7, 2020 at 1:25 PM Stanislas Polu <[email protected]> wrote: > >> Thanks! Makes perfect sense. I will adapt the proof accordingly! >> >> -stan >> >> On Sat, Mar 7, 2020 at 10:47 AM Mario Carneiro <[email protected]> wrote: >> >>> Yep, you correctly identified eliman0 as the bad lemma here. I hadn't >>> heard of it but it's using a trick to avoid having to prove that the input >>> is in the domain of the function. Using metamath.exe, I searched for this >>> pattern and got a few results: >>> >>> MM> sea * '( ? ` ? ) e. ( ? " ? )'/j >>> 19563 eliman0 $p |- ( ( A e. B /\ -. ( F ` A ) = (/) ) -> ( F ` A ) e. ( >>> F " B >>> ) ) >>> 20603 funfvima $p |- ( ( Fun F /\ B e. dom F ) -> ( B e. A -> ( F ` B ) >>> e. ( F >>> " A ) ) ) >>> 20604 funfvima2 $p |- ( ( Fun F /\ A C_ dom F ) -> ( B e. A -> ( F ` B ) >>> e. ( F >>> " A ) ) ) >>> 20611 fnfvima $p |- ( ( F Fn A /\ S C_ A /\ X e. S ) -> ( F ` X ) e. ( F >>> " S ) >>> ) >>> 20740 f1elima $p |- ( ( F : A -1-1-> B /\ X e. A /\ Y C_ A ) -> ( ( F ` >>> X ) e. >>> ( F " Y ) <-> X e. Y ) ) >>> 79323 kqfvima $e |- F = ( x e. X |-> { y e. J | x e. y } ) $p |- ( ( J >>> e. ( >>> TopOn ` X ) /\ U e. J /\ A e. X ) -> ( A e. U <-> ( F ` A ) e. ( F " >>> U ) ) >>> ) >>> >>> and the actual theorems you want to reference are either funfvima, >>> funfvima2, or fnfvima depending on how the function is presented. (Arguably >>> eliman0 should be moved to after fnfvima and given a more similar name, >>> e.g. fviman0.) In this case, the function has known domain and range so I >>> would go for fnfvima, using fnco to prove that ( abs o. F ) Fn RR. >>> >>> >>> On Fri, Mar 6, 2020 at 11:59 PM 'Stanislas Polu' via Metamath < >>> [email protected]> wrote: >>> >>>> (fvco3d is a natural deduction form of fvco3 proved here: >>>> https://github.com/metamath/set.mm/commit/454132a35254c17c4e54353b5c2c772eeb2ebb65#diff-12dc1484b058d1ee6cb68a74194d66c7R641421-R641429 >>>> ) >>>> >>>> -stan >>>> >>>> On Sat, Mar 7, 2020 at 8:54 AM Stanislas Polu <[email protected]> wrote: >>>> >>>>> Interesting! >>>>> >>>>> It basically comes from an attempt at satisfying the conditions >>>>> for eliman0. Here's the full proof draft: >>>>> >>>>> ``` >>>>> $( <MM> <PROOF_ASST> THEOREM=imo72b2lem1 LOC_AFTER=? >>>>> >>>>> h1::imo72b2lem1.1 |- ( ph -> F : RR --> RR ) >>>>> h2::imo72b2lem1.7 |- ( ph -> E. x e. RR ( F ` x ) =/= 0 ) >>>>> h3::imo72b2lem0.6 |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 ) >>>>> >>>>> !d84:: |- ( ( ph /\ x e. RR ) -> ( ( abs o. F ) ` x ) =/= (/) >>>>> ) >>>>> d83:d84:adantrr |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) >>>>> -> ( ( abs o. F ) ` x ) =/= (/) ) >>>>> d81:d83:neneqd |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>>>> -. ( ( abs o. F ) ` x ) = (/) ) >>>>> >>>>> d95:1:ffvelrnda |- ( ( ph /\ x e. RR ) -> ( F ` x ) e. RR ) >>>>> d94:d95:adantrr |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>>>> ( F ` x ) e. RR ) >>>>> d92:d94:recnd |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) >>>>> -> ( F ` x ) e. CC ) >>>>> d93::simprr |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>>>> ( F ` x ) =/= 0 ) >>>>> d91:d92,d93:absrpcld |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) >>>>> -> ( abs ` ( F ` x ) ) e. RR+ ) >>>>> d9:d91:rpgt0d |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>>>> 0 < ( abs ` ( F ` x ) ) ) >>>>> >>>>> d80::simprl |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>>>> x e. RR ) >>>>> d82::eliman0 |- ( ( x e. RR /\ -. ( ( abs o. F ) ` x ) = (/) ) >>>>> -> ( ( abs o. F ) ` x ) e. ( ( abs o. F ) " RR ) ) >>>>> d75:d80,d81,d82:syl2anc |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) >>>>> ) -> ( ( abs o. F ) ` x ) e. ( ( abs o. F ) " RR ) ) >>>>> oeqaa::imaco |- ( ( abs o. F ) " RR ) = ( abs " ( F " RR ) ) >>>>> d71:d75,oeqaa:syl6eleq |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) >>>>> -> ( ( abs o. F ) ` x ) e. ( abs " ( F " RR ) ) ) >>>>> d73:1:adantr |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>>>> F : RR --> RR ) >>>>> d74::simprl |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>>>> x e. RR ) >>>>> d72:d73,d74:fvco3d |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>>>> ( ( abs o. F ) ` x ) = ( abs ` ( F ` x ) ) ) >>>>> d7:d72,d71:eqeltrrd |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> >>>>> ( abs ` ( F ` x ) ) e. ( abs " ( F " RR ) ) ) >>>>> >>>>> d10::simpr |- ( ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) >>>>> /\ z = ( abs ` ( F ` x ) ) ) -> z = ( abs ` ( F ` x ) ) ) >>>>> d8:d10:breq2d |- ( ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) >>>>> /\ z = ( abs ` ( F ` x ) ) ) -> ( 0 < z <-> 0 < ( abs ` ( F ` x ) ) ) ) >>>>> >>>>> d6:d7,d8,d9:rspcedvd |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) >>>>> -> E. z e. ( abs " ( F " RR ) ) 0 < z ) >>>>> qed:2,d6:rexlimddv |- ( ph -> E. z e. ( abs " ( F " RR ) ) 0 < z ) >>>>> >>>>> $) >>>>> >>>>> -stan >>>>> >>>>> On Fri, Mar 6, 2020 at 11:58 PM Mario Carneiro <[email protected]> >>>>> wrote: >>>>> >>>>>> The composition function value combination is easy enough to >>>>>> eliminate using fvco, but the equality to the empty set is a type error, >>>>>> because the lhs is a real number and the question of whether the empty >>>>>> set >>>>>> is a real number is deliberately left ambiguous by the real number >>>>>> axioms. >>>>>> So I would like to know what steps got you to this point. There are some >>>>>> function value theorems that assume this as a "convenience" but there >>>>>> should be analogues of them that don't (probably with some other >>>>>> assumption >>>>>> like the function is a set). >>>>>> >>>>>> On Fri, Mar 6, 2020 at 8:02 AM 'Stanislas Polu' via Metamath < >>>>>> [email protected]> wrote: >>>>>> >>>>>>> Thanks again Mario! >>>>>>> >>>>>>> I made more progress towards the final demonstration of the full IMO >>>>>>> problem. Working on the following lemma: >>>>>>> >>>>>>> ``` >>>>>>> h1::imo72b2lem1.1 |- ( ph -> F : RR --> RR ) >>>>>>> >>>>>>> h2::imo72b2lem1.7 |- ( ph -> E. x e. RR ( F ` x ) =/= 0 ) >>>>>>> >>>>>>> h3::imo72b2lem0.6 |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ >>>>>>> 1 ) >>>>>>> ``` >>>>>>> >>>>>>> I need to prove the following goal which seems pretty obvious but >>>>>>> I'm struggling to find a way to discharge it: >>>>>>> >>>>>>> ``` >>>>>>> d84:: |- ( ( ph /\ x e. RR ) -> ( ( abs o. F ) ` x ) =/= (/) >>>>>>> ) >>>>>>> ``` >>>>>>> >>>>>>> Any idea on how to proceed with this? >>>>>>> >>>>>>> Thanks thanks! >>>>>>> >>>>>>> -stan >>>>>>> >>>>>>> On Thu, Mar 5, 2020 at 6:27 PM Mario Carneiro <[email protected]> >>>>>>> wrote: >>>>>>> >>>>>>>> There is a theorem specifically for that translation, something >>>>>>>> like A. x e. ( F " A ) P[x] <-> A. y e. A P[( F ` y )]. It's probably >>>>>>>> called ralima but you've caught me on the bus again. >>>>>>>> >>>>>>>> Mario >>>>>>>> >>>>>>>> On Thu, Mar 5, 2020, 8:07 AM 'Stanislas Polu' via Metamath < >>>>>>>> [email protected]> wrote: >>>>>>>> >>>>>>>>> Thanks Mario! >>>>>>>>> >>>>>>>>> I just finished formalizing the following lemma (which is a good >>>>>>>>> chunk of the proof \o/): >>>>>>>>> >>>>>>>>> ``` >>>>>>>>> $d F c x $. $d c ph x $. >>>>>>>>> imo72b2lem.1 $e |- ( ph -> F : RR --> RR ) $. >>>>>>>>> imo72b2lem.2 $e |- ( ph -> G : RR --> RR ) $. >>>>>>>>> imo72b2lem.3 $e |- ( ph -> A e. RR ) $. >>>>>>>>> imo72b2lem.4 $e |- ( ph -> B e. RR ) $. >>>>>>>>> imo72b2lem.5 $e |- ( ph -> ( ( F ` ( A + B ) ) + ( F ` ( A - B >>>>>>>>> ) ) ) = ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) ) $. >>>>>>>>> imo72b2lem.6 $e |- ( ph -> A. x e. ( abs " ( F " RR ) ) x <_ 1 >>>>>>>>> ) $. >>>>>>>>> imo72b2lem.7 $e |- ( ph -> E. x e. RR ( F ` x ) =/= 0 ) $. >>>>>>>>> >>>>>>>>> imo72b2lem $p |- ( ph -> ( ( abs ` ( F ` A ) ) x. ( abs ` ( G >>>>>>>>> ` B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) ) $= >>>>>>>>> ``` >>>>>>>>> >>>>>>>>> Proof here: >>>>>>>>> https://github.com/spolu/set.mm/commit/454132a35254c17c4e54353b5c2c772eeb2ebb65 >>>>>>>>> >>>>>>>>> One thing I'm quite dissatisfied with is the shape of >>>>>>>>> `imo72b2lem.6`. I'd much rather have the more natural/intuitive >>>>>>>>> expression >>>>>>>>> `|- ( ph -> A. x e. RR ( abs ` ( F `x ) ) <_ 1 )` but I completely >>>>>>>>> failed >>>>>>>>> to prove imo72b2lem.6 from it. Any help on this would be greatly >>>>>>>>> appreciated! >>>>>>>>> >>>>>>>>> -stan >>>>>>>>> >>>>>>>>> On Wed, Mar 4, 2020 at 8:45 PM Mario Carneiro <[email protected]> >>>>>>>>> wrote: >>>>>>>>> >>>>>>>>>> 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 >>>>>>>>>> <https://groups.google.com/d/msgid/metamath/CAFXXJStosWZ0BEO7zjpeW90VMNT3pf-Kr6nUaqLefJyA%3Dgwa2Q%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_0zgFkBD0kOaAXNGyB3PL18Qt06uSHV%3DEmwOjh6Rk5j3OQ%40mail.gmail.com >>>>>>>>> <https://groups.google.com/d/msgid/metamath/CACZd_0zgFkBD0kOaAXNGyB3PL18Qt06uSHV%3DEmwOjh6Rk5j3OQ%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/CAFXXJSs4iVxdk7Uz1_bW-heUVCJy-CMGENLNtzWd8%2B12rFEVBQ%40mail.gmail.com >>>>>>>> <https://groups.google.com/d/msgid/metamath/CAFXXJSs4iVxdk7Uz1_bW-heUVCJy-CMGENLNtzWd8%2B12rFEVBQ%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_0x2N3k16mC%2Byc_%3D6HvNQ3OWpAXtQ3fHkMv%3DPqERwFR60Q%40mail.gmail.com >>>>>>> <https://groups.google.com/d/msgid/metamath/CACZd_0x2N3k16mC%2Byc_%3D6HvNQ3OWpAXtQ3fHkMv%3DPqERwFR60Q%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/CAFXXJSv0pGnDb%2Bfae5_ZS_mAK_R6MeMQPAL4gsHD-9S5g2XSVQ%40mail.gmail.com >>>>>> <https://groups.google.com/d/msgid/metamath/CAFXXJSv0pGnDb%2Bfae5_ZS_mAK_R6MeMQPAL4gsHD-9S5g2XSVQ%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_0yzRWT%3DZn6qPpgXPbzSabuOqHVSLW6uG9aF6S6yYht5mA%40mail.gmail.com >>>> <https://groups.google.com/d/msgid/metamath/CACZd_0yzRWT%3DZn6qPpgXPbzSabuOqHVSLW6uG9aF6S6yYht5mA%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/CAFXXJSutmF6LrPLUHM%3DoBbd5d_4kE8jeM9j-gFsc9tnYVU4Mcg%40mail.gmail.com >>> <https://groups.google.com/d/msgid/metamath/CAFXXJSutmF6LrPLUHM%3DoBbd5d_4kE8jeM9j-gFsc9tnYVU4Mcg%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_0wpSzR5JhXYHkGLSq9F%2ByUVc_p-JAZ%2BnX5gO26gKsz82A%40mail.gmail.com.
