mathlib3

3b3f9a21 - refactor(measure_theory): review def&API of the `dirac` measure (#5732)

refactor(measure_theory): review def&API of the `dirac` measure (#5732) * use `set.indicator` instead of `⨆ a ∈ s, 1` in the definition. * rename some theorems to `thm'`, add a version assuming `[measurable_singleton_class α]` but not `is_measurable s`/`measurable f` under the old name. * rename some lemmas from `eventually` to `ae`. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>