tendsto_pow_atTop_nhdsWithin_zero_of_lt_one

English

In a metric space, the uniformity has a basis given by sets where the distance is less than r^k for k ∈ ℕ, with r∈(0,1).

Русский

В метрическом пространстве унитарность имеет базис из множеств, где расстояние меньше r^k, для натуральных k и 0<r<1.

LaTeX

$$$$ (\\text{uniformity } \\alpha).HasBasis (\\lambda _ : \\mathbb{N}, \\text{True}) (\\lambda k, \\{p : \\alpha \\times \\alpha \\mid \\operatorname{dist} p.1 p.2 < r^k\\}). $$$$

Lean4

theorem tendsto_pow_atTop_nhdsWithin_zero_of_lt_one {𝕜 : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
    [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} (h₁ : 0 < r) (h₂ : r < 1) :
    Tendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝[>] 0) :=
  tendsto_inf.2
    ⟨tendsto_pow_atTop_nhds_zero_of_lt_one h₁.le h₂, tendsto_principal.2 <| Eventually.of_forall fun _ ↦ pow_pos h₁ _⟩

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