Sure, please. As a side note, I (as everybody else, in this forum) keep adding small theorems that could be used to shorten proofs I wrote before.
When I find myself writing three times the same 5 line proof, then I decide to extract a theorem, and almost certainly it could be used to shorten a dozen of my previous theorems, but it's hard to go back and find/rewrite them all. But cnfex is simply useless :-) Il giorno giovedì 22 aprile 2021 alle 20:16:37 UTC+2 [email protected] ha scritto: > Thanks everyone! > > Glauco, if you are interested, I was able to shorten 3 other proofs in > your mathbox, they are: n0p (339 to 330 bytes), unima (412 to 79 bytes), > and nelrnresa (87 to 58 bytes), all of them rely on the same, or a subset > of the axioms originally used. Let me know if you want to see them and I > will post them here! > > On Thursday, April 22, 2021 at 1:43:51 PM UTC-4 Glauco wrote: > >> Did I really write it? :-) >> >> It looks like I wrote it when I was proving the Stone Weierstrass >> theorem, and that's been my first theorem in mm. >> >> Back then, the whole framework was new to me, and I guess that the (sad) >> simple explanation is that I didn't know I was just one a1i away from ovex. >> >> Thanks for the post, added to the refactor/cleanup mathbox to-do list. >> >> >> Glauco >> >> Il giorno giovedì 22 aprile 2021 alle 04:15:04 UTC+2 [email protected] ha >> scritto: >> >>> It is a bit of a strange theorem. I see that it is in Glauco's mathbox >>> (and referenced a few times), and both the proof and the uses can be >>> simplified using ovex, but perhaps there is something that they were trying >>> to avoid (not axioms, the axiom list is a strict subset with the new >>> proof). Perhaps they can chime in here. >>> >>> On Wed, Apr 21, 2021 at 9:48 PM Jim Kingdon <[email protected]> wrote: >>> >>>> On 4/21/21 5:37 PM, Kyle Wyonch wrote: >>>> >>>> > I was wondering if this shortening [of cnfex] was valid >>>> >>>> Short answer is, yes it is valid. >>>> >>>> The longer answer is that set.mm defines a function evaluated outside >>>> its domain to be the empty set which is why >>>> http://us.metamath.org/mpeuni/fvex.html does not have any conditions. >>>> >>>> By contrast, iset.mm does not have the ability to do quite this, so >>>> instead cnfex would need to use >>>> http://us.metamath.org/ileuni/funfvex.html or one of the other >>>> alternatives under fvex at >>>> http://us.metamath.org/ileuni/mmil.html#setmm >>>> >>>> There is some discussion of this in the "undefined results" section of >>>> http://us.metamath.org/mpeuni/conventions.html and >>>> http://us.metamath.org/ileuni/conventions.html >>>> >>>> -- >>>> 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/c36661f8-ac06-7264-2dd8-d95a1cb1b41f%40panix.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/53e31fad-fb19-4cd2-bb2d-617eac65e1cdn%40googlegroups.com.
