α : Type u_1
β : Type ?u.405254
γ : Type ?u.405257
δ : Type ?u.405260
ι : Type ?u.405263
R : Type ?u.405266
R' : Type ?u.405269
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
h : ae μ ≤ ae ν
s : Set α
⊢ (∀ᵐ (a : α) ∂ν, ¬a ∈ s) → ∀ᵐ (a : α) ∂μ, ¬a ∈ s
α : Type u_1
β : Type ?u.405254
γ : Type ?u.405257
δ : Type ?u.405260
ι : Type ?u.405263
R : Type ?u.405266
R' : Type ?u.405269
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
h : ae μ ≤ ae ν
s : Set α
⊢ ↑↑ν s = 0 → ↑↑μ s = 0
rw [measure_zero_iff_ae_nmem, measure_zero_iff_ae_nmem]
no goals
α : Type u_1
β : Type ?u.405254
γ : Type ?u.405257
δ : Type ?u.405260
ι : Type ?u.405263
R : Type ?u.405266
R' : Type ?u.405269
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
h : ae μ ≤ ae ν
s : Set α
⊢ (∀ᵐ (a : α) ∂ν, ¬a ∈ s) → ∀ᵐ (a : α) ∂μ, ¬a ∈ s
exact fun hs => h hs