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

Definition df-bdop 22252
Description: Define the set of bounded linear Hilbert space operators. (See df-hosum 21992 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 21358 . 2  class  BndLinOp
2 vt . . . . . 6  set  t
32cv 1618 . . . . 5  class  t
4 cnop 21355 . . . . 5  class  normop
53, 4cfv 4592 . . . 4  class  ( normop `  t )
6 cpnf 8744 . . . 4  class  +oo
7 clt 8747 . . . 4  class  <
85, 6, 7wbr 3920 . . 3  wff  ( normop `  t )  <  +oo
9 clo 21357 . . 3  class  LinOp
108, 2, 9crab 2512 . 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  22270  hhbloi  22312
  Copyright terms: Public domain W3C validator