Theorem MeasureTheory.Measure.isProbabilityMeasure_of_map

Modification history

2026-08-26 08:21
Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean
refactor: change the default value of `Measure.map` to a Dirac mass (#42322) …
Modified MeasureTheory.Measure.isProbabilityMeasure_of_mapView on Github →
2025-12-01 09:24
Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean
feat: drop a measurability assumption (#32280) …
Modified MeasureTheory.Measure.isProbabilityMeasure_of_mapView on Github →
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_mapView on Github →