tendsto_mul_const_atBot_of_pos — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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