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	$$⊢{\mathbf{C}}_{\mathscr{H}}=\left\{h\in {\mathbf{S}}_{\mathscr{H}}|\underset{v}{⇝}\left[h^{\mathbb{N}}\right]\subseteq h\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cch	$$class{\mathbf{C}}_{\mathscr{H}}$$
1		vh	$$setvarh$$
2		csh	$$class{\mathbf{S}}_{\mathscr{H}}$$
3		chli	$$class\underset{v}{⇝}$$
4	1	cv	$$setvarh$$
5		cmap	$$class{\uparrow }_{𝑚}$$
6		cn	$$class\mathbb{N}$$
7	4 6 5	co	$$class\left(h^{\mathbb{N}}\right)$$
8	3 7	cima	$$class\underset{v}{⇝}\left[h^{\mathbb{N}}\right]$$
9	8 4	wss	$$wff\underset{v}{⇝}\left[h^{\mathbb{N}}\right]\subseteq h$$
10	9 1 2	crab	$$class\left\{h\in {\mathbf{S}}_{\mathscr{H}}|\underset{v}{⇝}\left[h^{\mathbb{N}}\right]\subseteq h\right\}$$
11	0 10	wceq	$$wff{\mathbf{C}}_{\mathscr{H}}=\left\{h\in {\mathbf{S}}_{\mathscr{H}}|\underset{v}{⇝}\left[h^{\mathbb{N}}\right]\subseteq h\right\}$$