Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > df-hnorm | Structured version Visualization version Unicode version |
Description: Define the function for the norm of a vector of Hilbert space. See normval 27981 for its value and normcl 27982 for its closure. Theorems norm-i-i 27990, norm-ii-i 27994, and norm-iii-i 27996 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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cno 27780 | . 2 | |
2 | vx | . . 3 | |
3 | csp 27779 | . . . . 5 | |
4 | 3 | cdm 5114 | . . . 4 |
5 | 4 | cdm 5114 | . . 3 |
6 | 2 | cv 1482 | . . . . 5 |
7 | 6, 6, 3 | co 6650 | . . . 4 |
8 | csqrt 13973 | . . . 4 | |
9 | 7, 8 | cfv 5888 | . . 3 |
10 | 2, 5, 9 | cmpt 4729 | . 2 |
11 | 1, 10 | wceq 1483 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: dfhnorm2 27979 |
Copyright terms: Public domain | W3C validator |