Subsequence_of_Sequence_in_Metric_Space_with_Limit
Provedlimits-of-sequencesmetric-spacesproofwiki
Let M be a metric space. Let (x_n) be a sequence in M converging to L. Then every subsequence of (x_n) also converges to L.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Subsequence_of_Sequence_in_Metric_Space_with_Limit {X : Type _} [MetricSpace X] {x : ℕ → X} {L : X} (h : Filter.Tendsto x Filter.atTop (nhds L)) (φ : ℕ → ℕ) (hφ : StrictMono φ) : Filter.Tendsto (x ∘ φ) Filter.atTop (nhds L) := by sorrySource