tendsto_zero_pow_of_le_exp_neg_one

English

In a valuated ring with valuation into ℤᵐ⁰, if v(x) ≤ exp(−1) then x^n → 0 as n → ∞.

Русский

В оцениваемом кольце с отображением значения в ℤᵐ⁰, если v(x) ≤ exp(−1), то x^n стремится к нулю при n → ∞.

LaTeX

$$$\operatorname{Tendsto} \bigl(n \mapsto x^n\bigr)_{n \to \infty} \,(\mathcal{N}(0))$$$

Lean4

/-- In a `ℤᵐ⁰`-valued ring, powers of `x` tend to zero if `v x ≤ exp (-1)`. -/
theorem tendsto_zero_pow_of_le_exp_neg_one [Valued R ℤᵐ⁰] {x : R} (hx : v x ≤ exp (-1)) :
    Tendsto (fun n : ℕ ↦ x ^ n) atTop (𝓝 0) :=
  by
  refine tendsto_zero_pow_of_v_lt_one (hx.trans_lt ?_)
  rw [← exp_zero, exp_lt_exp]
  simp

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