tendsto_mul_add_inv_atTop_nhds_zero

English

For a real-algebraic embedding of 𝕜, the limit of the mapped inverse sequence is 0 as n → ∞.

Русский

Для отображения через алгебраическое отображение в 𝕜 предел последовательности обратных значений стремится к 0 при n → ∞.

LaTeX

$$$$\\operatorname{Tendsto}(n \\mapsto (n)^{-1})\\text{ atTop } (0)$$$$

Lean4

/-- If `a ≠ 0`, `(a * x + c)⁻¹` tends to `0` as `x` tends to `∞`. -/
theorem tendsto_mul_add_inv_atTop_nhds_zero (a c : ℝ) (ha : a ≠ 0) : Tendsto (fun x => (a * x + c)⁻¹) atTop (𝓝 0) :=
  by
  obtain ha' | ha' := lt_or_gt_of_ne ha
  · exact tendsto_inv_atBot_zero.comp (tendsto_atBot_add_const_right _ c (tendsto_id.const_mul_atTop_of_neg ha'))
  · exact tendsto_inv_atTop_zero.comp (tendsto_atTop_add_const_right _ c (tendsto_id.const_mul_atTop ha'))

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