Theorem hhcau

Description: The Cauchy sequences of Hilbert space. (Contributed by NM, 19-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhlm.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
	hhlm.2	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
Assertion	hhcau	⊢ Cauchy = ( ( Cau ‘ 𝐷 ) ∩ ( ℋ ↑m ℕ ) )

Proof

Step	Hyp	Ref	Expression
1		hhlm.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2		hhlm.2	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
3	1	hhnv	⊢ 𝑈 ∈ NrmCVec
4	1	hhba	⊢ ℋ = ( BaseSet ‘ 𝑈 )
5	1 3 4 2	h2hcau	⊢ Cauchy = ( ( Cau ‘ 𝐷 ) ∩ ( ℋ ↑m ℕ ) )