English
In any group with zero, if a sequence g tends to 0 along a filter, then (f/g)g equals f eventually; i.e., division by a nonzero term cancels out asymptotically.
Русский
В любой группе с нулём, если g(x) стремится к нулю по фильтру, то (f(x)/g(x))g(x) = f(x) эффектно (набором будущих значений).
LaTeX
$$$$ (f/g)\\cdot g =ᶠ_{\\ell} f $$ при подходящем фильтре $\ell$ к бесконечности, где $G$ — группа с нулём.$$
Lean4
/-- The limit of `n / (n + x)` is 1, for any constant `x` (valid in `ℝ` or any topological division
algebra over `ℝ`, e.g., `ℂ`).
TODO: introduce a typeclass saying that `1 / n` tends to 0 at top, making it possible to get this
statement simultaneously on `ℚ`, `ℝ` and `ℂ`. -/
theorem tendsto_natCast_div_add_atTop {𝕜 : Type*} [DivisionRing 𝕜] [TopologicalSpace 𝕜] [CharZero 𝕜] [Algebra ℝ 𝕜]
[ContinuousSMul ℝ 𝕜] [IsTopologicalDivisionRing 𝕜] (x : 𝕜) : Tendsto (fun n : ℕ ↦ (n : 𝕜) / (n + x)) atTop (𝓝 1) :=
by
convert Tendsto.congr' ((eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn ↦ _)) _
· exact fun n : ℕ ↦ 1 / (1 + x / n)
· simp [Nat.cast_ne_zero.mpr hn, add_div']
· have : 𝓝 (1 : 𝕜) = 𝓝 (1 / (1 + x * (0 : 𝕜))) := by rw [mul_zero, add_zero, div_one]
rw [this]
refine tendsto_const_nhds.div (tendsto_const_nhds.add ?_) (by simp)
simp_rw [div_eq_mul_inv]
refine tendsto_const_nhds.mul ?_
have := ((continuous_algebraMap ℝ 𝕜).tendsto _).comp tendsto_inverse_atTop_nhds_zero_nat
rw [map_zero, Filter.tendsto_atTop'] at this
refine Iff.mpr tendsto_atTop' ?_
intros
simp_all only [comp_apply, map_inv₀, map_natCast]
