Commit 2023-12-17 17:55 9764993a

View on Github →

feat: Checking ae on a countable type (#8945) and other simple measure lemmas From PFR and LeanCamCombi

Estimated changes

Modified Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

Modified Mathlib/MeasureTheory/Measure/AEMeasurable.lean

Modified Mathlib/MeasureTheory/Measure/Dirac.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem AEMeasurable.nullMeasurableSet_preimage

added theorem MeasureTheory.Measure.absolutelyContinuous_smul

modified theorem MeasureTheory.Measure.map_apply

modified theorem MeasureTheory.Measure.map_apply_of_aemeasurable

added theorem MeasureTheory.Measure.map_eq_zero_iff

added theorem MeasureTheory.Measure.map_ne_zero_iff

modified theorem MeasureTheory.Measure.map_toOuterMeasure

added theorem MeasureTheory.Measure.mapₗ_eq_zero_iff

added theorem MeasureTheory.Measure.mapₗ_ne_zero_iff

added theorem MeasureTheory.Measure.smul_absolutelyContinuous

modified theorem MeasureTheory.measure_compl

added theorem MeasureTheory.measure_compl₀

added theorem MeasureTheory.measure_inter_conull'

added theorem MeasureTheory.measure_inter_conull

added theorem MeasureTheory.measure_preimage_eq_zero_iff_of_countable

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

modified theorem MeasureTheory.ae_ball_iff

added theorem MeasureTheory.ae_iff_of_countable

added theorem MeasureTheory.measure_null_iff_singleton