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 \mathrm{V}$$
Assertion	hlimveci	$$⊢F\underset{v}{⇝}A\to A\in \mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		hlim.1	$$⊢A\in \mathrm{V}$$
2	1	hlimi	$$⊢F\underset{v}{⇝}A\leftrightarrow \left(\left(F:\mathbb{N}⟶\mathscr{H}\wedge A\in \mathscr{H}\right)\wedge \forall x\in {ℝ}^{+}\exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(F\left(z\right){-}_{ℎ}A\right)<x\right)$$
3	2	simplbi	$$⊢F\underset{v}{⇝}A\to \left(F:\mathbb{N}⟶\mathscr{H}\wedge A\in \mathscr{H}\right)$$
4	3	simprd	$$⊢F\underset{v}{⇝}A\to A\in \mathscr{H}$$