mathlib3

8ab1b3b4 - feat(measure_theory/probability_mass_function): Calculate supports of pmf constructions (#10371)

feat(measure_theory/probability_mass_function): Calculate supports of pmf constructions (#10371) This PR gives explicit descriptions for the `support` of the various `pmf` constructions in mathlib. This also tries to clean up the variable declarations in the different sections, so that all the lemmas don't need to specify them explicitly.