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

Definition df-bdop 22347
Description: Define the set of bounded linear Hilbert space operators. (See df-hosum 22087 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 21453 . 2  class  BndLinOp
2 vt . . . . . 6  set  t
32cv 1618 . . . . 5  class  t
4 cnop 21450 . . . . 5  class  normop
53, 4cfv 4638 . . . 4  class  ( normop `  t )
6 cpnf 8797 . . . 4  class  +oo
7 clt 8800 . . . 4  class  <
85, 6, 7wbr 3963 . . 3  wff  ( normop `  t )  <  +oo
9 clo 21452 . . 3  class  LinOp
108, 2, 9crab 2519 . 2  class  { t  e.  LinOp  |  ( normop `  t )  <  +oo }
111, 10wceq 1619 1  wff  BndLinOp  =  {
t  e.  LinOp  |  (
normop `  t )  <  +oo }
Colors of variables: wff set class
This definition is referenced by:  elbdop  22365  hhbloi  22407
  Copyright terms: Public domain W3C validator