This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ↦ ( ℝ^ ‘ ( 1 ... 𝑛 ) ) )

Detailed syntax breakdown

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