Metamath Proof Explorer


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 = <. <. +h , .h >. , normh >.
hhlm.2
|- D = ( IndMet ` U )
hhlm.3
|- J = ( MetOpen ` D )
Assertion hhlm
|- ~~>v = ( ( ~~>t ` J ) |` ( ~H ^m NN ) )

Proof

Step Hyp Ref Expression
1 hhlm.1
 |-  U = <. <. +h , .h >. , normh >.
2 hhlm.2
 |-  D = ( IndMet ` U )
3 hhlm.3
 |-  J = ( MetOpen ` D )
4 1 hhnv
 |-  U e. NrmCVec
5 1 hhba
 |-  ~H = ( BaseSet ` U )
6 1 4 5 2 3 h2hlm
 |-  ~~>v = ( ( ~~>t ` J ) |` ( ~H ^m NN ) )