Theorem MeasureTheory.probReal_compl_eq_one_sub

Modification history

2025-11-24 17:30

Mathlib/MeasureTheory/Measure/Real.lean

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

Added MeasureTheory.probReal_compl_eq_one_sub View on Github →