atTop_div_const_of_neg — Mathlib

English

If a function tends to +∞ along a filter, dividing by a negative constant yields −∞, i.e., Tendsto (x ↦ f(x) / r) l atTop implies −∞ when r < 0.

Русский

Если функция стремится к +∞ по фильтру, деление на отрицательную константу даёт −∞; то есть Tendsto (x ↦ f(x) / r) l к +∞ подразумевает −∞ при r < 0.

LaTeX

$$$$ \text{If } \operatorname{Tendsto} f l aTop, \text{ then } \operatorname{Tendsto}\left(x \mapsto \frac{f(x)}{r}\right) l aBot \text{ when } r < 0 $$$$

Lean4

/-- If a function `f` tends to infinity along a filter,
then `f` divided by a negative constant tends to negative infinity. -/
theorem atTop_div_const_of_neg (hr : r < 0) (hf : Tendsto f l atTop) : Tendsto (fun x ↦ f x / r) l atBot :=
  (tendsto_div_const_atBot_of_neg hr).2 hf

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