HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-hnorm Unicode version

Definition df-hnorm 21509
Description: Define the function for the norm of a vector of Hilbert space. See normval 21664 for its value and normcl 21665 for its closure. Theorems norm-i-i 21673, norm-ii-i 21677, and norm-iii-i 21679 show it has the expected properties of a norm. In the literature, the norm of  A is usually written "||  A ||", 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.)
Assertion
Ref Expression
df-hnorm  |-  normh  =  ( x  e.  dom  dom  .ih  |->  ( sqr `  (
x  .ih  x )
) )

Detailed syntax breakdown of Definition df-hnorm
StepHypRef Expression
1 cno 21464 . 2  class  normh
2 vx . . 3  set  x
3 csp 21463 . . . . 5  class  .ih
43cdm 4661 . . . 4  class  dom  .ih
54cdm 4661 . . 3  class  dom  dom  .ih
62cv 1618 . . . . 5  class  x
76, 6, 3co 5792 . . . 4  class  ( x 
.ih  x )
8 csqr 11684 . . . 4  class  sqr
97, 8cfv 4673 . . 3  class  ( sqr `  ( x  .ih  x
) )
102, 5, 9cmpt 4051 . 2  class  ( x  e.  dom  dom  .ih  |->  ( sqr `  ( x 
.ih  x ) ) )
111, 10wceq 1619 1  wff  normh  =  ( x  e.  dom  dom  .ih  |->  ( sqr `  (
x  .ih  x )
) )
Colors of variables: wff set class
This definition is referenced by:  dfhnorm2  21662
  Copyright terms: Public domain W3C validator