α : Type ?u.777110
β : Type ?u.777113
γ : Type ?u.777116
δ : Type ?u.777119
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f✝ : α → G
f : ℕ → G
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)
α : Type ?u.777110
β : Type ?u.777113
γ : Type ?u.777116
δ : Type ?u.777119
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f✝ : α → G
f : ℕ → G
hf : Summable f
⊢ Tendsto f atTop (𝓝 0)
rw [← Nat.cofinite_eq_atTop]
no goals
α : Type ?u.777110
β : Type ?u.777113
γ : Type ?u.777116
δ : Type ?u.777119
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : AddCommGroup G
inst✝ : TopologicalAddGroup G
f✝ : α → G
f : ℕ → G
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)
exact hf.tendsto_cofinite_zero