Commit 2023-10-17 10:36 3759c6d3

View on Github →

feat: simple lemmas about withDensity (#7714)

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

added theorem MeasureTheory.set_lintegral_smul_measure

Modified Mathlib/MeasureTheory/Measure/AEMeasurable.lean

added theorem AEMeasurable.mono_ac

Modified Mathlib/MeasureTheory/Measure/WithDensity.lean

added theorem MeasureTheory.withDensity_const

added theorem MeasureTheory.withDensity_smul_measure

added theorem MeasureTheory.withDensity_zero_left