no goals
α : Type u_1
β : Type ?u.84148
γ : Type ?u.84151
inst✝ : MeasurableSpace α
p : Pmf α
s t : Set α
hs : MeasurableSet s
⊢ ↑↑(toMeasure p) s = 0 ↔ Disjoint (support p) s
rw [toMeasure_apply_eq_toOuterMeasure_apply p s hs, toOuterMeasure_apply_eq_zero_iff]