atTop_of_le_const_mul — Mathlib

English

If there exists C with f(x) ≤ C for all x, and f(x) · g(x) → +∞ along l, then g(x) → +∞ along l.

Русский

Если существует константа C такая, что f(x) ≤ C для всех x, и f(x)·g(x) → +∞, то g(x) → +∞ вдоль l.

LaTeX

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

Lean4

@[to_additive]
theorem atTop_of_le_const_mul (hf : ∃ C, ∀ x, f x ≤ C) (hfg : Tendsto (fun x ↦ f x * g x) l atTop) :
    Tendsto g l atTop :=
  hfg.atTop_of_isBoundedUnder_le_mul <| hf.imp fun _C hC ↦ eventually_map.mpr <| .of_forall hC

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