English
For any y > 0, the function x ↦ x^{y} tends to +∞ in the extended sense as x → +∞.
Русский
Для любого y > 0 функция x ↦ x^{y} стремится к +∞ в расширенном смысле при x → +∞.
LaTeX
$$$$\displaystyle \lim_{x \to +\infty} x^{y} = +\infty\quad (y>0).$$$$
Lean4
theorem tendsto_rpow_at_top {y : ℝ} (hy : 0 < y) : Tendsto (fun x : ℝ≥0∞ => x ^ y) (𝓝 ⊤) (𝓝 ⊤) :=
by
rw [ENNReal.tendsto_nhds_top_iff_nnreal]
intro x
obtain ⟨c, _, hc⟩ := (atTop_basis_Ioi.tendsto_iff atTop_basis_Ioi).mp (NNReal.tendsto_rpow_atTop hy) x trivial
have hc' : Set.Ioi ↑c ∈ 𝓝 (⊤ : ℝ≥0∞) := Ioi_mem_nhds ENNReal.coe_lt_top
filter_upwards [hc'] with a ha
by_cases ha' : a = ⊤
· simp [ha', hy]
lift a to ℝ≥0 using ha'
simp only [Set.mem_Ioi, coe_lt_coe] at ha hc
rw [← ENNReal.coe_rpow_of_nonneg _ hy.le]
exact mod_cast hc a ha
