English
Let α be an ordered field and l a filter on β. If r is a negative constant, then Tendsto (x ↦ r · f(x)) along l to +∞ is equivalent to Tendsto f along l to −∞.
Русский
Пусть α — упорядоченное поле, l — фильтр на β. Пусть r < 0. Тогда Tendsto (x ↦ r · f(x)) вдоль l к +∞ эквивалентно Tendsto f вдоль l к −∞.
LaTeX
$$$$ r < 0 \Rightarrow \operatorname{Tendsto}(x \mapsto r \cdot f(x))\ l\ aTop \Leftrightarrow \operatorname{Tendsto} f\ l\ aBot $$$$
Lean4
/-- If `r` is a negative constant, `fun x ↦ r * f x` tends to infinity along a filter `l`
if and only if `f` tends to negative infinity along `l`. -/
theorem tendsto_const_mul_atTop_of_neg (hr : r < 0) : Tendsto (fun x => r * f x) l atTop ↔ Tendsto f l atBot := by
simpa only [neg_mul, tendsto_neg_atBot_iff] using tendsto_const_mul_atBot_of_pos (neg_pos.2 hr)
