atTop_of_mul_const₀ — Mathlib

English

If c > 0 and f(x) c → +∞, then f(x) → +∞ as x → ∞.

Русский

Если c > 0 и f(x) c → +∞, то f(x) → +∞ при x → ∞.

LaTeX

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

Lean4

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

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