tendsto_mul_const_atTop_of_pos — Mathlib

English

If r > 0 and f tends to infinity along l, then the function x ↦ f(x) · r tends to infinity along l, and conversely.

Русский

Если r > 0 и f идёт к бесконечности вдоль l, то x ↦ f(x) · r идёт к бесконечности вдоль l, и наоборот.

LaTeX

$$$\text{Tendsto}(x \mapsto f(x) \cdot r)\ l\ atTop \iff \text{Tendsto}(f)\ l\ atTop$$$

Lean4

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

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