α : Type u_1
β : Type ?u.25862
γ : Type ?u.25865
p : Pmf α
s t : Set α
⊢ (∀ (i : α), Set.indicator s (↑p) i = 0) ↔ Disjoint (support p) s
α : Type u_1
β : Type ?u.25862
γ : Type ?u.25865
p : Pmf α
s t : Set α
⊢ ↑(toOuterMeasure p) s = 0 ↔ Disjoint (support p) s
rw [toOuterMeasure_apply, ENNReal.tsum_eq_zero]
no goals
α : Type u_1
β : Type ?u.25862
γ : Type ?u.25865
p : Pmf α
s t : Set α
⊢ (∀ (i : α), Set.indicator s (↑p) i = 0) ↔ Disjoint (support p) s
exact Function.funext_iff.symm.trans Set.indicator_eq_zero'