const_mul_atTop — Mathlib

English

If f tends to infinity along a filter l and r > 0, then x ↦ r · f(x) tends to infinity along l.

Русский

Если f идёт к бесконечности вдоль l и r > 0, то x ↦ r · f(x) идёт к бесконечности вдоль l.

LaTeX

$$$\operatorname{Tendsto}(x \mapsto r \cdot f(x))\ l\ atTop$$$

Lean4

/-- If `f` tends to infinity along a filter, then `f` multiplied by a positive
constant (on the left) also tends to infinity. For a version working in `ℕ` or `ℤ`, use
`Filter.Tendsto.const_mul_atTop'` instead. -/
theorem const_mul_atTop (hr : 0 < r) (hf : Tendsto f l atTop) : Tendsto (fun x => r * f x) l atTop :=
  (tendsto_const_mul_atTop_of_pos hr).2 hf

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