α : Type u_1
β : Type ?u.238111
γ : Type ?u.238114
δ : Type ?u.238117
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a✝ b : α
s : Finset β
inst✝ : T2Space α
f : ℕ → α
a : α
hf : Summable f
h : Tendsto (fun n => ∑ i in range n, f i) atTop (𝓝 a)
⊢ HasSum f a
α : Type u_1
β : Type ?u.238111
γ : Type ?u.238114
δ : Type ?u.238117
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a✝ b : α
s : Finset β
inst✝ : T2Space α
f : ℕ → α
a : α
hf : Summable f
⊢ HasSum f a ↔ Tendsto (fun n => ∑ i in range n, f i) atTop (𝓝 a)
refine' ⟨fun h => h.tendsto_sum_nat, fun h => _⟩
α : Type u_1
β : Type ?u.238111
γ : Type ?u.238114
δ : Type ?u.238117
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a✝ b : α
s : Finset β
inst✝ : T2Space α
f : ℕ → α
a : α
hf : Summable f
h : Tendsto (fun n => ∑ i in range n, f i) atTop (𝓝 a)
⊢ HasSum f (∑' (b : ℕ), f b)
α : Type u_1
β : Type ?u.238111
γ : Type ?u.238114
δ : Type ?u.238117
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a✝ b : α
s : Finset β
inst✝ : T2Space α
f : ℕ → α
a : α
hf : Summable f
h : Tendsto (fun n => ∑ i in range n, f i) atTop (𝓝 a)
⊢ HasSum f a
rw [tendsto_nhds_unique h hf.hasSum.tendsto_sum_nat]
no goals
α : Type u_1
β : Type ?u.238111
γ : Type ?u.238114
δ : Type ?u.238117
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a✝ b : α
s : Finset β
inst✝ : T2Space α
f : ℕ → α
a : α
hf : Summable f
h : Tendsto (fun n => ∑ i in range n, f i) atTop (𝓝 a)
⊢ HasSum f (∑' (b : ℕ), f b)
exact hf.hasSum