The former message must be read this way. (Modifications marked by two stars.)
I think you should adapt your *EEhil* (and RR^) definition so that the > topology and uniform structure are generated from the distance. Currently > and unless I'm mistaken (the definitions are sometimes a little confusing) > I think they are independent. It will allow to speak of EEhil as a Hilbert > space with a standard norm defined from the inner product, a standard > distance defined from the norm, a uniform structure defined from the > distance, and a standard topology defined from the uniform structure. > > -- 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/0eed8f5b-a63f-421d-a1d2-9e19e85eb2a6%40googlegroups.com.
