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

Definition df-sh 26241
Description: Define the set of subspaces of a Hilbert space. See issh 26242 for its membership relation. Basically, a subspace is a subset of a Hilbert space that acts like a vector space. From Definition of [Beran] p. 95. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
Assertion
Ref Expression
df-sh  |-  SH  =  { h  e.  ~P ~H  |  ( 0h  e.  h  /\  (  +h  " ( h  X.  h ) )  C_  h  /\  (  .h  "
( CC  X.  h
) )  C_  h
) }

Detailed syntax breakdown of Definition df-sh
StepHypRef Expression
1 csh 25962 . 2  class  SH
2 c0v 25958 . . . . 5  class  0h
3 vh . . . . . 6  setvar  h
43cv 1398 . . . . 5  class  h
52, 4wcel 1826 . . . 4  wff  0h  e.  h
6 cva 25954 . . . . . 6  class  +h
74, 4cxp 4911 . . . . . 6  class  ( h  X.  h )
86, 7cima 4916 . . . . 5  class  (  +h  " ( h  X.  h ) )
98, 4wss 3389 . . . 4  wff  (  +h  " ( h  X.  h ) )  C_  h
10 csm 25955 . . . . . 6  class  .h
11 cc 9401 . . . . . . 7  class  CC
1211, 4cxp 4911 . . . . . 6  class  ( CC 
X.  h )
1310, 12cima 4916 . . . . 5  class  (  .h  " ( CC  X.  h ) )
1413, 4wss 3389 . . . 4  wff  (  .h  " ( CC  X.  h ) )  C_  h
155, 9, 14w3a 971 . . 3  wff  ( 0h  e.  h  /\  (  +h  " ( h  X.  h ) )  C_  h  /\  (  .h  "
( CC  X.  h
) )  C_  h
)
16 chil 25953 . . . 4  class  ~H
1716cpw 3927 . . 3  class  ~P ~H
1815, 3, 17crab 2736 . 2  class  { h  e.  ~P ~H  |  ( 0h  e.  h  /\  (  +h  " ( h  X.  h ) ) 
C_  h  /\  (  .h  " ( CC  X.  h ) )  C_  h ) }
191, 18wceq 1399 1  wff  SH  =  { h  e.  ~P ~H  |  ( 0h  e.  h  /\  (  +h  " ( h  X.  h ) )  C_  h  /\  (  .h  "
( CC  X.  h
) )  C_  h
) }
Colors of variables: wff setvar class
This definition is referenced by:  issh  26242
  Copyright terms: Public domain W3C validator