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/c54f5b85-7cc1-4395-8ee6-160063a1287dn%40googlegroups.com.
