Theorem seq1hcau

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

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	baib	$$⊢F:\mathbb{N}⟶\mathscr{H}\to \left(F\in \mathrm{Cauchy}\leftrightarrow \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)$$