lhopital_zero_right_on_Ico — Mathlib

English

Let a<b. If f,g are differentiable on Ioo(a,b) with g' nonzero there, and f,g continuous on Ico(a,b) with f(a)=0 and g(a)=0, and the quotient of derivatives tends to l as x→a from the right, then f/g tends to l at a from the right over Ioi-type neighborhoods.

Русский

Пусть a<b. Если f,g дифференцируемы на Ioo(a,b) и g' ≠ 0 там, f,g непрерывны на Ico(a,b) и f(a)=g(a)=0, а отношение производных → l при x→a справа, то f/g имеет предел l при x→a справа.

LaTeX

$$$$ a

Lean4

theorem lhopital_zero_right_on_Ico (hab : a < b) (hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x)
    (hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x) (hcf : ContinuousOn f (Ico a b)) (hcg : ContinuousOn g (Ico a b))
    (hg' : ∀ x ∈ Ioo a b, g' x ≠ 0) (hfa : f a = 0) (hga : g a = 0) (hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l) :
    Tendsto (fun x => f x / g x) (𝓝[>] a) l :=
  by
  refine lhopital_zero_right_on_Ioo hab hff' hgg' hg' ?_ ?_ hdiv
  · rw [← hfa, ← nhdsWithin_Ioo_eq_nhdsGT hab]
    exact ((hcf a <| left_mem_Ico.mpr hab).mono Ioo_subset_Ico_self).tendsto
  · rw [← hga, ← nhdsWithin_Ioo_eq_nhdsGT hab]
    exact ((hcg a <| left_mem_Ico.mpr hab).mono Ioo_subset_Ico_self).tendsto

Похожие утверждения