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}(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 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_mul_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 only [mul_comm _ r, tendsto_const_mul_atBot_iff]
