Theorem MeasureTheory.aEMeasurable_withDensity_eNNReal_iff

Modification history

2023-05-26 09:28
Mathlib/MeasureTheory/Integral/Lebesgue.lean
style(MeasureTheory/Integral/Lebesgue): rename `aEMeasurable_withDensity_eNNReal_iff` to `aemeasurable_withDensity_ennreal_iff` (#4379)
Deleted MeasureTheory.aEMeasurable_withDensity_eNNReal_iffView on Github →
2023-05-21 17:05
Mathlib/MeasureTheory/Integral/Lebesgue.lean
feat: port MeasureTheory.Integral.Lebesgue (#4058)
Added MeasureTheory.aEMeasurable_withDensity_eNNReal_iffView on Github →