atBot_mul_const — Mathlib

English

If a function tends to negative infinity along a filter, then multiplying by a positive constant preserves this tendency.

Русский

Если функция стремится к минус бесконечности вдоль фильтра, умножение на положительную константу сохраняет это стремление.

LaTeX

$$$0 < r \land \operatorname{Tendsto}(f, l, \operatorname{atBot}) \Rightarrow \operatorname{Tendsto}(x \mapsto f(x) \cdot r, l, \operatorname{atBot})$$$

Lean4

/-- If a function `f` tends to negative infinity along a filter, then `f` multiplied by
a positive constant (on the right) also tends to negative infinity. -/
theorem atBot_mul_const (hr : 0 < r) (hf : Tendsto f l atBot) : Tendsto (fun x => f x * r) l atBot :=
  (tendsto_mul_const_atBot_of_pos hr).2 hf

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