English
In a framework allowing nonstandard neighborhoods away from a point a, the L'Hôpital rule asserts the limit of f/g along any NHDS neighbourhood where the derivative ratio tends to a prescribed limit l.
Русский
В рамках обобщённых окрестностей в точке a, правило Лопиталя утверждает предел f/g в NHDS-окрестностях, там где отношение производных сходится к l.
LaTeX
$$$$ \\text{If } \\lim f'(x)/g'(x) = l \\text{ in a neighborhood of } a, \\lim f/g = l. $$$$
Lean4
/-- L'Hôpital's rule for approaching a real, `HasDerivAt` version. This
does not require anything about the situation at `a` -/
theorem lhopital_zero_nhdsNE (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
simp only [← Iio_union_Ioi, nhdsWithin_union, tendsto_sup, eventually_sup] at *
exact
⟨lhopital_zero_nhdsLT hff'.1 hgg'.1 hg'.1 hfa.1 hga.1 hdiv.1,
lhopital_zero_nhdsGT hff'.2 hgg'.2 hg'.2 hfa.2 hga.2 hdiv.2⟩
