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 29159 for its value and normcl 29160 for its closure. Theorems norm-i-i 29168, norm-ii-i 29172, and norm-iii-i 29174 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 28958 | . 2 class normℎ | |
2 | vx | . . 3 setvar 𝑥 | |
3 | csp 28957 | . . . . 5 class ·ih | |
4 | 3 | cdm 5536 | . . . 4 class dom ·ih |
5 | 4 | cdm 5536 | . . 3 class dom dom ·ih |
6 | 2 | cv 1542 | . . . . 5 class 𝑥 |
7 | 6, 6, 3 | co 7191 | . . . 4 class (𝑥 ·ih 𝑥) |
8 | csqrt 14761 | . . . 4 class √ | |
9 | 7, 8 | cfv 6358 | . . 3 class (√‘(𝑥 ·ih 𝑥)) |
10 | 2, 5, 9 | cmpt 5120 | . 2 class (𝑥 ∈ dom dom ·ih ↦ (√‘(𝑥 ·ih 𝑥))) |
11 | 1, 10 | wceq 1543 | 1 wff normℎ = (𝑥 ∈ dom dom ·ih ↦ (√‘(𝑥 ·ih 𝑥))) |
Colors of variables: wff setvar class |
This definition is referenced by: dfhnorm2 29157 |
Copyright terms: Public domain | W3C validator |