Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-ehl | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-ehl | ⊢ 𝔼hil = (𝑛 ∈ ℕ0 ↦ (ℝ^‘(1...𝑛))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cehl 24537 | . 2 class 𝔼hil | |
2 | vn | . . 3 setvar 𝑛 | |
3 | cn0 12222 | . . 3 class ℕ0 | |
4 | c1 10861 | . . . . 5 class 1 | |
5 | 2 | cv 1538 | . . . . 5 class 𝑛 |
6 | cfz 13228 | . . . . 5 class ... | |
7 | 4, 5, 6 | co 7269 | . . . 4 class (1...𝑛) |
8 | crrx 24536 | . . . 4 class ℝ^ | |
9 | 7, 8 | cfv 6428 | . . 3 class (ℝ^‘(1...𝑛)) |
10 | 2, 3, 9 | cmpt 5158 | . 2 class (𝑛 ∈ ℕ0 ↦ (ℝ^‘(1...𝑛))) |
11 | 1, 10 | wceq 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 |