tendsto_self_div_two_mul_self_add_one

English

The sequence n/(2n+1) tends to 1/2 as n → ∞.

Русский

Последовательность n/(2n+1) стремится к 1/2 при n → ∞.

LaTeX

$$$$ \lim_{n\to\infty} \frac{n}{2n+1} = \frac{1}{2}. $$$$

Lean4

/-- The sequence `n / (2 * n + 1)` tends to `1/2` -/
theorem tendsto_self_div_two_mul_self_add_one : Tendsto (fun n : ℕ => (n : ℝ) / (2 * n + 1)) atTop (𝓝 (1 / 2)) :=
  by
  conv =>
    congr
    · skip
    · skip
    rw [one_div, ← add_zero (2 : ℝ)]
  refine
    (((tendsto_const_div_atTop_nhds_zero_nat 1).const_add (2 : ℝ)).inv₀ ((add_zero (2 : ℝ)).symm ▸ two_ne_zero)).congr'
      (eventually_atTop.mpr ⟨1, fun n hn => ?_⟩)
  rw [add_div' (1 : ℝ) 2 n (cast_ne_zero.mpr (one_le_iff_ne_zero.mp hn)), inv_div]

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