Description: A sequence on a Hilbert space is a Cauchy sequence if it converges. (Contributed by NM, 16-Aug-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | seq1hcau | |- ( F : NN --> ~H -> ( F e. Cauchy <-> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hcau | |- ( F e. Cauchy <-> ( F : NN --> ~H /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) ) |
|
2 | 1 | baib | |- ( F : NN --> ~H -> ( F e. Cauchy <-> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) ) |