Commit 2021-01-14 11:59 3b3f9a21
View on Github →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 notis_measurable s
/measurable f
under the old name. - rename some lemmas from
eventually
toae
.