Definition df-ch 27462

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

Assertion

Ref	Expression
df-ch	⊢ Cℋ = {ℎ ∈ Sℋ ∣ ( ⇝𝑣 “ (ℎ ↑𝑚 ℕ)) ⊆ ℎ}

Detailed syntax breakdown of Definition df-ch

Step	Hyp	Ref	Expression
1		cch 27170	. 2 class Cℋ
2		chli 27168	. . . . 5 class ⇝𝑣
3		vh	. . . . . . 7 setvar ℎ
4	3	cv 1474	. . . . . 6 class ℎ
5		cn 10897	. . . . . 6 class ℕ
6		cmap 7744	. . . . . 6 class ↑𝑚
7	4, 5, 6	co 6549	. . . . 5 class (ℎ ↑𝑚 ℕ)
8	2, 7	cima 5041	. . . 4 class ( ⇝𝑣 “ (ℎ ↑𝑚 ℕ))
9	8, 4	wss 3540	. . 3 wff ( ⇝𝑣 “ (ℎ ↑𝑚 ℕ)) ⊆ ℎ
10		csh 27169	. . 3 class Sℋ
11	9, 3, 10	crab 2900	. 2 class {ℎ ∈ Sℋ ∣ ( ⇝𝑣 “ (ℎ ↑𝑚 ℕ)) ⊆ ℎ}
12	1, 11	wceq 1475	1 wff Cℋ = {ℎ ∈ Sℋ ∣ ( ⇝𝑣 “ (ℎ ↑𝑚 ℕ)) ⊆ ℎ}

This definition is referenced by:  isch  27463