lebesgue): add set version of `lintegral_with_density_eq_lintegral_mul` (#9270)

Commit

4 years ago

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.

Author

kex-y

Parents

25e67dd8

mathlib 383e05a2 - feat(measure_theory/integral/lebesgue): add set version of `lintegral_with_density_eq_lintegral_mul` (#9270)

mathlib
383e05a2 - feat(measure_theory/integral/lebesgue): add set version of `lintegral_with_density_eq_lintegral_mul` (#9270)