Definition df-ehl

Description: Define a function generating the real Euclidean spaces of finite dimension. The case n = 0 corresponds to a space of dimension 0, that is, limited to a neutral element (see ehl0 ). Members of this family of spaces are Hilbert spaces, as shown in - ehlhl . (Contributed by Thierry Arnoux, 16-Jun-2019)

	Ref	Expression
Assertion	df-ehl

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cehl	$$class{𝔼}_{\mathrm{hil}}$$
1		vn	$$setvarn$$
2		cn0	$$class{\mathbb{N}}_0$$
3		crrx	$$class\mathrm{ℝ\uparrow }$$
4		c1	$$class1$$
5		cfz	$$class\dots$$
6	1	cv	$$setvarn$$
7	4 6 5	co	$$class\left(1\dots n\right)$$
8	7 3	cfv
9	1 2 8	cmpt
10	0 9	wceq