atBot_mul_le_one — Mathlib

English

If f is pointwise ≥ 1 and g tends to +∞, then f·g tends to +∞.

Русский

Если f(x) ≥ 1 для всех x, и g(x) → ∞, то f(x)·g(x) → ∞.

LaTeX

$$$\\forall l, (\\forall x, f(x) \\ge 1) \\Rightarrow \\operatorname{Tendsto}(x\\mapsto f(x)\\,g(x))\,l\\operatorname{atTop}$$$

Lean4

@[to_additive]
theorem atBot_mul_le_one (hf : Tendsto f l atBot) (hg : ∀ x, g x ≤ 1) : Tendsto (fun x => f x * g x) l atBot :=
  hf.atBot_mul_eventuallyLE_one (.of_forall hg)

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