tendsto_const_mul_atTop_of_pos — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- If `r` is a positive constant, `fun x ↦ r * f x` tends to infinity along a filter
if and only if `f` tends to infinity along the same filter. -/
theorem tendsto_const_mul_atTop_of_pos (hr : 0 < r) : Tendsto (fun x => r * f x) l atTop ↔ Tendsto f l atTop :=
  ⟨fun h => h.atTop_of_const_mul₀ hr, fun h =>
    Tendsto.atTop_of_const_mul₀ (inv_pos.2 hr) <| by simpa only [inv_mul_cancel_left₀ hr.ne']⟩

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