Theorem MeasureTheory.Measure.map_dirac'

Modification history

2026-03-02 10:08

Mathlib/MeasureTheory/Measure/Dirac.lean

feat(MeasureTheory): Add `MeasurableSingletonClass` version of `Measure.map_dirac` (#35784) …

Added MeasureTheory.Measure.map_dirac'View on Github →