atBot_of_isBoundedUnder_ge_mul — Mathlib

English

Dual statement: if g is bounded below 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}(\\ge, 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_isBoundedUnder_ge_mul (hf : IsBoundedUnder (· ≥ ·) l f) (h : Tendsto (fun x => f x * g x) l atBot) :
    Tendsto g l atBot :=
  h.atTop_of_isBoundedUnder_le_mul (M := Mᵒᵈ) hf

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