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

Definition df-bdop 23194
Description: Define the set of bounded linear Hilbert space operators. (See df-hosum 23082 for definition of operator.) (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-bdop  |-  BndLinOp  =  {
t  e.  LinOp  |  (
normop `  t )  <  +oo }

Detailed syntax breakdown of Definition df-bdop
StepHypRef Expression
1 cbo 22300 . 2  class  BndLinOp
2 vt . . . . . 6  set  t
32cv 1648 . . . . 5  class  t
4 cnop 22297 . . . . 5  class  normop
53, 4cfv 5395 . . . 4  class  ( normop `  t )
6 cpnf 9051 . . . 4  class  +oo
7 clt 9054 . . . 4  class  <
85, 6, 7wbr 4154 . . 3  wff  ( normop `  t )  <  +oo
9 clo 22299 . . 3  class  LinOp
108, 2, 9crab 2654 . 2  class  { t  e.  LinOp  |  ( normop `  t )  <  +oo }
111, 10wceq 1649 1  wff  BndLinOp  =  {
t  e.  LinOp  |  (
normop `  t )  <  +oo }
Colors of variables: wff set class
This definition is referenced by:  elbdop  23212  hhbloi  23254
  Copyright terms: Public domain W3C validator