Commit 2024-09-17 19:29 78022fea

View on Github →

feat(MeasureTheory/Borel): add nullMeasurable_Ixx (#16829)

Estimated changes

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

added theorem nullMeasurableSet_Icc

added theorem nullMeasurableSet_Ici

added theorem nullMeasurableSet_Ico

added theorem nullMeasurableSet_Iic

added theorem nullMeasurableSet_Iio

added theorem nullMeasurableSet_Ioc

added theorem nullMeasurableSet_Ioi

added theorem nullMeasurableSet_Ioo

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

Modified Mathlib/MeasureTheory/Constructions/UnitInterval.lean

Modified Mathlib/MeasureTheory/Decomposition/UnsignedHahn.lean

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

Modified Mathlib/MeasureTheory/Integral/Periodic.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/MeasureTheory/Measure/NullMeasurable.lean

Modified Mathlib/MeasureTheory/Measure/Regular.lean

Modified Mathlib/MeasureTheory/Measure/Stieltjes.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

Modified Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean