proposition: Lemma eq0_pr A mu : (forall x, x \in dinsupp mu -> x \notin A) -> \P_[mu] A = 0.
proof: Proof. move=> h; apply/psum_eq0=> x; apply/eqP. rewrite mulf_eq0 orbC; case/boolP: (mu x == 0) => //=. by move/h; rewrite -topredE /= => /negbTE->. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum