My dear Thierry, I think you should adapt your EE (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 RRhil 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.
(The promised comments are coming in. The weather has been a little hot so far.) -- 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/b10abc04-40ea-4698-8fa8-047442c54812%40googlegroups.com.
