Definition df-ch

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 . From Definition of Beran p. 107. Alternate definitions are given by isch2 and isch3 . (Contributed by NM, 17-Aug-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	df-ch	|- CH = { h e. SH | ( ~~>v " ( h ^m NN ) ) C_ h }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cch	|- CH
1		vh	|- h
2		csh	|- SH
3		chli	|- ~~>v
4	1	cv	|- h
5		cmap	|- ^m
6		cn	|- NN
7	4 6 5	co	|- ( h ^m NN )
8	3 7	cima	|- ( ~~>v " ( h ^m NN ) )
9	8 4	wss	|- ( ~~>v " ( h ^m NN ) ) C_ h
10	9 1 2	crab	|- { h e. SH | ( ~~>v " ( h ^m NN ) ) C_ h }
11	0 10	wceq	|- CH = { h e. SH | ( ~~>v " ( h ^m NN ) ) C_ h }