tendsto_add_mul_div_add_mul_atTop_nhds

English

For a, b, c in 𝕜 with d ≠ 0, the limit of (a + c k)/(b + d k) as k → ∞ equals c/d.

Русский

Для элементов a, b, c в 𝕜 и d ≠ 0 предельное поведение (a + c k)/(b + d k) при k → ∞ равно c/d.

LaTeX

$$$\lim_{k \to \infty} \frac{a + c k}{b + d k} = \frac{c}{d} \quad (d \neq 0)$$$

Lean4

theorem tendsto_add_mul_div_add_mul_atTop_nhds (a b c : 𝕜) {d : 𝕜} (hd : d ≠ 0) :
    Tendsto (fun k : ℕ ↦ (a + c * k) / (b + d * k)) atTop (𝓝 (c / d)) :=
  by
  apply Filter.Tendsto.congr'
  case f₁ => exact fun k ↦ (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)
  · refine (eventually_ne_atTop 0).mp (Eventually.of_forall ?_)
    intro h hx
    field_simp (discharger := norm_cast)
  · apply Filter.Tendsto.div _ _ hd
    all_goals
      apply zero_add (_ : 𝕜) ▸ Filter.Tendsto.add_const _ _
      apply mul_zero (_ : 𝕜) ▸ Filter.Tendsto.const_mul _ _
      exact tendsto_inverse_atTop_nhds_zero_nat 𝕜

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