As long as one is willing to accept that the (rescaled) sine function ( x e. CC |-> (sin ` ( _pi x. x ) ) ) is both an unbounded holomorphic function and a Cauchy sequence, all is fine.
On Sunday, January 23, 2022 at 9:23:11 PM UTC+1 [email protected] wrote: > 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/4f0eae2f-2290-4486-bfca-169b05d844e9n%40googlegroups.com.
