no goals
α : Type u_2
β : Type u_1
γ : Type ?u.38564
δ : Type ?u.38567
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a b✝ : α
s : Finset β
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 0
this : HasSum f (∑ b' in {b}, f b')
⊢ HasSum f (f b)
simpa using this
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.38564
δ : Type ?u.38567
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f✝ g : β → α
a b✝ : α
s : Finset β
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 0
⊢ ∀ (b_1 : β), ¬b_1 ∈ {b} → f b_1 = 0
simpa [hf]