Limit_iff_Limits_from_Left_and_Right

Proved

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

analysislimits-of-functionsproofwiki

Let $f$ be a real function defined on an open interval $\openint a b$ except possibly at a point $c \in \openint a b$ . Then $\map f x \to l$ as $x \to c$ $\map f x \to l$ as $x \to c^-$ and $\map f x \to l$ as $x \to c^+$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Limit_iff_Limits_from_Left_and_Right {f : ℝ → ℝ} {a L : ℝ} : Filter.Tendsto f (nhdsWithin a (Set.Iio a)) (nhds L) ∧ Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds L) ↔ Filter.Tendsto f (nhdsWithin a {a}ᶜ) (nhds L) := by sorry

Source

https://proofwiki.org/wiki/Limit_iff_Limits_from_Left_and_Right

View graph