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

Metamath Proof Explorer

Theorem hlimveci

Description: Closure of the limit of a sequence on Hilbert space. (Contributed by NM, 16-Aug-1999) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	hlim.1	$⊢ A \in V$
	Assertion	hlimveci	$⊢ F \underset{v}{⇝} A \to A \in ℋ$

Step	Hyp	Ref	Expression
1		hlim.1	$⊢ A \in V$
2	1	hlimi	$⊢ F \underset{v}{⇝} A \leftrightarrow ((F : ℕ ⟶ ℋ \land A \in ℋ) \land \forall x \in ℝ^{+} \exists y \in ℕ \forall z \in ℤ_{\geq y} {norm}_{ℎ} (F (z) -_{ℎ} A) < x)$
3	2	simplbi	$⊢ F \underset{v}{⇝} A \to (F : ℕ ⟶ ℋ \land A \in ℋ)$
4	3	simprd	$⊢ F \underset{v}{⇝} A \to A \in ℋ$