Commit 2023-12-18 19:32 564283d7

View on Github →

feat: Comap of a probability measure under an ae surjective embedding (#8954) From PFR

Estimated changes

Modified Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

added theorem MeasureTheory.ProbabilityMeasure.coe_mk

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

added theorem MeasureTheory.ae_iff_prob_eq_one

added theorem MeasureTheory.isProbabilityMeasure_comap

added theorem MeasureTheory.isProbabilityMeasure_iff

added theorem MeasureTheory.mem_ae_iff_prob_eq_one