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.
