one_eventuallyLE_mul_atTop — Mathlib

English

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

Русский

Если f в итоге не меньше 1, а g стремится к бесконечности, то произведение f·g идёт к бесконечности.

LaTeX

$$$\\forall l, {f,g}: α \\to M,\\;\\text{l.EventuallyLE } 1\\ f \\rightarrow \\operatorname{Tendsto} g\,l\\operatorname{atTop} \\Rightarrow \\operatorname{Tendsto}(x\\mapsto f(x)\\,g(x))\,l\,\\operatorname{atTop}$$$

Lean4

@[to_additive]
theorem one_eventuallyLE_mul_atTop (hf : 1 ≤ᶠ[l] f) (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atTop :=
  tendsto_atTop_mono' l (hf.mono fun _ ↦ le_mul_of_one_le_left') hg

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