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