English
The Tendsto of (x ↦ f(x) · r) to +∞ along l is equivalent to either (0 < r and Tendsto f to +∞) or (r < 0 and Tendsto f to −∞).
Русский
Пусть Tendsto (x ↦ f(x) · r) вдоль l к +∞ эквивалентно либо (0 < r и Tendsto f к +∞), либо (r < 0 и Tendsto f к −∞).
LaTeX
$$$$ \operatorname{Tendsto}(x \mapsto f(x) \cdot r) l aTop \Leftrightarrow (0 < r \land \operatorname{Tendsto} f l aTop) \lor (r < 0 \land \operatorname{Tendsto} f l aBot) $$$$
Lean4
/-- The function `fun x ↦ f x * r` tends to infinity along a nontrivial filter
if and only if `r > 0` and `f` tends to infinity or `r < 0` and `f` tends to negative infinity. -/
theorem tendsto_mul_const_atTop_iff [NeBot l] :
Tendsto (fun x => f x * r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot := by
simp only [mul_comm _ r, tendsto_const_mul_atTop_iff]
