tendsto_bdd_div_atTop_nhds_zero — Mathlib

English

If f is eventually bounded between b and B and g → +∞, then f/g → 0.

Русский

Если f ограничено между b и B и g → +∞, то f/g → 0.

LaTeX

$$Let f, g : α → 𝕜 with b ≤ f(x) ≤ B eventually and g(x) → +∞, then f(x)/g(x) → 0.$$

Lean4

/-- If `g` tends to `atTop` and there exist constants `b B : 𝕜` such that eventually
  `b ≤ f x| ≤ B`, then the quotient `f / g` tends to zero. -/
theorem tendsto_bdd_div_atTop_nhds_zero {f g : α → 𝕜} {b B : 𝕜} (hb : ∀ᶠ x in l, b ≤ f x) (hB : ∀ᶠ x in l, f x ≤ B)
    (hg : Tendsto g l atTop) : Tendsto (fun x => f x / g x) l (𝓝 0) :=
  by
  simp only [div_eq_mul_inv]
  exact bdd_le_mul_tendsto_zero hb hB hg.inv_tendsto_atTop

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