Definition df-ehl

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

	Ref	Expression
Assertion	df-ehl	⊢ 𝔼hil = ( 𝑛 ∈ ℕ0 ↦ ( ℝ^ ‘ ( 0 ..^ 𝑛 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cehl	⊢ 𝔼hil
1		vn	⊢ 𝑛
2		cn0	⊢ ℕ0
3		crrx	⊢ ℝ^
4		cc0	⊢ 0
5		cfzo	⊢ ..^
6	1	cv	⊢ 𝑛
7	4 6 5	co	⊢ ( 0 ..^ 𝑛 )
8	7 3	cfv	⊢ ( ℝ^ ‘ ( 0 ..^ 𝑛 ) )
9	1 2 8	cmpt	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ℝ^ ‘ ( 0 ..^ 𝑛 ) ) )
10	0 9	wceq	⊢ 𝔼hil = ( 𝑛 ∈ ℕ0 ↦ ( ℝ^ ‘ ( 0 ..^ 𝑛 ) ) )