α : Type u_3
β : Type u_2
γ : Type ?u.254025
δ : Type ?u.254028
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ b : α
s✝ : Finset β
inst✝ : ContinuousAdd α
ι : Type u_1
s : Finset ι
t : ι → Set β
a : ι → α
hs : Set.Pairwise (↑s) (Disjoint on t)
hf : ∀ (i : ι), i ∈ s → HasSum (Set.indicator (t i) f) (a i)
⊢ HasSum (Set.indicator (⋃ (i : ι) (_ : i ∈ s), t i) f) (∑ i in s, a i)
α : Type u_3
β : Type u_2
γ : Type ?u.254025
δ : Type ?u.254028
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ b : α
s✝ : Finset β
inst✝ : ContinuousAdd α
ι : Type u_1
s : Finset ι
t : ι → Set β
a : ι → α
hs : Set.Pairwise (↑s) (Disjoint on t)
hf : ∀ (i : ι), i ∈ s → HasSum (f ∘ Subtype.val) (a i)
⊢ HasSum (f ∘ Subtype.val) (∑ i in s, a i)
simp_rw [hasSum_subtype_iff_indicator] at *
α : Type u_3
β : Type u_2
γ : Type ?u.254025
δ : Type ?u.254028
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ b : α
s✝ : Finset β
inst✝ : ContinuousAdd α
ι : Type u_1
s : Finset ι
t : ι → Set β
a : ι → α
hs : Set.Pairwise (↑s) (Disjoint on t)
hf : ∀ (i : ι), i ∈ s → HasSum (Set.indicator (t i) f) (a i)
⊢ HasSum (fun a => ∑ i in s, Set.indicator (t i) f a) (∑ i in s, a i)
α : Type u_3
β : Type u_2
γ : Type ?u.254025
δ : Type ?u.254028
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ b : α
s✝ : Finset β
inst✝ : ContinuousAdd α
ι : Type u_1
s : Finset ι
t : ι → Set β
a : ι → α
hs : Set.Pairwise (↑s) (Disjoint on t)
hf : ∀ (i : ι), i ∈ s → HasSum (Set.indicator (t i) f) (a i)
⊢ HasSum (Set.indicator (⋃ (i : ι) (_ : i ∈ s), t i) f) (∑ i in s, a i)
rw [Set.indicator_finset_biUnion _ _ hs]
no goals
α : Type u_3
β : Type u_2
γ : Type ?u.254025
δ : Type ?u.254028
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a✝ b : α
s✝ : Finset β
inst✝ : ContinuousAdd α
ι : Type u_1
s : Finset ι
t : ι → Set β
a : ι → α
hs : Set.Pairwise (↑s) (Disjoint on t)
hf : ∀ (i : ι), i ∈ s → HasSum (Set.indicator (t i) f) (a i)
⊢ HasSum (fun a => ∑ i in s, Set.indicator (t i) f a) (∑ i in s, a i)
exact hasSum_sum hf