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 →