no goals
α : Type u_1
β : Type ?u.101184
γ : Type ?u.101187
δ : Type ?u.101190
ι : Type ?u.101193
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ (∀ᵐ (x : α) ∂μ, ¬x ∈ s) ↔ ↑↑μ s = 0
simp only [ae_iff, Classical.not_not, setOf_mem_eq]