tendsto_const_div_atTop_nhds_zero_nat

English

If a finite, nonzero extended-real number C (i.e., C ≠ ⊥ and C ≠ ⊤) is fixed, then C/n → 0 as n → ∞.

Русский

Если фиксировано конечное ненулевое число C в области EReal (C ≠ ⊥ и C ≠ ⊤), то C/n → 0 при n → ∞.

LaTeX

$$$$\\text{If } C \\in \\mathbb{E}\\mathbb{R} \\setminus\\{\\bot,\\top\\},\\quad \\lim_{n\\to\\infty} \\frac{C}{n} = 0.$$$$

Lean4

theorem tendsto_const_div_atTop_nhds_zero_nat {C : EReal} (h : C ≠ ⊥) (h' : C ≠ ⊤) :
    Tendsto (fun n : ℕ ↦ C / n) atTop (𝓝 0) :=
  by
  have : (fun n : ℕ ↦ C / n) = fun n : ℕ ↦ ((C.toReal / n : ℝ) : EReal) :=
    by
    ext n
    nth_rw 1 [← coe_toReal h' h, ← coe_coe_eq_natCast n, ← coe_div C.toReal n]
  rw [this, ← coe_zero, tendsto_coe]
  exact _root_.tendsto_const_div_atTop_nhds_zero_nat C.toReal

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