no goals
α : Type ?u.27357
β : Type ?u.27360
ι : Type ?u.27363
𝕜 : Type u_1
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h₁ : 0 ≤ r
h₂ : r < 1
hr : 0 = r
⊢ Tendsto (fun n => r ^ (n + 1)) atTop (𝓝 0)
simp [_root_.pow_succ, ← hr, tendsto_const_nhds]
no goals
α : Type ?u.27357
β : Type ?u.27360
ι : Type ?u.27363
𝕜 : Type u_1
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h₁ : 0 ≤ r
h₂ : r < 1
hr : 0 < r
this : Tendsto (fun n => r⁻¹ ^ n) atTop atTop
n : ℕ
⊢ ((fun r => r⁻¹) ∘ fun n => r⁻¹ ^ n) n = r ^ n
simp