English
For nontrivial l, Tendsto (x ↦ f(x) / r) l atTop is equivalent to r > 0 and Tendsto f l atTop or r < 0 and Tendsto f l atBot.
Русский
Для непустого фильтра l: Tendsto (x ↦ f(x) / r) l к +∞ эквивалентно либо r > 0 и 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
/-- If `f` tends to negative infinity along a nontrivial filter `l`,
then `fun x ↦ r * f x` tends to infinity if and only if `r < 0`. -/
theorem tendsto_const_mul_atTop_iff_neg [NeBot l] (h : Tendsto f l atBot) :
Tendsto (fun x => r * f x) l atTop ↔ r < 0 := by
simp [tendsto_const_mul_atTop_iff, h, h.not_tendsto disjoint_atBot_atTop]
