MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ehl Structured version   Visualization version   GIF version

Definition df-ehl 24539
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 24570). 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
StepHypRef Expression
1 cehl 24537 . 2 class 𝔼hil
2 vn . . 3 setvar 𝑛
3 cn0 12222 . . 3 class 0
4 c1 10861 . . . . 5 class 1
52cv 1538 . . . . 5 class 𝑛
6 cfz 13228 . . . . 5 class ...
74, 5, 6co 7269 . . . 4 class (1...𝑛)
8 crrx 24536 . . . 4 class ℝ^
97, 8cfv 6428 . . 3 class (ℝ^‘(1...𝑛))
102, 3, 9cmpt 5158 . 2 class (𝑛 ∈ ℕ0 ↦ (ℝ^‘(1...𝑛)))
111, 10wceq 1539 1 wff 𝔼hil = (𝑛 ∈ ℕ0 ↦ (ℝ^‘(1...𝑛)))
Colors of variables: wff setvar class
This definition is referenced by:  ehlval  24567
  Copyright terms: Public domain W3C validator