Some fixes.
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. > > *(a) 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.) * > > *(b) There may be a shortcut for topologies defined in terms of distances > by bypassing uniform structures. But it bothers me too. * > > *The reason is that there is a problem of generality in (a) and (b).* > *We should adopt a homogeneous way of treating all spaces and not rely on properties specific to a type of space. This does not mean that we cannot then prove the derivations specific to a specific space. If we adopt a homogeneous and standard way of defining all these spaces, it will be easier to memorize and manage. We will not have to check the details of the definitions for each structure.* -- 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/268f1733-9225-4ead-8afe-628adef310ea%40googlegroups.com.
