Behaviour_of_Function_Near_Limit
Provedanalysislimitsproofwikireal-analysis
If f(x) -> l as x -> xi and l > 0, then f(x) > 0 in some neighborhood of xi.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Behaviour_of_Function_Near_Limit (f : ℝ → ℝ) (l ξ : ℝ) (hl : Filter.Tendsto f (nhds ξ) (nhds l)) (hlpos : 0 < l) : ∃ δ > 0, ∀ x, |x - ξ| < δ → 0 < f x := by sorry
Source