Definition df-ehl 22982

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. 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 22980	. 2 class 𝔼hil
2		vn	. . 3 setvar 𝑛
3		cn0 11169	. . 3 class ℕ0
4		c1 9816	. . . . 5 class 1
5	2	cv 1474	. . . . 5 class 𝑛
6		cfz 12197	. . . . 5 class ...
7	4, 5, 6	co 6549	. . . 4 class (1...𝑛)
8		crrx 22979	. . . 4 class ℝ^
9	7, 8	cfv 5804	. . 3 class (ℝ^‘(1...𝑛))
10	2, 3, 9	cmpt 4643	. 2 class (𝑛 ∈ ℕ0 ↦ (ℝ^‘(1...𝑛)))
11	1, 10	wceq 1475	1 wff 𝔼hil = (𝑛 ∈ ℕ0 ↦ (ℝ^‘(1...𝑛)))

This definition is referenced by:  ehlval  23001