This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 Cauchy \to F : ℕ ⟶ ℋ$

Proof

Step	Hyp	Ref	Expression
1		hcau	$⊢ F \in Cauchy \leftrightarrow (F : ℕ ⟶ ℋ \land \forall x \in ℝ^{+} \exists y \in ℕ \forall z \in ℤ_{\geq y} {norm}_{ℎ} (F (y) -_{ℎ} F (z)) < x)$
2	1	simplbi	$⊢ F \in Cauchy \to F : ℕ ⟶ ℋ$