atBot_mul_const_of_neg — Mathlib

English

If a function tends to negative infinity along a filter, then multiplying by a negative constant (on the right) tends to positive infinity.

Русский

Если функция стремится к минус бесконечности вдоль фильтра, умножение на отрицательную константу с конца приводит к плюсом бесконечности.

LaTeX

$$$0 \le r < 0 \land \operatorname{Tendsto}(f, l, \operatorname{atBot}) \Rightarrow \operatorname{Tendsto}\left(x \mapsto f(x) \cdot r, l, \operatorname{atTop}\right)$$$

Lean4

/-- If a function tends to negative infinity along a filter,
then `f` multiplied by a negative constant (on the right) tends to positive infinity. -/
theorem atBot_mul_const_of_neg (hr : r < 0) (hf : Tendsto f l atBot) : Tendsto (fun x => f x * r) l atTop :=
  (tendsto_mul_const_atTop_of_neg hr).2 hf

Похожие утверждения