no goals
α : Type u_1
β : Type ?u.576854
γ : Type ?u.576857
δ : Type ?u.576860
ι : Type ?u.576863
R : Type ?u.576866
R' : Type ?u.576869
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ t : Set α
p : α → Prop
ht : ∀ᵐ (x : α) ∂Measure.restrict μ t, p x
htc : ∀ᵐ (x : α) ∂Measure.restrict μ (tᶜ), p x
⊢ ↑↑μ {x | ¬p x} = ↑↑μ ({x | ¬p x} ∩ t ∪ {x | ¬p x} ∩ tᶜ)
rw [← inter_union_distrib_left, union_compl_self, inter_univ]
no goals
α : Type u_1
β : Type ?u.576854
γ : Type ?u.576857
δ : Type ?u.576860
ι : Type ?u.576863
R : Type ?u.576866
R' : Type ?u.576869
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ t : Set α
p : α → Prop
ht : ∀ᵐ (x : α) ∂Measure.restrict μ t, p x
htc : ∀ᵐ (x : α) ∂Measure.restrict μ (tᶜ), p x
⊢ ↑↑(Measure.restrict μ t) {x | ¬p x} + ↑↑(Measure.restrict μ (tᶜ)) {x | ¬p x} = 0
rw [ae_iff.1 ht, ae_iff.1 htc, zero_add]