atTop_of_const_mul₀ — Mathlib

English

If c > 0 and c f(x) → +∞ along a filter, then f(x) → +∞ along that filter.

Русский

Если c > 0 и c f(x) стремится к +∞ по фильтру, то f(x) стремится к +∞ по этому фильтру.

LaTeX

$$$ c > 0 \wedge \lim_{x\to\infty} c\,f(x) = +\infty \Rightarrow \lim_{x\to\infty} f(x) = +\infty. $$$

Lean4

theorem atTop_of_const_mul₀ {c : α} (hc : 0 < c) (hf : Tendsto (fun x => c * f x) l atTop) : Tendsto f l atTop :=
  tendsto_atTop.2 fun b => (tendsto_atTop.1 hf (c * b)).mono fun _x hx => le_of_mul_le_mul_left hx hc

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