Theorem MeasureTheory.ProbabilityMeasure.measurableSet_isProbabilityMeasure

Modification history

2025-03-06 11:11
Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
feat: Giry monoidal product (#22062) …
Added MeasureTheory.ProbabilityMeasure.measurableSet_isProbabilityMeasureView on Github →