English
A general form: if the derivative ratios converge along a neighborhood excluding a, then the quotient limit equals that limit along the same neighborhood.
Русский
Общая форма: если отношение производных сходится в окрестности, исключающей a, то предел отношения равен этому значению на той же окрестности.
LaTeX
$$$$ \\lim_{x\\to a, x\\neq a} \\frac{f(x)}{g(x)} = \\lim_{x\\to a, x\\neq a} \\frac{f'(x)}{g'(x)}. $$$$
Lean4
/-- **L'Hôpital's rule** for approaching a real, `HasDerivAt` version -/
theorem lhopital_zero_nhds (hff' : ∀ᶠ x in 𝓝 a, HasDerivAt f (f' x) x) (hgg' : ∀ᶠ x in 𝓝 a, HasDerivAt g (g' x) x)
(hg' : ∀ᶠ x in 𝓝 a, g' x ≠ 0) (hfa : Tendsto f (𝓝 a) (𝓝 0)) (hga : Tendsto g (𝓝 a) (𝓝 0))
(hdiv : Tendsto (fun x => f' x / g' x) (𝓝 a) l) : Tendsto (fun x => f x / g x) (𝓝[≠] a) l := by
apply @lhopital_zero_nhdsNE _ _ _ f' _ g' <;>
(first
| apply eventually_nhdsWithin_of_eventually_nhds
| apply tendsto_nhdsWithin_of_tendsto_nhds) <;>
assumption
