English
Let α be an ordered field and l a nontrivial filter. If r < 0 and Tendsto f along l to the bottom, then Tendsto (x ↦ f(x) · r) to the top holds iff Tendsto f along l to the top.
Русский
Пусть α — упорядоченное поле, l — непустой фильтр. Если r < 0 и Tendsto f вдоль l к нижней границе, то Tendsto (x ↦ f(x) · r) к верхней границе эквивалентно Tendsto f вдоль l к верхней границе.
LaTeX
$$$$ r < 0 \land \operatorname{Tendsto} f\ l\ aBot \Rightarrow \operatorname{Tendsto}(x \mapsto f(x) \cdot r)\ l\ aTop $$$$
Lean4
/-- If `r` is a negative constant, `fun x ↦ f x * r` tends to negative infinity along a filter `l`
if and only if `f` tends to infinity along `l`. -/
theorem tendsto_mul_const_atBot_of_neg (hr : r < 0) : Tendsto (fun x => f x * r) l atBot ↔ Tendsto f l atTop := by
simpa only [mul_comm] using tendsto_const_mul_atBot_of_neg hr
