Theorems · Theorem · real analysis

HasDerivAt.lhopital_zero_nhdsGT

∀ {a : ℝ} {l : Filter ℝ} {f f' g g' : ℝ → ℝ},
  (∀ᶠ (x : ℝ) in nhdsWithin a (Set.Ioi a), HasDerivAt f (f' x) x) →
    (∀ᶠ (x : ℝ) in nhdsWithin a (Set.Ioi a), HasDerivAt g (g' x) x) →
      (∀ᶠ (x : ℝ) in nhdsWithin a (Set.Ioi a), g' x ≠ 0) →
        Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds 0) →
          Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds 0) →
            Filter.Tendsto (fun x => f' x / g' x) (nhdsWithin a (Set.Ioi a)) l →
              Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Ioi a)) l

L'Hôpital's rule for approaching a real from the right, HasDerivAt version

Defined in

Mathlib.Analysis.Calculus.LHopital

Cited by

2 results in Mathlib

Foundations

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