Definition df-ehl 24455

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 24486). 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 24453	. 2 class 𝔼hil
2		vn	. . 3 setvar 𝑛
3		cn0 12163	. . 3 class ℕ0
4		c1 10803	. . . . 5 class 1
5	2	cv 1538	. . . . 5 class 𝑛
6		cfz 13168	. . . . 5 class ...
7	4, 5, 6	co 7255	. . . 4 class (1...𝑛)
8		crrx 24452	. . . 4 class ℝ^
9	7, 8	cfv 6418	. . 3 class (ℝ^‘(1...𝑛))
10	2, 3, 9	cmpt 5153	. 2 class (𝑛 ∈ ℕ0 ↦ (ℝ^‘(1...𝑛)))
11	1, 10	wceq 1539	1 wff 𝔼hil = (𝑛 ∈ ℕ0 ↦ (ℝ^‘(1...𝑛)))

This definition is referenced by:  ehlval  24483