![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > df-hnorm | Structured version Visualization version GIF version |
Description: Define the function for the norm of a vector of Hilbert space. See normval 27365 for its value and normcl 27366 for its closure. Theorems norm-i-i 27374, norm-ii-i 27378, and norm-iii-i 27380 show it has the expected properties of a norm. In the literature, the norm of 𝐴 is usually written "|| 𝐴 ||", but we use function notation to take advantage of our existing theorems about functions. Definition of norm in [Beran] p. 96. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
Ref | Expression |
---|---|
df-hnorm | ⊢ normℎ = (𝑥 ∈ dom dom ·ih ↦ (√‘(𝑥 ·ih 𝑥))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cno 27164 | . 2 class normℎ | |
2 | vx | . . 3 setvar 𝑥 | |
3 | csp 27163 | . . . . 5 class ·ih | |
4 | 3 | cdm 5038 | . . . 4 class dom ·ih |
5 | 4 | cdm 5038 | . . 3 class dom dom ·ih |
6 | 2 | cv 1474 | . . . . 5 class 𝑥 |
7 | 6, 6, 3 | co 6549 | . . . 4 class (𝑥 ·ih 𝑥) |
8 | csqrt 13821 | . . . 4 class √ | |
9 | 7, 8 | cfv 5804 | . . 3 class (√‘(𝑥 ·ih 𝑥)) |
10 | 2, 5, 9 | cmpt 4643 | . 2 class (𝑥 ∈ dom dom ·ih ↦ (√‘(𝑥 ·ih 𝑥))) |
11 | 1, 10 | wceq 1475 | 1 wff normℎ = (𝑥 ∈ dom dom ·ih ↦ (√‘(𝑥 ·ih 𝑥))) |
Colors of variables: wff setvar class |
This definition is referenced by: dfhnorm2 27363 |
Copyright terms: Public domain | W3C validator |