no goals
α : Type u_1
β : Type ?u.292265
γ : Type ?u.292268
δ : Type ?u.292271
ι : Type ?u.292274
R : Type ?u.292277
R' : Type ?u.292280
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
⊢ restrict μ s = 0 ↔ ↑↑μ s = 0
rw [← measure_univ_eq_zero, restrict_apply_univ]