const_mul_atTop_of_neg — Mathlib

English

For a nontrivial l, Tendsto (x ↦ r · f(x)) l atTop is equivalent to Tendsto f l atTop or Tendsto f l atBot depending on r’s sign.

Русский

Для непустого l: Tendsto (x ↦ r · f(x)) к +∞ эквивалентно Tendsto f к +∞ или к −∞ в зависимости от знака r.

LaTeX

$$$$ \operatorname{Tendsto}(x \mapsto r \cdot f(x)) l aTop \Leftrightarrow (0 < r \land \operatorname{Tendsto} f l aTop) \lor (r < 0 \land \operatorname{Tendsto} f l aBot) $$$$

Lean4

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

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