tendsto_const_div_pow — Mathlib

English

If k ≠ 0, then r/n^k → 0 for any real r.

Русский

Если k ≠ 0, то r/n^k → 0 для любого вещественного r.

LaTeX

$$$\\\\forall r \\\\in \\\\mathbb{R}, \\\\lim_{n \\to \\infty} \\\\frac{r}{n^k} = 0$$$

Lean4

/-- For `k ≠ 0` and a constant `r` the function `r / n ^ k` tends to zero. -/
theorem tendsto_const_div_pow (r : ℝ) (k : ℕ) (hk : k ≠ 0) : Tendsto (fun n : ℕ => r / n ^ k) atTop (𝓝 0) := by
  simpa using Filter.Tendsto.const_div_atTop (tendsto_natCast_atTop_atTop (R := ℝ).comp (tendsto_pow_atTop hk)) r

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