tendsto_mod_div_atTop_nhds_zero_nat

English

For any topological division algebra over ℝ, the expression (n:𝕜)/(n+x) tends to 1 as n → ∞, for any fixed x.

Русский

Для любой делимой надℝ алгебры в топологическом смысле выражение (n:𝕜)/(n+x) стремится к 1 при n→∞, для фиксированного x.

LaTeX

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

Lean4

/-- For any positive `m : ℕ`, `((n % m : ℕ) : ℝ) / (n : ℝ)` tends to `0` as `n` tends to `∞`. -/
theorem tendsto_mod_div_atTop_nhds_zero_nat {m : ℕ} (hm : 0 < m) :
    Tendsto (fun n : ℕ => ((n % m : ℕ) : ℝ) / (n : ℝ)) atTop (𝓝 0) :=
  by
  have h0 : ∀ᶠ n : ℕ in atTop, 0 ≤ (fun n : ℕ => ((n % m : ℕ) : ℝ)) n := by aesop
  exact
    tendsto_bdd_div_atTop_nhds_zero h0 (.of_forall (fun n ↦ cast_le.mpr (mod_lt n hm).le)) tendsto_natCast_atTop_atTop

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