tendsto_div_nhds_zero — Mathlib

English

If f = o_l g, then the quotient f/g tends to 0 as x → l.

Русский

Если f = o_l g, то отношение f(x)/g(x) стремится к нулю при x → лямда.

LaTeX

$$$ f =o[l] g \\Rightarrow \\text{Tendsto} (\\lambda x. f(x)/g(x))\\ l\\ (\\mathcal{N} 0) $$$

Lean4

theorem tendsto_div_nhds_zero {f g : α → 𝕜} (h : f =o[l] g) : Tendsto (fun x => f x / g x) l (𝓝 0) :=
  (isLittleO_one_iff 𝕜).mp <| by
    calc
      (fun x => f x / g x) =o[l] fun x => g x / g x := by
        simpa only [div_eq_mul_inv] using h.mul_isBigO (isBigO_refl _ _)
      _ =O[l] fun _x => (1 : 𝕜) := isBigO_of_le _ fun x => by simp [div_self_le_one]

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