α : Type ?u.130810
β : Type ?u.130813
ι : Type ?u.130816
R : Type u_1
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
⊢ Tendsto (fun n => ‖x‖ ^ n) atTop (𝓝 0)
α : Type ?u.130810
β : Type ?u.130813
ι : Type ?u.130816
R : Type u_1
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
⊢ Tendsto (fun n => x ^ n) atTop (𝓝 0)
apply squeeze_zero_norm' (eventually_norm_pow_le x)
no goals
α : Type ?u.130810
β : Type ?u.130813
ι : Type ?u.130816
R : Type u_1
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
⊢ Tendsto (fun n => ‖x‖ ^ n) atTop (𝓝 0)
exact tendsto_pow_atTop_nhds_0_of_lt_1 (norm_nonneg _) h