Of course, you can define a (finite-dimensional) Euclidean space as a direct sum or a direct product since, they are equal for a finite number of summands/factors. I think the present definition is better, since in the infinite case, you can define an inner product on a direct sum, but not on a direct product.
As for the unicode symbol for the direct sum of copies of \R, I would use Mario's suggestion from a previous thread, i.e. R^() instead of R^. This would free up the symbol R^ to be used for the direct product. Benoit -- 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/a36d3f23-52e7-4636-b838-f0dfab5853e3%40googlegroups.com.
