Limit_of_Image_of_Sequence
Provedcontinuitylimits-of-sequencesproofwiki
If f is continuous at a and x_n converges to a, then f(x_n) converges to f(a).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Limit_of_Image_of_Sequence (f : ℝ → ℝ) (a l : ℝ) (hf : ContinuousAt f a) (x : ℕ → ℝ) (hx : Filter.Tendsto x Filter.atTop (nhds a)) : Filter.Tendsto (f ∘ x) Filter.atTop (nhds (f a)) := by sorry
Source