Theorem hcauseq

Description: A Cauchy sequences on a Hilbert space is a sequence. (Contributed by NM, 16-Aug-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	hcauseq	|- ( F e. Cauchy -> F : NN --> ~H )

Proof

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	simplbi	|- ( F e. Cauchy -> F : NN --> ~H )