Definition df-ehl 25338

Description: Define a function generating the real Euclidean spaces of finite dimension. The case 𝑛 = 0 corresponds to a space of dimension 0, that is, limited to a neutral element (see ehl0 25369). 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 = (𝑛 ∈ ℕ0 ↦ (ℝ^‘(1...𝑛)))

Detailed syntax breakdown of Definition df-ehl

Step	Hyp	Ref	Expression
1		cehl 25336	. 2 class 𝔼hil
2		vn	. . 3 setvar 𝑛
3		cn0 12501	. . 3 class ℕ0
4		c1 11130	. . . . 5 class 1
5	2	cv 1539	. . . . 5 class 𝑛
6		cfz 13524	. . . . 5 class ...
7	4, 5, 6	co 7405	. . . 4 class (1...𝑛)
8		crrx 25335	. . . 4 class ℝ^
9	7, 8	cfv 6531	. . 3 class (ℝ^‘(1...𝑛))
10	2, 3, 9	cmpt 5201	. 2 class (𝑛 ∈ ℕ0 ↦ (ℝ^‘(1...𝑛)))
11	1, 10	wceq 1540	1 wff 𝔼hil = (𝑛 ∈ ℕ0 ↦ (ℝ^‘(1...𝑛)))

This definition is referenced by:  ehlval  25366