Theorem hhlm

Description: The limit sequences of Hilbert space. (Contributed by NM, 19-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhlm.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
	hhlm.2	$$⊢D=\mathrm{IndMet}\left(U\right)$$
	hhlm.3	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
Assertion	hhlm	$$⊢\underset{v}{⇝}={\underset{t}{⇝}\left(J\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}$$

Proof

Step	Hyp	Ref	Expression
1		hhlm.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
2		hhlm.2	$$⊢D=\mathrm{IndMet}\left(U\right)$$
3		hhlm.3	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
4	1	hhnv	$$⊢U\in \mathrm{NrmCVec}$$
5	1	hhba	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(U\right)$$
6	1 4 5 2 3	h2hlm	$$⊢\underset{v}{⇝}={\underset{t}{⇝}\left(J\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}$$