α : Type u_2
β : Type ?u.302552
γ : Type ?u.302555
δ : Type ?u.302558
ι : Type u_1
R : Type ?u.302564
R' : Type ?u.302567
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
hm : ∀ (i : ι), NullMeasurableSet (s i)
t : Set α
ht : MeasurableSet t
⊢ ↑↑μ (⋃ (i : ι), t ∩ s i) = ∑' (i : ι), ↑↑μ (t ∩ s i)
α : Type u_2
β : Type ?u.302552
γ : Type ?u.302555
δ : Type ?u.302558
ι : Type u_1
R : Type ?u.302564
R' : Type ?u.302567
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
hm : ∀ (i : ι), NullMeasurableSet (s i)
t : Set α
ht : MeasurableSet t
⊢ ↑↑(restrict μ (⋃ (i : ι), s i)) t = ∑' (i : ι), ↑↑(restrict μ (s i)) t
simp only [restrict_apply, ht, inter_iUnion]
no goals
α : Type u_2
β : Type ?u.302552
γ : Type ?u.302555
δ : Type ?u.302558
ι : Type u_1
R : Type ?u.302564
R' : Type ?u.302567
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
hm : ∀ (i : ι), NullMeasurableSet (s i)
t : Set α
ht : MeasurableSet t
⊢ ↑↑μ (⋃ (i : ι), t ∩ s i) = ∑' (i : ι), ↑↑μ (t ∩ s i)
exact
  measure_iUnion₀ (hd.mono fun i j h => h.mono (inter_subset_right _ _) (inter_subset_right _ _))
    fun i => ht.nullMeasurableSet.inter (hm i)