Commit 2021-09-19 10:06 383e05a2

View on Github →

feat(measure_theory/integral/lebesgue): add set version of lintegral_with_density_eq_lintegral_mul (#9270) I also made measurable_space α an implicit argument whenever μ : measure α is explicit.

Estimated changes

Modified src/measure_theory/integral/lebesgue.lean

modified theorem measure_theory.lintegral_trim

modified theorem measure_theory.lintegral_trim_ae

modified theorem measure_theory.lintegral_with_density_eq_lintegral_mul

added theorem measure_theory.restrict_with_density

added theorem measure_theory.set_lintegral_with_density_eq_set_lintegral_mul