Hi Thierry, I missed the fact that the topology is defined from the distance by toNrmGrp.
I still think that the order of definitions should be: (1) The distance is defined from the norm. (2) The uniform structure is defined from the distance. (3) The topology is defined from the uniform structure. We should adopt this order for all spaces where there are combined norms metrics, uniform structures, topologies, regardless of the level of generality of the spaces for the sake of homogeneity. It bothers me that the norm is defined by distance. (Even if in this case, this is possible. But only because there is a zero.) There may be a shortcut for topologies defined in terms of distances by bypassing uniform structures. Because there is still a problem of generality. The least general, the most particular space here is the normed space, then the metric space then the space with a uniform structure then the space with a topology. There are spaces where there are distances and no norms. There are spaces where the natural concept is the norm. The distance is derived. Hoping to have been able to convey what I wanted to say and I havn't made any mistakes. (I also notice, in df-nm, that putting dist in the middle of the expression (x(dist`w)(0g` w)) can be difficult to understand when you are not a distinguished expert in metamath. But it's not your definition.) -- FL -- 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/ed288a9d-d64c-4fbd-b6fe-26d54ae6c329%40googlegroups.com.
