English
For nontrivial l, Tendsto (x ↦ f(x) / r) l atTop ↔ (0 < r ∧ Tendsto f l atTop) ∨ (r < 0 ∧ Tendsto f l atBot).
Русский
Для непустого фильтра l: Tendsto (x ↦ f(x) / r) l к +∞ эквивалентно (0 < r и Tendsto f l к +∞) или (r < 0 и Tendsto f l к −∞).
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 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_div_const_atBot_iff [NeBot l] :
Tendsto (fun x ↦ f x / r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop := by
simp [div_eq_mul_inv, tendsto_mul_const_atBot_iff]
