Hi Frédéric, The definitions of RR^ (and by extension EEhil) use toCHil, which itself uses toNrmGrp (~ df-tng).
The toNrmGrp operation ensures that the topology and metric components are set according to the distance. The norm is always defined according to the distance (see ~ df-nm)，so it will be compatible with the topology and metric. As far as the uniform structure is concerned, toNrmGrp does not set it. If we want it to be set correctly (so that the resulting space is a uniform space), we would need to modify toNrmGrp to also set the uniform structure to the uniform structure generated by the structure’s metric. This is provided by the “ metUnif “ function (see ~ df-metu). So... here is the whole process again: * df-cnfld defines the complex addition and multiplication operation. * df-refld restricts it to the field of the real numbers * df-rgmod / df-sra assigns the field of reals as its own scalar field, and the inner product as the real multiplication, so we obtain the real numbers as a left module, * df-frlm / df-dsmm (df-prds) defines an inner product on the direct sum (product) structure, so that we get the inner product as the sum of (inner) products of each components, pairwise. This is the scalar product. * df-tch then defines a norm function as the square root of the inner (scalar) product of a vector with itself, * df-tng uses that norm to populate the distance (which is a metric) and topology. It may be enhanced to also populate the uniform structure defined from the same distance. Is there any interesting application for that? * finally, df-ehl restricts the whole to index sets of the form ( 1 ... N ) It’s indeed a complicated construct, but it is following the path you describe. I believe all bits and pieces are there for a Hilbert space. I’ll try to continue on that path! _ Thierry > Le 2 juil. 2019 à 02:07, 'fl' via Metamath <[email protected]> a > écrit : > > > 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. -- 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/A6BEB6E3-AB5A-43A7-AA6A-55A9724AAE0A%40gmx.net.
