This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = + ℎ ⋅ ℎ norm ℎ
hhlm.2 ⊢ D = IndMet ⁡ U
Assertion hhcau ⊢ Cauchy = Cau ⁡ D ∩ ℋ ℕ

Proof

Step Hyp Ref Expression
1 hhlm.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
2 hhlm.2 ⊢ D = IndMet ⁡ U
3 1 hhnv ⊢ U ∈ NrmCVec
4 1 hhba ⊢ ℋ = BaseSet ⁡ U
5 1 3 4 2 h2hcau ⊢ Cauchy = Cau ⁡ D ∩ ℋ ℕ