English
If f tends to −∞ along a nontrivial filter l, then f multiplied by a negative constant r tends to +∞, and this occurs iff r < 0.
Русский
Если f стремится к −∞ по не тривиальному фильтру l, то f, умноженное на отрицательную константу, стремится к +∞; это происходит тогда, когда r < 0.
LaTeX
$$$$ \operatorname{Tendsto}(x \mapsto f(x) \cdot r) l aTop \Leftrightarrow (r < 0) $$$$
Lean4
/-- The function `fun x ↦ r * f x` tends to negative infinity along a nontrivial filter
if and only if `r > 0` and `f` tends to negative infinity or `r < 0` and `f` tends to infinity. -/
theorem tendsto_const_mul_atBot_iff [NeBot l] :
Tendsto (fun x => r * f x) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop := by
simp only [← tendsto_neg_atTop_iff, ← mul_neg, tendsto_const_mul_atTop_iff, neg_neg]
