Database
COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)
Cauchy sequences and completeness axiom
Cauchy sequences and limits
seq1hcau
Metamath Proof Explorer
Description: A sequence on a Hilbert space is a Cauchy sequence if it converges.
(Contributed by NM , 16-Aug-1999) (Revised by Mario Carneiro , 14-May-2014) (New usage is discouraged.)
Ref
Expression
Assertion
seq1hcau
⊢ ( 𝐹 : ℕ ⟶ ℋ → ( 𝐹 ∈ Cauchy ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑦 ) −ℎ ( 𝐹 ‘ 𝑧 ) ) ) < 𝑥 ) )
Proof
Step
Hyp
Ref
Expression
1
hcau
⊢ ( 𝐹 ∈ Cauchy ↔ ( 𝐹 : ℕ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑦 ) −ℎ ( 𝐹 ‘ 𝑧 ) ) ) < 𝑥 ) )
2
1
baib
⊢ ( 𝐹 : ℕ ⟶ ℋ → ( 𝐹 ∈ Cauchy ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑦 ) −ℎ ( 𝐹 ‘ 𝑧 ) ) ) < 𝑥 ) )