Definition df-ch 9013

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 closedsub 9014. From Definition of [Beran] p. 107. Alternate definitions are given by chcmh 9034 and dfch2 9164.

Assertion

Ref	Expression
df-ch	⊢ Cℋ = {h∣(h ∈ Sℋ ⋀ ∀f∀x((f:ℕ–→h ⋀ f ⇝v x) → x ∈ h))}

Distinct variable group:   x,f,h

Detailed syntax breakdown of Definition df-ch

Step	Hyp	Ref	Expression
1		cch 8737	. 2 class Cℋ
2		vh	. . . . . 6 set h
3	2	cv 952	. . . . 5 class h
4		csh 8736	. . . . 5 class Sℋ
5	3, 4	wcel 955	. . . 4 wff h ∈ Sℋ
6		cn 5268	. . . . . . . . 9 class ℕ
7		vf	. . . . . . . . . 10 set f
8	7	cv 952	. . . . . . . . 9 class f
9	6, 3, 8	wf 3168	. . . . . . . 8 wff f:ℕ–→h
10		vx	. . . . . . . . . 10 set x
11	10	cv 952	. . . . . . . . 9 class x
12		chli 8735	. . . . . . . . 9 class ⇝v
13	8, 11, 12	wbr 2609	. . . . . . . 8 wff f ⇝v x
14	9, 13	wa 223	. . . . . . 7 wff (f:ℕ–→h ⋀ f ⇝v x)
15	11, 3	wcel 955	. . . . . . 7 wff x ∈ h
16	14, 15	wi 3	. . . . . 6 wff ((f:ℕ–→h ⋀ f ⇝v x) → x ∈ h)
17	16, 10	wal 951	. . . . 5 wff ∀x((f:ℕ–→h ⋀ f ⇝v x) → x ∈ h)
18	17, 7	wal 951	. . . 4 wff ∀f∀x((f:ℕ–→h ⋀ f ⇝v x) → x ∈ h)
19	5, 18	wa 223	. . 3 wff (h ∈ Sℋ ⋀ ∀f∀x((f:ℕ–→h ⋀ f ⇝v x) → x ∈ h))
20	19, 2	cab 1456	. 2 class {h∣(h ∈ Sℋ ⋀ ∀f∀x((f:ℕ–→h ⋀ f ⇝v x) → x ∈ h))}
21	1, 20	wceq 953	1 wff Cℋ = {h∣(h ∈ Sℋ ⋀ ∀f∀x((f:ℕ–→h ⋀ f ⇝v x) → x ∈ h))}

This definition is referenced by:  closedsub 9014  chsssh 9015

Copyright terms: Public domain