α : Type u_1
β : Type ?u.134378
γ : Type ?u.134381
δ : Type ?u.134384
ι : Type ?u.134387
R : Type ?u.134390
R' : Type ?u.134393
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
p : α → Prop
c : ℝ≥0∞
hc : c ≠ 0
⊢ c = 0 → ↑↑μ {a | ¬p a} = 0
α : Type u_1
β : Type ?u.134378
γ : Type ?u.134381
δ : Type ?u.134384
ι : Type ?u.134387
R : Type ?u.134390
R' : Type ?u.134393
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
p : α → Prop
c : ℝ≥0∞
hc : c ≠ 0
⊢ (∀ᵐ (x : α) ∂c • μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p x
simp only [ae_iff, Algebra.id.smul_eq_mul, smul_apply, or_iff_right_iff_imp, mul_eq_zero]
no goals
α : Type u_1
β : Type ?u.134378
γ : Type ?u.134381
δ : Type ?u.134384
ι : Type ?u.134387
R : Type ?u.134390
R' : Type ?u.134393
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
p : α → Prop
c : ℝ≥0∞
hc : c ≠ 0
⊢ c = 0 → ↑↑μ {a | ¬p a} = 0
simp only [IsEmpty.forall_iff, hc]