Forget the name "generalized Euclidean space"

[benjub]

I was reminded of the name "generalized Euclidean space" in https://github.com/metamath/set.mm/pull/2993#discussion_r1080671402. The definition is at https://us.metamath.org/mpeuni/df-rrx.html

To me the best name to call ( RR^ ` I ) is simply "( RR^ ` I )" (and if you have to pronounce it: "R to the I"). First, "generalized euclidean space" is nonstandard. I never heard of it with that meaning (which is no proof it's nonstandard of course, but an indication). It is probably used in multiple places, and my guess is that it is given various different meanings, but generally not the present one, for a reason I now explain.

The space ( RR^ ` I ) is a specific and concrete one (and this is especially true in set.mm where everything is encoded in set theory: this is a specifc set of specific sets of... down to \varnothing). On the other hand, definitions of Euclidean spaces, Banach spaces (or really mostly anything: abelian group, polish space, distributive lattice, affine scheme, Cauchy sequence...) are about objects satisfying some properties, rather than specific objects. That is, these definitions generally begin like "a ...... space is a (real) vector space such that.....".

As an illustration of this, you can point at a specific nonzero element of RR^I (provided that you can point at a specific element of I), like (1, 0, 0, ...), but you cannot point at a specific nonzero vector of B if I just tell you that B is a real Banach space. Still in other words (but this is linked to the previous illustration), anyone reasonable would hope that a space which is isomorphic (in the appropriate category, here the category of real prehilbertian spaces with obvious morphisms) to a "generalized Euclidean space" is also a "generalized Euclidean space". But a real prehilbertian space isomorphic to ( RR^ ` I ) need not be an ( RR^ ` J ) (for a rather silly reason: just define your favorite "reals" to be of the form (0, x) where x is a real, and transport all the structures to that new set).

Lastly, of course there are names for specific famous objects, like the Cantor set or the Klein group (or bottle) or the Hopf fibration, etc. We cannot here christen some specific objects with new names like was done for these very standard ones.

[tirix]

I agree with Benoît, and as a matter of fact Wikipedia also makes a clear distinction:

• Real Coordinate Space denotes the specific construct, with ( RR^ ` n ) as a notation
• Euclidean Space is the general concept.

It would be nice to have separate definitions, and to show for example:

• that the Real Coordinate Space of dimension n, ( RR^ ` n ), is an Euclidean Space,
• that all Euclidean spaces of dimension n are isomorphic to ( RR^ ` n )

[avekens]

Thank you, @benjub, for the clarification and pointing out the seemingly small, but important differences of the two concepts. And @tirix gives a convincing solution for this issue: Calling ( RR^ ` n ) a "real coordinate space", as done in Wikipedia, is a really good idea (in German it is called "reeller Koordinatenraum"). So this should be applied to set.mm, i.e., ( RR^ ` n ) should be called "real coordinate space" instead of "generalized Euclidean space" in set.mm.

But how should (EEhil ` n ) be called then? "finite-dimensional real coordinate space"?

According to Wikipedia, a "real coordinate space" has already a finite dimension, so maybe we should call ( RR^ ` n ) a "generalized real coordinate space" and (EEhil ` n ) a "real coordinate space". Or maybe EEhil can be removed from set.mm ((EEhil ` N ) is simply ( RR^ ` ( 1 ... N ) )) - there are only a few theorems using this definition...

[tirix]

985 has a discussion about the naming of EEhil:

That EE notation was originally from Scott Fenton, denominating the base, and I have defined EEhil because this is the Hilbert Space structure corresponding to the base EE, similarly to what RRfld is to RR: a field structure enriching the base RR.

The definitions EE and EEhil both actually still refers to real coordinate spaces, of finite dimensions, so unfortunately at the light of Benoît's remark, I believe both notation and naming should be improved here, if we reserve the name "Euclidean Space" for generic spaces.

Based on @benjub and @digama0 maybe we could use the following notations:

• RR^() instead the current RR^, to denote that it's a direct product.
• RR^ instead of EE
• RRhilˆ instead of EEhil, for example?

[benjub]

Thanks for the comments @avekens and @tirix. I would say:

• df-rrx : RR^() (since it is a direct sum and not a direct product); no need for a name in my opinion (if you insist, then "real coordinate space" is ok); displayed $\mathbb{R}^{\wedge (-)}$ or $\mathbb{R}_\mathrm{eucl}^{\wedge (-)}$ (maybe replace the dash with a space) ; maybe add "eucl" ? (I would not use "hil" which is strongly associated with completeness, since RR^() need not be complete)
• df-ehl : something like RReucl^; no need for a name, it's simply "R to the n endowed with its standard Euclidean structure"; displayed $\mathbb{R}_\mathrm{eucl}^{\wedge}$
• df-ee: RR^; no need for a name, it's simply "R to the n"; displayed $\mathbb{R}^{\wedge}$

[avekens]

I agree with the definitions and symbols. But the labels should be changed, too: maybe df-rrx -> df-rrneucl (called"real coordinate space"), df-ehl -> df-rrfineucl (called "finite-dimensional real coordinate space"), df-ee -> df-rr or df-rrn (there is, however, a definition of an Euclidean space (another one!) with the label df-rrn in JM's mathbox).

I would like to have descriptive names for these constructs, and my proposals above are close to their usage in Wikipedia, mentioned by Thierry.

Maybe the definition df-ee could be moved up in set.mm near to the other definitions.

[benjub]

@avekens you're right, labels should be changed too (and this may imply changing the corresponding "sublabel" in other statements, e.g. rrxval -> NEWLABELABBREVIATIONval. In the balance to find between short and explicit labels, I think we should aim for shorter ones than the ones you give. Haven't thought much about proposals... Maybe df-rrn / df-rreuc / df-rrgeuc (I'm not happy with the last one...) ?

As for the one in the mathbox, it seems to follow the older way of defining structures only by some operation (e.g., the group law gives back the underlying set as the domain of the group law, so a group was defined only by its group law), and it is superseded by the definitions in the main part, so we should used whatever we need for the notions in the main part, and in case of clashes, modify the mathbox.

As for moving up the current "df-ee" (soon to be df-rrn) RR^, I agree: move the few most basic results about it right before the definition of RR^(). We can "subsubsection" it to have one definition per subsubsection. Then we can do a second pass to modify the TOC if necessary.

Let's not hurry to do the PR. We're progressively reaching an agreement here so let's continue this nice way of working.

[tirix]

Also adding here a reference to #52, which is related.