Commit 2024-08-30 10:14 c34aad51

View on Github →

chore: Make measurability of sets/functions in discrete spaces available with anonymous dot notation (#16136) From LeanAPAP

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

Modified Mathlib/MeasureTheory/Group/Arithmetic.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Defs.lean

added theorem Measurable.of_discrete

added theorem MeasurableSet.of_discrete

modified theorem measurableSet_discrete

modified theorem measurable_discrete

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

added theorem AEMeasurable.of_discrete