α : Type u_1
β : Type ?u.569665
γ : Type ?u.569668
δ : Type ?u.569671
ι : Type ?u.569674
R : Type ?u.569677
R' : Type ?u.569680
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t s : Set α
p : α → Prop
h : ↑↑(Measure.restrict μ s) {a | ¬p a} = 0
⊢ ↑↑μ {a | ¬(a ∈ s → p a)} = 0
α : Type u_1
β : Type ?u.569665
γ : Type ?u.569668
δ : Type ?u.569671
ι : Type ?u.569674
R : Type ?u.569677
R' : Type ?u.569680
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t s : Set α
p : α → Prop
h : ∀ᵐ (x : α) ∂Measure.restrict μ s, p x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → p x
simp only [ae_iff] at h⊢
no goals
α : Type u_1
β : Type ?u.569665
γ : Type ?u.569668
δ : Type ?u.569671
ι : Type ?u.569674
R : Type ?u.569677
R' : Type ?u.569680
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t s : Set α
p : α → Prop
h : ↑↑(Measure.restrict μ s) {a | ¬p a} = 0
⊢ ↑↑μ {a | ¬(a ∈ s → p a)} = 0
simpa [setOf_and, inter_comm] using measure_inter_eq_zero_of_restrict h