LHopitals_Rule
Disproveddifferential-calculusl-h-pital-s-rulelimits-of-functionsproofwiki
Let and be real functions which are continuous on the closed interval and differentiable on the open interval . Let where denotes the derivative of . Let Then provided that the second limit exists.
Preamble
import Mathlib.Analysis.Calculus.MeanValue import Mathlib.Topology.Order.Basic
Formal statement
theorem LHopitals_Rule (f g : ℝ → ℝ) (a L : ℝ) (hf : ContinuousOn f (Set.Ioi a)) (hg : ContinuousOn g (Set.Ioi a)) (hf0 : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds 0)) (hg0 : Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds 0)) (hg' : ∀ x, x > a → deriv g x ≠ 0) (hlim : Filter.Tendsto (fun x => deriv f x / deriv g x) (nhdsWithin a (Set.Ioi a)) (nhds L)) : Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Ioi a)) (nhds L) := by sorry
Source