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

Definition df-bdop 22368
Description: Define the set of bounded linear Hilbert space operators. (See df-hosum 22108 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 21474 . 2  class  BndLinOp
2 vt . . . . . 6  set  t
32cv 1618 . . . . 5  class  t
4 cnop 21471 . . . . 5  class  normop
53, 4cfv 4659 . . . 4  class  ( normop `  t )
6 cpnf 8818 . . . 4  class  +oo
7 clt 8821 . . . 4  class  <
85, 6, 7wbr 3983 . . 3  wff  ( normop `  t )  <  +oo
9 clo 21473 . . 3  class  LinOp
108, 2, 9crab 2520 . 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  22386  hhbloi  22428
  Copyright terms: Public domain W3C validator