α : Type ?u.1359
β : Type ?u.1362
ι : Type ?u.1365
⊢ Tendsto (fun a => ↑(↑a)⁻¹) atTop (𝓝 ↑0)
α : Type ?u.1359
β : Type ?u.1362
ι : Type ?u.1365
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (𝓝 0)
rw [← NNReal.tendsto_coe]
no goals
α : Type ?u.1359
β : Type ?u.1362
ι : Type ?u.1365
⊢ Tendsto (fun a => ↑(↑a)⁻¹) atTop (𝓝 ↑0)
exact _root_.tendsto_inverse_atTop_nhds_0_nat