tendsto_pow_atTop_nhds_zero_of_lt_one

English

For any field 𝕜, Tendsto r^n to 0 is equivalent to |r|<1.

Русский

Для поля 𝕜 переход r^n к 0 эквивалентен |r|<1.

LaTeX

$$$$\\text{Tendsto}(r^n)\\to 0\\;\\iff\\; |r|<1.$$$$

Lean4

theorem tendsto_pow_atTop_nhds_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) :=
  h₁.eq_or_lt.elim (fun hr ↦ (tendsto_add_atTop_iff_nat 1).mp <| by simp [_root_.pow_succ, ← hr])
    (fun hr ↦
      have := (one_lt_inv₀ hr).2 h₂ |> tendsto_pow_atTop_atTop_of_one_lt
      (tendsto_inv_atTop_zero.comp this).congr fun n ↦ by simp)

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