mathlib
99693218 - feat(measure_theory/probability_mass_function): Lemmas connecting `pmf.support` and `pmf.to_measure` (#11842)

Commit

3 years ago

feat(measure_theory/probability_mass_function): Lemmas connecting `pmf.support` and `pmf.to_measure` (#11842) Add lemmas relating the support of a `pmf` to the measures of sets under the induced measure.

Author

dtumad

Parents

612ca40a

mathlib 99693218 - feat(measure_theory/probability_mass_function): Lemmas connecting `pmf.support` and `pmf.to_measure` (#11842)

mathlib
99693218 - feat(measure_theory/probability_mass_function): Lemmas connecting `pmf.support` and `pmf.to_measure` (#11842)