Theorem MeasureTheory.IsZeroOneMeasure.exists_eq_dirac

Modification history

2026-10-16 13:06

Mathlib/MeasureTheory/Constructions/Polish/Basic.lean

refactor(MeasureTheory/Measure/Typeclasses/ZeroOne): reduce imports (#44931) …

Modified MeasureTheory.IsZeroOneMeasure.exists_eq_dirac View on Github →

2026-05-04 16:33

Mathlib/MeasureTheory/Measure/Typeclasses/ZeroOne.lean

feat(Probability/Kernel): define `IsDeterministic` (#38211) …

Added MeasureTheory.IsZeroOneMeasure.exists_eq_dirac View on Github →