tendsto_const_mul_atBot_of_pos — Mathlib

English

If r > 0, then Tendsto (x ↦ r · f(x)) l atBot is equivalent to Tendsto f l atBot.

Русский

Если r > 0, то Tendsto (x ↦ r · f(x)) l atBot эквивалентно Tendsto f l atBot.

LaTeX

$$$\operatorname{Tendsto}(x \mapsto r \cdot f(x))\ l\ atBot \iff \operatorname{Tendsto}(f)\ l\ atBot$$$

Lean4

/-- If `r` is a positive constant, `fun x ↦ r * f x` tends to negative infinity along a filter
if and only if `f` tends to negative infinity along the same filter. -/
theorem tendsto_const_mul_atBot_of_pos (hr : 0 < r) : Tendsto (fun x => r * f x) l atBot ↔ Tendsto f l atBot := by
  simpa only [← mul_neg, ← tendsto_neg_atTop_iff] using tendsto_const_mul_atTop_of_pos hr

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