2025-09-26 11:33
Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean
feat(MeasureTheory/ProbabilityTheory): `Is(Probability/Finite)Measure` iff map `Is(Probability/Finite)Measure` (#29922) …
Added MeasureTheory.Measure.isProbabilityMeasure_of_map