tendsto_pow_atTop_nhds_zero_of_norm_lt_one

English

In a normed ring, if ||x|| < 1 then x^n → 0 as n → ∞.

Русский

В нормированном кольце, если ||x|| < 1, то x^n → 0 при n → ∞.

LaTeX

$$$\\\\forall x \\\\in R, \\\\|x\\\\| < 1 \\\\Rightarrow \\\\lim_{n \\to \\infty} x^n = 0$$$

Lean4

/-- In a normed ring, the powers of an element x with `‖x‖ < 1` tend to zero. -/
theorem tendsto_pow_atTop_nhds_zero_of_norm_lt_one {R : Type*} [SeminormedRing R] {x : R} (h : ‖x‖ < 1) :
    Tendsto (fun n : ℕ ↦ x ^ n) atTop (𝓝 0) :=
  by
  apply squeeze_zero_norm' (eventually_norm_pow_le x)
  exact tendsto_pow_atTop_nhds_zero_of_lt_one (norm_nonneg _) h

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