Limit_of_Subsequence_equals_Limit_of_Sequence
Provedlimits-of-sequencesproofwikisubsequences
If x_n converges to l and phi is a strictly increasing function on naturals, then x_{phi(n)} also converges to l.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Limit_of_Subsequence_equals_Limit_of_Sequence (x : ℕ → ℝ) (l : ℝ) (h : Filter.Tendsto x Filter.atTop (nhds l)) (phi : ℕ → ℕ) (hphi : StrictMono phi) : Filter.Tendsto (x ∘ phi) Filter.atTop (nhds l) := by sorry
Source