case h.e'_2.h.e'_7.h.e'_4.h.e'_3.h
α : Type u_2
β : Type ?u.19521
E : Type u_3
F : Type ?u.19527
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f g : α → E
s✝ t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_1
inst✝ : Fintype ι
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), IntegrableOn f (s i)
x✝ : ι
⊢ s x✝ = ⋃ (_ : x✝ ∈ Finset.univ), s x✝

α : Type u_2
β : Type ?u.19521
E : Type u_3
F : Type ?u.19527
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f g : α → E
s✝ t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_1
inst✝ : Fintype ι
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), IntegrableOn f (s i)
⊢ Set.Pairwise (↑Finset.univ) (Disjoint on fun i => s i)
α : Type u_2
β : Type ?u.19521
E : Type u_3
F : Type ?u.19527
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f g : α → E
s✝ t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_1
inst✝ : Fintype ι
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), IntegrableOn f (s i)
⊢ (∫ (x : α) in ⋃ (i : ι), s i, f x ∂μ) = ∑ i : ι, ∫ (x : α) in s i, f x ∂μ
convert integral_finset_biUnion Finset.univ (fun i _ => hs i) _ fun i _ => hf i
no goals
case h.e'_2.h.e'_7.h.e'_4.h.e'_3.h
α : Type u_2
β : Type ?u.19521
E : Type u_3
F : Type ?u.19527
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f g : α → E
s✝ t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_1
inst✝ : Fintype ι
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), IntegrableOn f (s i)
x✝ : ι
⊢ s x✝ = ⋃ (_ : x✝ ∈ Finset.univ), s x✝
simp
no goals
α : Type u_2
β : Type ?u.19521
E : Type u_3
F : Type ?u.19527
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f g : α → E
s✝ t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_1
inst✝ : Fintype ι
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), IntegrableOn f (s i)
⊢ Set.Pairwise (↑Finset.univ) (Disjoint on fun i => s i)
simp [pairwise_univ, h's]