Theorem MeasureTheory.probReal_univ

Modification history

2025-11-24 17:30

Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean

feat(MeasureTheory): `Measure.real` of a probability measure (#31942)

Added MeasureTheory.probReal_univ View on Github →