case intro.intro
α : Type ?u.42152
β : Type ?u.42155
ι : Type ?u.42158
r : ℝ≥0
hr' : ↑r < 1
hr : ↑r < 1
⊢ Tendsto (fun n => ↑r ^ n) atTop (𝓝 0)
α : Type ?u.42152
β : Type ?u.42155
ι : Type ?u.42158
r : ℝ≥0∞
hr : r < 1
⊢ Tendsto (fun n => r ^ n) atTop (𝓝 0)
rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩
case intro.intro
α : Type ?u.42152
β : Type ?u.42155
ι : Type ?u.42158
r : ℝ≥0
hr' : ↑r < 1
hr : ↑r < 1
⊢ Tendsto (fun n => ↑r ^ n) atTop (𝓝 ↑0)
case intro.intro
α : Type ?u.42152
β : Type ?u.42155
ι : Type ?u.42158
r : ℝ≥0
hr' : ↑r < 1
hr : ↑r < 1
⊢ Tendsto (fun n => ↑r ^ n) atTop (𝓝 0)
rw [← ENNReal.coe_zero]
case intro.intro
α : Type ?u.42152
β : Type ?u.42155
ι : Type ?u.42158
r : ℝ≥0
hr' hr : r < 1
⊢ Tendsto (fun a => r ^ a) atTop (𝓝 0)
case intro.intro
α : Type ?u.42152
β : Type ?u.42155
ι : Type ?u.42158
r : ℝ≥0
hr' : ↑r < 1
hr : ↑r < 1
⊢ Tendsto (fun n => ↑r ^ n) atTop (𝓝 ↑0)
norm_cast at *
no goals
case intro.intro
α : Type ?u.42152
β : Type ?u.42155
ι : Type ?u.42158
r : ℝ≥0
hr' hr : r < 1
⊢ Tendsto (fun a => r ^ a) atTop (𝓝 0)
apply NNReal.tendsto_pow_atTop_nhds_0_of_lt_1 hr