tendsto_algebraMap_inverse_atTop_nhds_zero_nat

English

For any 𝕜 with a real-algebra structure, the map n ↦ (n)^{-1} under the real-algebra map tends to 0 as n → ∞.

Русский

Для любого 𝕜 с действительной алгебраической структурой отображение n ↦ n^{-1} через действительное отображение стремится к 0 при n → ∞.

LaTeX

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

Lean4

theorem tendsto_algebraMap_inverse_atTop_nhds_zero_nat (𝕜 : Type*) [Semiring 𝕜] [Algebra ℝ 𝕜] [TopologicalSpace 𝕜]
    [ContinuousSMul ℝ 𝕜] : Tendsto (algebraMap ℝ 𝕜 ∘ fun n : ℕ ↦ (n : ℝ)⁻¹) atTop (𝓝 0) :=
  NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat 𝕜

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