tendsto_algebraMap_inverse_atTop_nhds_zero_nat

English

For any topological semiring 𝕜 with a compatible ℝ≥0-algebra structure, the image of n^{-1} under the algebra map tends to 0 as n → ∞.

Русский

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

LaTeX

$$$$\\operatorname{Tendsto}\\bigl(\\mathsf{algebraMap}\\, \\mathbb{R}_{\\ge 0} 𝕜 \\circ (n \\mapsto (n)^{-1})\\bigr)\\text{ atTop } (0)$$$$

Lean4

theorem tendsto_algebraMap_inverse_atTop_nhds_zero_nat (𝕜 : Type*) [Semiring 𝕜] [Algebra ℝ≥0 𝕜] [TopologicalSpace 𝕜]
    [ContinuousSMul ℝ≥0 𝕜] : Tendsto (algebraMap ℝ≥0 𝕜 ∘ fun n : ℕ ↦ (n : ℝ≥0)⁻¹) atTop (𝓝 0) :=
  by
  convert (continuous_algebraMap ℝ≥0 𝕜).continuousAt.tendsto.comp tendsto_inverse_atTop_nhds_zero_nat
  rw [map_zero]

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