Theorem MeasureTheory.IsZeroOneMeasure.exists_measure_eq_one_iff_measure_univ_eq_one

Modification history

2026-05-04 16:33
Mathlib/MeasureTheory/Measure/Typeclasses/ZeroOne.lean
feat(Probability/Kernel): define `IsDeterministic` (#38211) …
Added MeasureTheory.IsZeroOneMeasure.exists_measure_eq_one_iff_measure_univ_eq_oneView on Github →