Oh, I just noticed there is another issue with your definition, which might help explain why ^pm CC is used: You are requiring that f is a function on NN0, but we want it to work for functions that are only "eventually defined" on upper integers. In particular, we don't want to single out any particular upper integer set here, it should work just as well for NN and NN0, or (ZZ>=`37). I think you could get away with ^pm ZZ for this, but it's also sometimes convenient to use functions with a predetermined domain like RR or CC.
On Sun, Jan 23, 2022 at 2:18 PM Benoit <[email protected]> wrote: > On Sunday, January 23, 2022 at 4:46:01 PM UTC+1 [email protected] wrote: > >> The current definition of df-cau has fewer quantifiers and is also >> shorter. >> > > We can prove a few theorems of the form > F e. ( Cau ` X ) <-> .... > where each of these characterizations might have an advantage in different > cases. As for which characterization serves as "the" definition, this is > secondary once we have these characterizations, but I think the one I > proposed was easier to understand, closer to textbook definitions, and was > not using constructions such as ( y ( ball `d ) x ) (meaning: the open ball > of center y and radius x for the metric d). > > >> The switch to using structures is also breaking; I would want to see >> whether it leads to a shortening in theorems since you might have a raw >> distance function and wrapping it in a structure might cause issues. >> > > It would probably make proofs longer, because of the > packaging/unpackaging, as you wrote. But it would offer a more unified > framework across set.mm, it seems to me, instead of sometimes defining > notions on "structured sets" (set.mm's "extensible structures"), and > sometimes using the specific raw structure (here: the metric itself, or the > topology itself) instead of the structured set (here: the metric space, the > topological space). > > Anyway, I'm not going to change it, and I think Glauco's initial question > was about the domain of the function (i.e., why CC instead of NN0). > > 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/b1f2d238-6165-4928-b627-d571c8f17346n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/b1f2d238-6165-4928-b627-d571c8f17346n%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/CAFXXJSvbQH_atvwC%3Djv3YjALANa6D_jhPL9WOifacA2LyFKJAA%40mail.gmail.com.
