α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.24186
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g✝ : β → α
a b : α
s : Finset β
g : β → γ
hg : Injective g
⊢ ∀ (x : γ), ¬x ∈ Set.range g → extend g f 0 x = 0
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.24186
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g✝ : β → α
a b : α
s : Finset β
g : β → γ
hg : Injective g
⊢ HasSum (extend g f 0) a ↔ HasSum f a
rw [← hg.hasSum_iff, extend_comp hg]
no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.24186
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g✝ : β → α
a b : α
s : Finset β
g : β → γ
hg : Injective g
⊢ ∀ (x : γ), ¬x ∈ Set.range g → extend g f 0 x = 0
exact extend_apply' _ _