Description: The Cauchy 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 ) |
||
Assertion | hhcau | |- Cauchy = ( ( Cau ` D ) i^i ( ~H ^m NN ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hhlm.1 | |- U = <. <. +h , .h >. , normh >. |
|
2 | hhlm.2 | |- D = ( IndMet ` U ) |
|
3 | 1 | hhnv | |- U e. NrmCVec |
4 | 1 | hhba | |- ~H = ( BaseSet ` U ) |
5 | 1 3 4 2 | h2hcau | |- Cauchy = ( ( Cau ` D ) i^i ( ~H ^m NN ) ) |