Commit 2024-08-30 10:14 283ca404

View on Github →

chore(MeasureTheory): generalize to NullMeasurableSet (#16279) Generalize some lemmas from MeasurableSets to NullMeasurableSets.

Estimated changes

Modified Mathlib/Analysis/Convex/Measure.lean

Modified Mathlib/Dynamics/Ergodic/Ergodic.lean

modified theorem Ergodic.ae_empty_or_univ_of_ae_le_preimage'

modified theorem Ergodic.ae_empty_or_univ_of_ae_le_preimage

modified theorem Ergodic.ae_empty_or_univ_of_image_ae_le'

modified theorem Ergodic.ae_empty_or_univ_of_image_ae_le

modified theorem Ergodic.ae_empty_or_univ_of_preimage_ae_le'

modified theorem Ergodic.ae_empty_or_univ_of_preimage_ae_le

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

added theorem IsCompact.nullMeasurableSet

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

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

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

Modified Mathlib/MeasureTheory/Covering/Besicovitch.lean

Modified Mathlib/MeasureTheory/Decomposition/UnsignedHahn.lean

Modified Mathlib/MeasureTheory/Function/Egorov.lean

Modified Mathlib/MeasureTheory/Group/AddCircle.lean

Modified Mathlib/MeasureTheory/Group/Measure.lean

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

Modified Mathlib/MeasureTheory/Measure/ContinuousPreimage.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Unique.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

Modified Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

modified theorem MeasureTheory.ae_eq_of_ae_subset_of_measure_ge

modified theorem MeasureTheory.ae_eq_of_subset_of_measure_ge

modified theorem MeasureTheory.measure_add_diff

modified theorem MeasureTheory.measure_diff'

modified theorem MeasureTheory.measure_diff

modified theorem MeasureTheory.measure_diff_le_iff_le_add

modified theorem MeasureTheory.measure_diff_lt_of_lt_add

modified theorem MeasureTheory.measure_iInter_eq_iInf

modified theorem MeasureTheory.measure_symmDiff_eq

Modified Mathlib/MeasureTheory/Measure/Regular.lean

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

Modified Mathlib/MeasureTheory/Measure/Stieltjes.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

Modified Mathlib/MeasureTheory/Order/UpperLower.lean

Modified Mathlib/NumberTheory/WellApproximable.lean

Modified Mathlib/Probability/Independence/Kernel.lean

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

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

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

Modified Mathlib/Probability/Kernel/MeasurableIntegral.lean