α : Type u_2
β : Type u_1
γ : Type ?u.424010
δ : Type ?u.424013
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
s : Set β
hf : HasSum (f ∘ Subtype.val) a₁
h : HasSum f (a₁ + a₂)
⊢ HasSum (f ∘ Subtype.val) a₂
α : Type u_2
β : Type u_1
γ : Type ?u.424010
δ : Type ?u.424013
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
s : Set β
hf : HasSum (f ∘ Subtype.val) a₁
⊢ HasSum (f ∘ Subtype.val) a₂ ↔ HasSum f (a₁ + a₂)
refine' ⟨fun h => hf.add_compl h, fun h => _⟩
α : Type u_2
β : Type u_1
γ : Type ?u.424010
δ : Type ?u.424013
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
s : Set β
hf : HasSum (Set.indicator s f) a₁
h : HasSum f (a₁ + a₂)
⊢ HasSum (Set.indicator (sᶜ) f) a₂
α : Type u_2
β : Type u_1
γ : Type ?u.424010
δ : Type ?u.424013
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
s : Set β
hf : HasSum (f ∘ Subtype.val) a₁
h : HasSum f (a₁ + a₂)
⊢ HasSum (f ∘ Subtype.val) a₂
rw [hasSum_subtype_iff_indicator] at hf⊢
α : Type u_2
β : Type u_1
γ : Type ?u.424010
δ : Type ?u.424013
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
s : Set β
hf : HasSum (Set.indicator s f) a₁
h : HasSum f (a₁ + a₂)
⊢ HasSum (f - Set.indicator s f) a₂
α : Type u_2
β : Type u_1
γ : Type ?u.424010
δ : Type ?u.424013
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
s : Set β
hf : HasSum (Set.indicator s f) a₁
h : HasSum f (a₁ + a₂)
⊢ HasSum (Set.indicator (sᶜ) f) a₂
rw [Set.indicator_compl]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.424010
δ : Type ?u.424013
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
s : Set β
hf : HasSum (Set.indicator s f) a₁
h : HasSum f (a₁ + a₂)
⊢ HasSum (f - Set.indicator s f) a₂
simpa only [add_sub_cancel'] using h.sub hf