tendsto_mul_const_atBot_iff_pos — Mathlib

English

If f tends to −∞ along a nontrivial filter l, then Tendsto (x ↦ f(x) · r) l atTop is equivalent to 0 < r.

Русский

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

LaTeX

$$$$ [\text{NeBot } l] \Rightarrow \operatorname{Tendsto}(x \mapsto f(x) \cdot r) l aTop \Leftrightarrow 0 < r $$$$

Lean4

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

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