atTop_mul_const_of_neg — Mathlib

English

If f tends to −∞ along a nontrivial l, Tendsto (x ↦ f(x) · r) l atTop ↔ r < 0, under the irrelevance of Right-hand side.

Русский

Если f стремится к −∞ по не тривиальному l, Tendsto (x ↦ f(x) · r) к +∞ эквивалентно r < 0.

LaTeX

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

Lean4

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

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