α : Type u_1
f : α → ℝ≥0
hf : Summable fun a => ↑(f a)
⊢ Tendsto (fun a => ↑(f a)) cofinite (𝓝 ↑0)
α : Type u_1
f : α → ℝ≥0
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)
simp only [← summable_coe, ← tendsto_coe] at hf ⊢
no goals
α : Type u_1
f : α → ℝ≥0
hf : Summable fun a => ↑(f a)
⊢ Tendsto (fun a => ↑(f a)) cofinite (𝓝 ↑0)
exact hf.tendsto_cofinite_zero