atTop_of_mul_le_const — Mathlib

English

If there exists a constant 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_mul_le_const (hg : ∃ C, ∀ x, g x ≤ C) (hfg : Tendsto (fun x ↦ f x * g x) l atTop) :
    Tendsto f l atTop :=
  hfg.atTop_of_mul_isBoundedUnder_le <| hg.imp fun _C hC ↦ eventually_map.mpr <| .of_forall hC

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