α : Type u_2
β : Type ?u.921513
γ : Type ?u.921516
δ : Type ?u.921519
m✝ : MeasurableSpace α
μ✝ ν : Measure α
ι : Type u_1
m : MeasurableSpace α
s : Finset ι
f : α → ℝ≥0∞
μ : ι → Measure α
⊢ (∑' (i : { x // x ∈ s }), ∫⁻ (a : α), f a ∂μ ↑i) = ∑' (x : ↑↑s), ∫⁻ (a : α), f a ∂μ ↑x
α : Type u_2
β : Type ?u.921513
γ : Type ?u.921516
δ : Type ?u.921519
m✝ : MeasurableSpace α
μ✝ ν : Measure α
ι : Type u_1
m : MeasurableSpace α
s : Finset ι
f : α → ℝ≥0∞
μ : ι → Measure α
⊢ (∫⁻ (a : α), f a ∂∑ i in s, μ i) = ∑ i in s, ∫⁻ (a : α), f a ∂μ i
rw [← Measure.sum_coe_finset, lintegral_sum_measure, ← Finset.tsum_subtype']
no goals
α : Type u_2
β : Type ?u.921513
γ : Type ?u.921516
δ : Type ?u.921519
m✝ : MeasurableSpace α
μ✝ ν : Measure α
ι : Type u_1
m : MeasurableSpace α
s : Finset ι
f : α → ℝ≥0∞
μ : ι → Measure α
⊢ (∑' (i : { x // x ∈ s }), ∫⁻ (a : α), f a ∂μ ↑i) = ∑' (x : ↑↑s), ∫⁻ (a : α), f a ∂μ ↑x
rfl