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 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 ℕ ) ) ⊆ }