Commit 2021-10-26 07:25 f229c83c

chore(*): move 2 lemmas to reorder imports (#9969) I want to use measure_theory.measure_preserving in various files, including measure_theory.integral.lebesgue. The file about measure preserving map had two lemmas about product measures. I move them to measure_theory.constructions.prod. I also golfed (and made it more readable at the same time!) the proof of measure_theory.measure.prod_prod_le using to_measurable_set.