English
The Tendsto of (x ↦ f(x) / r) to +∞ along l equals the Tendsto of f along l to +∞ or −∞ depending on the sign of r, i.e., (0 < r and Tendsto f to +∞) or (r < 0 and Tendsto f to −∞).
Русский
Предел Tendsto (x ↦ f(x) / r) к +∞ по l равен Tendsto f к +∞ или −∞ в зависимости от знака r: (0 < r и Tendsto f к +∞) или (r < 0 и Tendsto f к −∞).
LaTeX
$$$$ \operatorname{Tendsto}\left(x \mapsto \frac{f(x)}{r}\right) 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_div_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 [div_eq_mul_inv, tendsto_mul_const_atTop_iff]
