tendsto_mul_const_atTop_iff_neg — Mathlib

English

If f tends to −∞ along a nontrivial l, then (x ↦ f(x) · r) tends to +∞ iff r < 0.

Русский

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

LaTeX

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

Lean4

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

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