Commit 2025-05-26 12:19 1454c2fc

feat(MeasureTheory/Measure/Dirac): Dirac measure applied to a set is either 0 or 1 (#24616) The Dirac measure at a point a, applied to a set s, is either 0 or 1. This feature provides two if and only ifs that can be used to turn statements in terms of \ne into statements in terms of =, as well as a "0 or 1 theorem". (The reason for adding these is to avoid having to simplify in terms of Set.indicator over and over while working with Dirac)