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

Definition df-ch 21726
Description: Define the set of closed subspaces of a Hilbert space. A closed subspace is one in which the limit of every convergent sequence in the subspace belongs to the subspace. For its membership relation, see isch 21727. From Definition of [Beran] p. 107. Alternate definitions are given by isch2 21728 and isch3 21746. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.)
Assertion
Ref Expression
df-ch  |-  CH  =  { h  e.  SH  |  (  ~~>v  " (
h  ^m  NN )
)  C_  h }

Detailed syntax breakdown of Definition df-ch
StepHypRef Expression
1 cch 21434 . 2  class  CH
2 chli 21432 . . . . 5  class  ~~>v
3 vh . . . . . . 7  set  h
43cv 1618 . . . . . 6  class  h
5 cn 9679 . . . . . 6  class  NN
6 cmap 6705 . . . . . 6  class  ^m
74, 5, 6co 5757 . . . . 5  class  ( h  ^m  NN )
82, 7cima 4629 . . . 4  class  (  ~~>v  "
( h  ^m  NN ) )
98, 4wss 3094 . . 3  wff  (  ~~>v  "
( h  ^m  NN ) )  C_  h
10 csh 21433 . . 3  class  SH
119, 3, 10crab 2519 . 2  class  { h  e.  SH  |  (  ~~>v  "
( h  ^m  NN ) )  C_  h }
121, 11wceq 1619 1  wff  CH  =  { h  e.  SH  |  (  ~~>v  " (
h  ^m  NN )
)  C_  h }
Colors of variables: wff set class
This definition is referenced by:  isch  21727
  Copyright terms: Public domain W3C validator