α : Type u_1
β : Type ?u.567121
γ : Type ?u.567124
δ : Type ?u.567127
ι : Type ?u.567130
R : Type ?u.567133
R' : Type ?u.567136
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
p : α → Prop
hp : MeasurableSet {x | p x}
⊢ ↑↑μ ({x | p x}ᶜ ∩ s) = 0 ↔ ↑↑μ ({x | x ∈ s → p x}ᶜ) = 0
α : Type u_1
β : Type ?u.567121
γ : Type ?u.567124
δ : Type ?u.567127
ι : Type ?u.567130
R : Type ?u.567133
R' : Type ?u.567136
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
p : α → Prop
hp : MeasurableSet {x | p x}
⊢ (∀ᵐ (x : α) ∂Measure.restrict μ s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x
simp only [ae_iff, ← compl_setOf, Measure.restrict_apply hp.compl]
α : Type u_1
β : Type ?u.567121
γ : Type ?u.567124
δ : Type ?u.567127
ι : Type ?u.567130
R : Type ?u.567133
R' : Type ?u.567136
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
p : α → Prop
hp : MeasurableSet {x | p x}
⊢ (↑↑μ ({x | p x}ᶜ ∩ s) = 0) = (↑↑μ ({x | x ∈ s → p x}ᶜ) = 0)
α : Type u_1
β : Type ?u.567121
γ : Type ?u.567124
δ : Type ?u.567127
ι : Type ?u.567130
R : Type ?u.567133
R' : Type ?u.567136
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
p : α → Prop
hp : MeasurableSet {x | p x}
⊢ ↑↑μ ({x | p x}ᶜ ∩ s) = 0 ↔ ↑↑μ ({x | x ∈ s → p x}ᶜ) = 0
rw [iff_iff_eq]
case e_a.e_a.h
α : Type u_1
β : Type ?u.567121
γ : Type ?u.567124
δ : Type ?u.567127
ι : Type ?u.567130
R : Type ?u.567133
R' : Type ?u.567136
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
p : α → Prop
hp : MeasurableSet {x | p x}
x : α
⊢ x ∈ {x | p x}ᶜ ∩ s ↔ x ∈ {x | x ∈ s → p x}ᶜ
α : Type u_1
β : Type ?u.567121
γ : Type ?u.567124
δ : Type ?u.567127
ι : Type ?u.567130
R : Type ?u.567133
R' : Type ?u.567136
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
p : α → Prop
hp : MeasurableSet {x | p x}
⊢ (↑↑μ ({x | p x}ᶜ ∩ s) = 0) = (↑↑μ ({x | x ∈ s → p x}ᶜ) = 0)
congr with x
no goals
case e_a.e_a.h
α : Type u_1
β : Type ?u.567121
γ : Type ?u.567124
δ : Type ?u.567127
ι : Type ?u.567130
R : Type ?u.567133
R' : Type ?u.567136
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
p : α → Prop
hp : MeasurableSet {x | p x}
x : α
⊢ x ∈ {x | p x}ᶜ ∩ s ↔ x ∈ {x | x ∈ s → p x}ᶜ
simp [and_comm]