div_mul_cancel_atTop — Mathlib

English

For any α, G with a Tendsto g to something nonzero, eventually f/g·g = f.

Русский

Пусть g(x) расходится; тогда существует множество x, для которых f(x)/g(x)·g(x) = f(x).

LaTeX

$$$$ (f/g)\\cdot g =ᶠ_{l} f $$$$

Lean4

/-- If `g` tends to `∞`, then eventually for all `x` we have `(f x / g x) * g x = f x`. -/
theorem div_mul_cancel_atTop {α K : Type*} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {f g : α → K}
    {l : Filter α} (hg : Tendsto g l atTop) : (fun x ↦ f x / g x * g x) =ᶠ[l] fun x ↦ f x :=
  div_mul_cancel <| hg.mono_right <| le_principal_iff.mpr <| mem_of_superset (Ioi_mem_atTop 0) <| by simp

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