Definition df-ehl 25420

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 25451). 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 25418	. 2 class 𝔼hil
2		vn	. . 3 setvar 𝑛
3		cn0 12526	. . 3 class ℕ0
4		c1 11156	. . . . 5 class 1
5	2	cv 1539	. . . . 5 class 𝑛
6		cfz 13547	. . . . 5 class ...
7	4, 5, 6	co 7431	. . . 4 class (1...𝑛)
8		crrx 25417	. . . 4 class ℝ^
9	7, 8	cfv 6561	. . 3 class (ℝ^‘(1...𝑛))
10	2, 3, 9	cmpt 5225	. 2 class (𝑛 ∈ ℕ0 ↦ (ℝ^‘(1...𝑛)))
11	1, 10	wceq 1540	1 wff 𝔼hil = (𝑛 ∈ ℕ0 ↦ (ℝ^‘(1...𝑛)))

This definition is referenced by:  ehlval  25448