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.
