Theorem MeasureTheory.dirac_eq_one_iff_mem

Modification history

2025-06-09 15:56
Mathlib/MeasureTheory/Measure/Dirac.lean
feat (MeasureTheory/Measure/Dirac): a point being in a measurable set is equivalent with dirac measure evaluation (#25396) …
Added MeasureTheory.dirac_eq_one_iff_memView on Github →