Sure, but that seems a bit pedantic. It induces a sequence in the obvious way. Arguably you could have a different notion of convergence for functions with more general domain, along the lines of df-rlim, but the minimalistic assumptions in df-cau are enough to prove most of the usual theorems and there is no need to be picky.
On Sun, Jan 23, 2022 at 2:59 PM Benoit <[email protected]> wrote: > On Sunday, January 23, 2022 at 8:42:15 PM UTC+1 [email protected] wrote: > >> 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. >> > > Indeed, and I mentioned this in my previous message: > > (provided there is a "Slot" for the (extended) metric of a metric > space). It might be better to define it for uniform spaces. Maybe one > could allow functions defined on ( ZZ>= ` n ) for n \in ZZ. > > If a function is defined on a larger domain, then it is not a sequence, > hence not a Cauchy sequence. Restricting it to NN0 may yield one. > > 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/ec3cec80-8dad-47c9-a757-ed2681a176fdn%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/ec3cec80-8dad-47c9-a757-ed2681a176fdn%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/CAFXXJSvT4Nd3H0fdOG2jFuT24S0vQ6-6uTGwYnsx8J5YCg_MXQ%40mail.gmail.com.
