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

Definition df-ch 21631
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 21632. From Definition of [Beran] p. 107. Alternate definitions are given by isch2 21633 and isch3 21651. (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 21339 . 2  class  CH
2 chli 21337 . . . . 5  class  ~~>v
3 vh . . . . . . 7  set  h
43cv 1618 . . . . . 6  class  h
5 cn 9626 . . . . . 6  class  NN
6 cmap 6658 . . . . . 6  class  ^m
74, 5, 6co 5710 . . . . 5  class  ( h  ^m  NN )
82, 7cima 4583 . . . 4  class  (  ~~>v  "
( h  ^m  NN ) )
98, 4wss 3078 . . 3  wff  (  ~~>v  "
( h  ^m  NN ) )  C_  h
10 csh 21338 . . 3  class  SH
119, 3, 10crab 2512 . 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  21632
  Copyright terms: Public domain W3C validator