Theorem MeasureTheory.dirac_eq_zero_iff_not_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_zero_iff_not_memView on Github →