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\in \mathrm{Cauchy}\to F:\mathbb{N}⟶\mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		hcau	$$⊢F\in \mathrm{Cauchy}\leftrightarrow \left(F:\mathbb{N}⟶\mathscr{H}\wedge \forall x\in {ℝ}^{+}\exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(F\left(y\right){-}_{ℎ}F\left(z\right)\right)<x\right)$$
2	1	simplbi	$$⊢F\in \mathrm{Cauchy}\to F:\mathbb{N}⟶\mathscr{H}$$