tendsto_mul_const_atBot_iff_neg — Mathlib

English

If f tends to +∞ along a nontrivial l, then f multiplied by a negative constant tends to −∞ if and only if r < 0.

Русский

Если f к +∞ по не тривиальному l, то f·r к −∞ тогда, когда r < 0.

LaTeX

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

Lean4

/-- If `f` tends to infinity along a nontrivial filter,
`fun x ↦ f x * r` tends to negative infinity if and only if `r < 0`. -/
theorem tendsto_mul_const_atBot_iff_neg [NeBot l] (h : Tendsto f l atTop) :
    Tendsto (fun x => f x * r) l atBot ↔ r < 0 := by simp only [mul_comm _ r, tendsto_const_mul_atBot_iff_neg h]

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