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

Definition df-ch 21795
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 21796. From Definition of [Beran] p. 107. Alternate definitions are given by isch2 21797 and isch3 21815. (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 21503 . 2  class  CH
2 chli 21501 . . . . 5  class  ~~>v
3 vh . . . . . . 7  set  h
43cv 1624 . . . . . 6  class  h
5 cn 9743 . . . . . 6  class  NN
6 cmap 6769 . . . . . 6  class  ^m
74, 5, 6co 5821 . . . . 5  class  ( h  ^m  NN )
82, 7cima 4693 . . . 4  class  (  ~~>v  "
( h  ^m  NN ) )
98, 4wss 3155 . . 3  wff  (  ~~>v  "
( h  ^m  NN ) )  C_  h
10 csh 21502 . . 3  class  SH
119, 3, 10crab 2550 . 2  class  { h  e.  SH  |  (  ~~>v  "
( h  ^m  NN ) )  C_  h }
121, 11wceq 1625 1  wff  CH  =  { h  e.  SH  |  (  ~~>v  " (
h  ^m  NN )
)  C_  h }
Colors of variables: wff set class
This definition is referenced by:  isch  21796
  Copyright terms: Public domain W3C validator