α : Type u_1
β : Type ?u.101868
γ : Type ?u.101871
δ : Type ?u.101874
ι : Type ?u.101877
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ ↑↑μ {a | a ∈ s ∧ ¬a ∈ t} = 0 ↔ ↑↑μ (s \ t) = 0
α : Type u_1
β : Type ?u.101868
γ : Type ?u.101871
δ : Type ?u.101874
ι : Type ?u.101877
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ (∀ᵐ (x : α) ∂μ, x ∈ s → x ∈ t) ↔ ↑↑μ (s \ t) = 0
simp [ae_iff]
no goals
α : Type u_1
β : Type ?u.101868
γ : Type ?u.101871
δ : Type ?u.101874
ι : Type ?u.101877
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ ↑↑μ {a | a ∈ s ∧ ¬a ∈ t} = 0 ↔ ↑↑μ (s \ t) = 0
rfl