English
If x ≠ ∞ and y > 1, then eventually x^(1/n) ≤ y as n → ∞ (in atTop).
Русский
Если x ≠ ∞ и y > 1, то при достаточно большом n верно x^(1/n) ≤ y в ходе n → ∞ (в atTop).
LaTeX
$$$\\\\forall {x: \\mathbb{R}_{\\ge 0\\infty}}, x \\,\\\\neq \\\\infty \\rightarrow \\\\forall {y: \\mathbb{R}_{\\ge 0\\infty}}, (1 < y) \\\\Rightarrow \\\\forall n \\in \\mathbb{N}, x^{1/n} \\le y \\,\\text{ eventually}$$$
Lean4
theorem eventually_pow_one_div_le {x : ℝ≥0∞} (hx : x ≠ ∞) {y : ℝ≥0∞} (hy : 1 < y) :
∀ᶠ n : ℕ in atTop, x ^ (1 / n : ℝ) ≤ y := by
lift x to ℝ≥0 using hx
by_cases h : y = ∞
· exact Eventually.of_forall fun n => h.symm ▸ le_top
· lift y to ℝ≥0 using h
have := NNReal.eventually_pow_one_div_le x (mod_cast hy : 1 < y)
refine this.congr (Eventually.of_forall fun n => ?_)
rw [← coe_rpow_of_nonneg x (by positivity : 0 ≤ (1 / n : ℝ)), coe_le_coe]
