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

Definition df-ch 21801
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 21802. From Definition of [Beran] p. 107. Alternate definitions are given by isch2 21803 and isch3 21821. (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 21509 . 2  class  CH
2 chli 21507 . . . . 5  class  ~~>v
3 vh . . . . . . 7  set  h
43cv 1622 . . . . . 6  class  h
5 cn 9746 . . . . . 6  class  NN
6 cmap 6772 . . . . . 6  class  ^m
74, 5, 6co 5858 . . . . 5  class  ( h  ^m  NN )
82, 7cima 4692 . . . 4  class  (  ~~>v  "
( h  ^m  NN ) )
98, 4wss 3152 . . 3  wff  (  ~~>v  "
( h  ^m  NN ) )  C_  h
10 csh 21508 . . 3  class  SH
119, 3, 10crab 2547 . 2  class  { h  e.  SH  |  (  ~~>v  "
( h  ^m  NN ) )  C_  h }
121, 11wceq 1623 1  wff  CH  =  { h  e.  SH  |  (  ~~>v  " (
h  ^m  NN )
)  C_  h }
Colors of variables: wff set class
This definition is referenced by:  isch  21802
  Copyright terms: Public domain W3C validator