atBot_mul_eventuallyLE_one — Mathlib

English

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

Русский

Если f стремится к +∞, а g в конце концов не меньше 1, то f·g стремится к +∞.

LaTeX

$$$\\operatorname{Tendsto}(f)\\;l\\;\\operatorname{atTop} \\Rightarrow \\operatorname{Tendsto}(x\\mapsto f(x)\\,g(x))\,l\\operatorname{atTop}$ under the hypothesis $g$ eventually ≥ 1.$$

Lean4

@[to_additive]
theorem atBot_mul_eventuallyLE_one (hf : Tendsto f l atBot) (hg : g ≤ᶠ[l] 1) : Tendsto (fun x => f x * g x) l atBot :=
  hf.atTop_mul_one_eventuallyLE (M := Mᵒᵈ) hg

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