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 ) ) |
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 ) ) |