mathlib

2026a5f7 - feat(measure_theory/measure): better `measure.restrict_singleton` (#9936)

feat(measure_theory/measure): better `measure.restrict_singleton` (#9936) With new `restrict_singleton`, `simp` can simplify `∫ x in {a}, f x ∂μ` to `(μ {a}).to_real • f a`.