tendsto_rpow_atTop — Mathlib

English

For any y > 0, the function x ↦ x^{y} tends to +∞ as x → +∞.

Русский

Для любого y > 0 функция x ↦ x^{y} стремится к +∞ при x → +∞.

LaTeX

$$$$\displaystyle \lim_{x \to +\infty} x^{y} = +\infty\quad (y>0).$$$$

Lean4

nonrec theorem tendsto_rpow_atTop {y : ℝ} (hy : 0 < y) : Tendsto (fun x : ℝ≥0 => x ^ y) atTop atTop :=
  by
  rw [Filter.tendsto_atTop_atTop]
  intro b
  obtain ⟨c, hc⟩ := tendsto_atTop_atTop.mp (tendsto_rpow_atTop hy) b
  use c.toNNReal
  intro a ha
  exact mod_cast hc a (Real.toNNReal_le_iff_le_coe.mp ha)

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