English
A unified statement: L'Hôpital's rule holds in the NE (non-equal) sense, combining left and right results to cover general neighborhoods excluding a.
Русский
Обобщённое утверждение: правило Лопиталя действует в смысле NE (не равно) объединяя левые и правые случаи на окрестностях исключая точку.
LaTeX
$$$$ \\text{L'Hôpital in NE: } \\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, `deriv` version. This
does not require anything about the situation at `a` -/
theorem lhopital_zero_nhdsNE (hdf : ∀ᶠ x in 𝓝[≠] a, DifferentiableAt ℝ f x) (hg' : ∀ᶠ x in 𝓝[≠] a, deriv g x ≠ 0)
(hfa : Tendsto f (𝓝[≠] a) (𝓝 0)) (hga : Tendsto g (𝓝[≠] a) (𝓝 0))
(hdiv : Tendsto (fun x => (deriv f) x / (deriv 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 hdf.1 hg'.1 hfa.1 hga.1 hdiv.1, lhopital_zero_nhdsGT hdf.2 hg'.2 hfa.2 hga.2 hdiv.2⟩
