atBot_of_mul_isBoundedUnder_ge — Mathlib

English

If g is bounded above along l and f(x) · g(x) → +∞ along l, then f(x) → +∞ along l.

Русский

Если g ограничено сверху вдоль l и f(x)·g(x) → +∞, то f(x) → +∞ вдоль l.

LaTeX

$$$\\text{IsBoundedUnder}(\\le, l, g) \\land \\operatorname{Tendsto}(\\lambda x. f(x) \\cdot g(x))\\ l\\ atTop \\Rightarrow \\operatorname{Tendsto} f\\ l\\ atTop$$$

Lean4

@[to_additive]
theorem atBot_of_mul_isBoundedUnder_ge (hg : IsBoundedUnder (· ≥ ·) l g) (h : Tendsto (fun x => f x * g x) l atBot) :
    Tendsto f l atBot :=
  h.atTop_of_mul_isBoundedUnder_le (M := Mᵒᵈ) hg

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