Commit 2023-12-08 12:07 62d6feff

View on Github →

feat: Discrete measurable spaces (#8859) Adds a typeclass for measurable spaces where all sets are measurable Proves several instances relating these to other classes

Estimated changes

Modified Mathlib/MeasureTheory/Group/Arithmetic.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Defs.lean

deleted theorem MeasurableSpace.Top.measurable

added theorem measurableSet_discrete

added theorem measurable_discrete

Modified Mathlib/MeasureTheory/Measure/Dirac.lean