Convergent_Subsequence_of_Cauchy_Sequence

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

cauchy-sequencesproofwiki

Let $\left({A, d}\right)$ be a metric space. Let $\left\langle{x_n}\right\rangle_{n \in \N}$ be a Cauchy sequence in $A$ . Let $x \in A$ . Then $\left\langle{x_n}\right\rangle$ converges to $x$ it has a subsequence that converges to $x$ .

Preamble

import Mathlib.Topology.MetricSpace.Basic

Formal statement

theorem Convergent_Subsequence_of_Cauchy_Sequence {α : Type _} [PseudoMetricSpace α] {f : ℕ → α} (hf : CauchySeq f) {a : α} {φ : ℕ → ℕ} (hφ : StrictMono φ) (ha : Filter.Tendsto (f ∘ φ) Filter.atTop (nhds a)) : Filter.Tendsto f Filter.atTop (nhds a) := by sorry

Source

https://proofwiki.org/wiki/Convergent_Subsequence_of_Cauchy_Sequence

View graph