English
Let R be a ring equipped with a valuation v into a linearly ordered group with zero. If v(x) < 1, then the sequence x^n tends to 0 as n goes to infinity in the valuation topology.
Русский
Пусть R — кольцо с нормой (оценкой) v, лежащей в линейно упорядоченной группе с нулём. Если v(x) < 1, то набор x^n сходится к 0 при n → ∞ в топологии, заданной этой оценкой.
LaTeX
$$$\operatorname{Tendsto} \bigl(n \mapsto x^n\bigr)_{n \to \infty} \, (\mathcal{N}(0))$$$
Lean4
theorem tendsto_zero_pow_of_v_lt_one [MulArchimedean Γ₀] [Valued R Γ₀] {x : R} (hx : v x < 1) :
Tendsto (fun n : ℕ ↦ x ^ n) atTop (𝓝 0) :=
by
simp only [(hasBasis_nhds_zero _ _).tendsto_right_iff, mem_setOf_eq, map_pow, eventually_atTop, forall_const]
intro y
obtain ⟨n, hn⟩ := exists_pow_lt₀ hx y
refine ⟨n, fun m hm ↦ ?_⟩
refine hn.trans_le' ?_
exact pow_le_pow_right_of_le_one' hx.le hm
