Definition df-ch 28078

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 28079. From Definition of [Beran] p. 107. Alternate definitions are given by isch2 28080 and isch3 28098. (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

Step	Hyp	Ref	Expression
1		cch 27786	. 2 class CH
2		chli 27784	. . . . 5 class ~~>v
3		vh	. . . . . . 7 setvar h
4	3	cv 1482	. . . . . 6 class h
5		cn 11020	. . . . . 6 class NN
6		cmap 7857	. . . . . 6 class ^m
7	4, 5, 6	co 6650	. . . . 5 class ( h ^m NN )
8	2, 7	cima 5117	. . . 4 class ( ~~>v " ( h ^m NN ) )
9	8, 4	wss 3574	. . 3 wff ( ~~>v " ( h ^m NN ) ) C_ h
10		csh 27785	. . 3 class SH
11	9, 3, 10	crab 2916	. 2 class { h e. SH | ( ~~>v " ( h ^m NN ) ) C_ h }
12	1, 11	wceq 1483	1 wff CH = { h e. SH | ( ~~>v " ( h ^m NN ) ) C_ h }

This definition is referenced by:  isch  28079