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	⊢ Cℋ = { ℎ ∈ Sℋ ∣ ( ⇝𝑣 “ ( ℎ ↑m ℕ ) ) ⊆ ℎ }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cch	⊢ Cℋ
1		vh	⊢ ℎ
2		csh	⊢ Sℋ
3		chli	⊢ ⇝𝑣
4	1	cv	⊢ ℎ
5		cmap	⊢ ↑m
6		cn	⊢ ℕ
7	4 6 5	co	⊢ ( ℎ ↑m ℕ )
8	3 7	cima	⊢ ( ⇝𝑣 “ ( ℎ ↑m ℕ ) )
9	8 4	wss	⊢ ( ⇝𝑣 “ ( ℎ ↑m ℕ ) ) ⊆ ℎ
10	9 1 2	crab	⊢ { ℎ ∈ Sℋ ∣ ( ⇝𝑣 “ ( ℎ ↑m ℕ ) ) ⊆ ℎ }
11	0 10	wceq	⊢ Cℋ = { ℎ ∈ Sℋ ∣ ( ⇝𝑣 “ ( ℎ ↑m ℕ ) ) ⊆ ℎ }