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

Definition df-bdop 23337
Description: Define the set of bounded linear Hilbert space operators. (See df-hosum 23225 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 22443 . 2  class  BndLinOp
2 vt . . . . . 6  set  t
32cv 1651 . . . . 5  class  t
4 cnop 22440 . . . . 5  class  normop
53, 4cfv 5446 . . . 4  class  ( normop `  t )
6 cpnf 9109 . . . 4  class  +oo
7 clt 9112 . . . 4  class  <
85, 6, 7wbr 4204 . . 3  wff  ( normop `  t )  <  +oo
9 clo 22442 . . 3  class  LinOp
108, 2, 9crab 2701 . 2  class  { t  e.  LinOp  |  ( normop `  t )  <  +oo }
111, 10wceq 1652 1  wff  BndLinOp  =  {
t  e.  LinOp  |  (
normop `  t )  <  +oo }
Colors of variables: wff set class
This definition is referenced by:  elbdop  23355  hhbloi  23397
  Copyright terms: Public domain W3C validator