Theorems · Theorem · real analysis

deriv.lhopital_zero_nhdsNE

∀ {a : ℝ} {l : Filter ℝ} {f g : ℝ → ℝ},
  (∀ᶠ (x : ℝ) in nhdsWithin a {a}ᶜ, DifferentiableAt ℝ f x) →
    (∀ᶠ (x : ℝ) in nhdsWithin a {a}ᶜ, deriv g x ≠ 0) →
      Filter.Tendsto f (nhdsWithin a {a}ᶜ) (nhds 0) →
        Filter.Tendsto g (nhdsWithin a {a}ᶜ) (nhds 0) →
          Filter.Tendsto (fun x => deriv f x / deriv g x) (nhdsWithin a {a}ᶜ) l →
            Filter.Tendsto (fun x => f x / g x) (nhdsWithin a {a}ᶜ) l

L'Hôpital's rule for approaching a real, deriv version. This does not require anything about the situation at a

Defined in

Mathlib.Analysis.Calculus.LHopital

Cited by

1 results in Mathlib

Foundations

Depth 194 from the axioms · uses propext, Classical.choice, Quot.sound