Limit_of_Function_by_Convergent_Sequences
Disprovedlimits-of-functionsproofwikisequential-characterization
f(x) -> l as x -> a if and only if for every sequence x_n -> a with x_n != a, f(x_n) -> l.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Limit_of_Function_by_Convergent_Sequences (f : ℝ → ℝ) (a l : ℝ) : Filter.Tendsto f (nhds a) (nhds l) ↔ ∀ (x : ℕ → ℝ), (∀ n, x n ≠ a) → Filter.Tendsto x Filter.atTop (nhds a) → Filter.Tendsto (f ∘ x) Filter.atTop (nhds l) := by sorry
Source