English
If a function tends to −∞ along a filter l, then multiplying by a positive constant preserves the −∞ trend: Tendsto (x ↦ r · f(x)) l atBot for r > 0 when Tendsto f l atBot.
Русский
Если f → −∞ по фильтру, то умножение на положительную константу сохраняет направление снизу: при r > 0 Tendsto (x ↦ r · f(x)) l atBot.
LaTeX
$$$$ r > 0 \Rightarrow \operatorname{Tendsto}(x \mapsto r \cdot f(x)) l aBot \text{ при } \operatorname{Tendsto} f l aBot $$$$
Lean4
/-- If a function `f` tends to negative infinity along a filter, then `f` multiplied by
a positive constant (on the left) also tends to negative infinity. -/
theorem const_mul_atBot (hr : 0 < r) (hf : Tendsto f l atBot) : Tendsto (fun x => r * f x) l atBot :=
(tendsto_const_mul_atBot_of_pos hr).2 hf
