Theorem MeasureTheory.aemeasurable_withDensity_ennreal_iff

Modification history

2023-10-05 17:31
Mathlib/MeasureTheory/Integral/Lebesgue.lean
chore: put Measure.withDensity into a new file (#7508) …
Modified MeasureTheory.aemeasurable_withDensity_ennreal_iffView on Github →
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)
Added MeasureTheory.aemeasurable_withDensity_ennreal_iffView on Github →