This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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