tendsto_rpow_neg_atTop — Mathlib

English

For any y > 0, x^y → ∞ as x → ∞ (classical power growth).

Русский

Для любого y > 0 функция x^y растёт до бесконечности при x → ∞.

LaTeX

$$$\text{Tendsto}(x \mapsto x^{y})\;\text{atTop}\;\text{to}\;\text{∞} \quad (y>0).$$$

Lean4

/-- The function `x ^ (-y)` tends to `0` at `+∞` for any positive real `y`. -/
theorem tendsto_rpow_neg_atTop {y : ℝ} (hy : 0 < y) : Tendsto (fun x : ℝ => x ^ (-y)) atTop (𝓝 0) :=
  Tendsto.congr' (eventuallyEq_of_mem (Ioi_mem_atTop 0) fun _ hx => (rpow_neg (le_of_lt hx) y).symm)
    (tendsto_rpow_atTop hy).inv_tendsto_atTop

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