This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 }