HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-ch 10725
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 10726. From Definition of [Beran] p. 107. Alternate definitions are given by chcmhi 10746 and dfch2 10882.
Assertion
Ref Expression
df-ch |- CH = {h | (h e. SH /\ A.fA.x((f:NN-->h /\ f ~~>v x) -> x e. h))}
Distinct variable group:   x,f,h

Detailed syntax breakdown of Definition df-ch
StepHypRef Expression
1 cch 10430 . 2 class CH
2 vh . . . . . 6 set h
32cv 1297 . . . . 5 class h
4 csh 10429 . . . . 5 class SH
53, 4wcel 1300 . . . 4 wff h e. SH
6 cn 6449 . . . . . . . . 9 class NN
7 vf . . . . . . . . . 10 set f
87cv 1297 . . . . . . . . 9 class f
96, 3, 8wf 3994 . . . . . . . 8 wff f:NN-->h
10 vx . . . . . . . . . 10 set x
1110cv 1297 . . . . . . . . 9 class x
12 chli 10428 . . . . . . . . 9 class ~~>v
138, 11, 12wbr 3338 . . . . . . . 8 wff f ~~>v x
149, 13wa 240 . . . . . . 7 wff (f:NN-->h /\ f ~~>v x)
1511, 3wcel 1300 . . . . . . 7 wff x e. h
1614, 15wi 3 . . . . . 6 wff ((f:NN-->h /\ f ~~>v x) -> x e. h)
1716, 10wal 1296 . . . . 5 wff A.x((f:NN-->h /\ f ~~>v x) -> x e. h)
1817, 7wal 1296 . . . 4 wff A.fA.x((f:NN-->h /\ f ~~>v x) -> x e. h)
195, 18wa 240 . . 3 wff (h e. SH /\ A.fA.x((f:NN-->h /\ f ~~>v x) -> x e. h))
2019, 2cab 1871 . 2 class {h | (h e. SH /\ A.fA.x((f:NN-->h /\ f ~~>v x) -> x e. h))}
211, 20wceq 1298 1 wff CH = {h | (h e. SH /\ A.fA.x((f:NN-->h /\ f ~~>v x) -> x e. h))}
Colors of variables: wff set class
This definition is referenced by:  closedsub 10726  chsssh 10727
Copyright terms: Public domain