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/b4e5aee5-61ce-421a-8d42-3fd00e40321fn%40googlegroups.com.
