Commit 2025-06-09 15:56 4141bd5e

feat (MeasureTheory/Measure/Dirac): a point being in a measurable set is equivalent with dirac measure evaluation (#25396) Mathlib has mem_ae_dirac_iff that provides s ∈ ae (dirac a) ↔ a ∈ s, which expands to (dirac a) sᶜ = 0 ↔ a ∈ s. A more natural statement (arguably) is (dirac a) s = 1 ↔ a ∈ s. This feature adds (dirac a) s = 1 ↔ a ∈ s and a companion theorem (dirac a) s = 0 ↔ a ∉ s. As an example, suppose we have

hs : MeasurableSet s
this : f i ∈ s
⊢ (dirac (f i)) s = 1

This goal can be closed with rwa [mem_dirac_eq_one_iff hs] if this feature is merged. (Note, the proofs depend on dirac being a ProbabilityMeasure, hence why the theorems are where they are in Dirac.lean.)