Definition df-ehl 23174

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. Members of this family of spaces are Hilbert spaces, as shown in - ehlhl . (Contributed by Thierry Arnoux, 16-Jun-2019.)

Assertion

Ref	Expression
df-ehl	|- 𝔼hil = ( n e. NN0 |-> (ℝ^ ` ( 1 ... n ) ) )

Detailed syntax breakdown of Definition df-ehl

Step	Hyp	Ref	Expression
1		cehl 23172	. 2 class 𝔼hil
2		vn	. . 3 setvar n
3		cn0 11292	. . 3 class NN0
4		c1 9937	. . . . 5 class 1
5	2	cv 1482	. . . . 5 class n
6		cfz 12326	. . . . 5 class ...
7	4, 5, 6	co 6650	. . . 4 class ( 1 ... n )
8		crrx 23171	. . . 4 class ℝ^
9	7, 8	cfv 5888	. . 3 class (ℝ^ ` ( 1 ... n ) )
10	2, 3, 9	cmpt 4729	. 2 class ( n e. NN0 |-> (ℝ^ ` ( 1 ... n ) ) )
11	1, 10	wceq 1483	1 wff 𝔼hil = ( n e. NN0 |-> (ℝ^ ` ( 1 ... n ) ) )

This definition is referenced by:  ehlval  23193