Metamath Proof Explorer


Theorem hhcau

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

Proof

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