case h.e'_2.h.e'_14.h
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1436330
G : Type ?u.1436333
𝕜 : Type ?u.1436336
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
hT : DominatedFinMeasAdditive μ T C
ι : Type u_4
s : Finset ι
f : ι → α → E
hf : ∀ (i : ι), i ∈ s → Integrable (f i)
a : α
⊢ ∑ i in s, f i a = Finset.sum s (fun i => f i) a
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1436330
G : Type ?u.1436333
𝕜 : Type ?u.1436336
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
hT : DominatedFinMeasAdditive μ T C
ι : Type u_4
s : Finset ι
f : ι → α → E
hf : ∀ (i : ι), i ∈ s → Integrable (f i)
⊢ (setToFun μ T hT fun a => ∑ i in s, f i a) = ∑ i in s, setToFun μ T hT (f i)
convert setToFun_finset_sum' hT s hf with a
no goals
case h.e'_2.h.e'_14.h
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1436330
G : Type ?u.1436333
𝕜 : Type ?u.1436336
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
hT : DominatedFinMeasAdditive μ T C
ι : Type u_4
s : Finset ι
f : ι → α → E
hf : ∀ (i : ι), i ∈ s → Integrable (f i)
a : α
⊢ ∑ i in s, f i a = Finset.sum s (fun i => f i) a
simp