tendsto_const_div_atTop_nhds_zero_nat

English

For any fixed nonnegative C, the sequence C/n tends to 0 as n → ∞.

Русский

Для фиксированного неотрицательного C последовательность C/n стремится к 0 при n → ∞.

LaTeX

$$$$\\displaystyle \\lim_{n\\to\\infty} \\frac{C}{n} = 0\\quad (C \\in \\mathbb{R}_{\\ge 0}).$$$$

Lean4

theorem tendsto_const_div_atTop_nhds_zero_nat (C : ℝ≥0) : Tendsto (fun n : ℕ ↦ C / n) atTop (𝓝 0) := by
  simpa using tendsto_const_nhds.mul NNReal.tendsto_inverse_atTop_nhds_zero_nat

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