one_le_mul_atTop — Mathlib

English

If f is bounded above by 1, and g tends to +∞, then f·g tends to +∞.

Русский

Если f ограничено сверху единицей, а g стремится к бесконечности, то f·g стремится к бесконечности.

LaTeX

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

Lean4

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

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