English
If a function tends to negative infinity along a filter, then multiplying on the left by a negative constant reverses the direction to positive infinity.
Русский
Если функция стремится к минус бесконечности вдоль фильтра, умножение слева на отрицательную константу переводит предел к положительной бесконечности.
LaTeX
$$$r < 0 \land \operatorname{Tendsto}(f, l, \operatorname{atBot}) \Rightarrow \operatorname{Tendsto}\left(x \mapsto r \cdot f(x), l, \operatorname{atTop}\right)$$$
Lean4
/-- If a function `f` tends to negative infinity along a filter,
then `f` multiplied by a negative constant (on the left) tends to positive infinity. -/
theorem const_mul_atBot_of_neg (hr : r < 0) (hf : Tendsto f l atBot) : Tendsto (fun x => r * f x) l atTop :=
(tendsto_const_mul_atTop_of_neg hr).2 hf
