Theorem hlimseqi

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

	Ref	Expression
Hypothesis	hlim.1	$$⊢A\in \mathrm{V}$$
Assertion	hlimseqi	$$⊢F\underset{v}{⇝}A\to F:\mathbb{N}⟶\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	simpld	$$⊢F\underset{v}{⇝}A\to F:\mathbb{N}⟶\mathscr{H}$$