English
The value of Tendsto (x ↦ r · f(x)) along l to +∞ is equivalent to either (i) 0 < r and Tendsto f along l to +∞, or (ii) r < 0 and Tendsto f along l to −∞.
Русский
Значение Tendsto (x ↦ r · f(x)) вдоль l к +∞ эквивалентно либо (i) 0 < r и Tendsto f вдоль l к +∞, либо (ii) r < 0 и Tendsto f вдоль l к −∞.
LaTeX
$$$$ \operatorname{Tendsto}(x \mapsto r f(x)) 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 ↦ r * f x` 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_const_mul_atTop_iff [NeBot l] :
Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot :=
by
rcases lt_trichotomy r 0 with (hr | rfl | hr)
· simp [hr, hr.not_gt, tendsto_const_mul_atTop_of_neg]
· simp [not_tendsto_const_atTop]
· simp [hr, hr.not_gt, tendsto_const_mul_atTop_of_pos]
