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

Axiom ax-hcompl 11540
Description: Completeness of a Hilbert space.
Assertion
Ref Expression
ax-hcompl |- (F e. Cauchy -> E.x e. ~H F ~~>v x)
Distinct variable group:   x,F

Detailed syntax breakdown of Axiom ax-hcompl
StepHypRef Expression
1 cF . . 3 class F
2 ccau 11265 . . 3 class Cauchy
31, 2wcel 1588 . 2 wff F e. Cauchy
4 vx . . . . 5 set x
54cv 1585 . . . 4 class x
6 chli 11266 . . . 4 class ~~>v
71, 5, 6wbr 3507 . . 3 wff F ~~>v x
8 chil 11258 . . 3 class ~H
97, 4, 8wrex 2356 . 2 wff E.x e. ~H F ~~>v x
103, 9wi 3 1 wff (F e. Cauchy -> E.x e. ~H F ~~>v x)
Colors of variables: wff set class
This axiom is referenced by:  hhcms 11541  chsscmi 11579
Copyright terms: Public domain