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 ℋ = h ∈ S ℋ | ⇝v h ℕ ⊆ h

Detailed syntax breakdown

Step Hyp Ref Expression
0 cch class C ℋ
1 vh setvar h
2 csh class S ℋ
3 chli class ⇝v
4 1 cv setvar h
5 cmap class ↑ 𝑚
6 cn class ℕ
7 4 6 5 co class h ℕ
8 3 7 cima class ⇝v h ℕ
9 8 4 wss wff ⇝v h ℕ ⊆ h
10 9 1 2 crab class h ∈ S ℋ | ⇝v h ℕ ⊆ h
11 0 10 wceq wff C ℋ = h ∈ S ℋ | ⇝v h ℕ ⊆ h