mathlib

6375f851 - feat(measure_theory/probability_mass_function): Probability one iff support equals singleton (#15334)