mathlib3

aacd7575 - feat(measurable_space): more properties of measurable sets in a product (#3703)

feat(measurable_space): more properties of measurable sets in a product (#3703) Add multiple lemmas about `prod` to `set.basic` Some cleanup in `set.basic` Fix the name of the instance `measure_space ℝ` Cleanup and a couple of additions to the `prod` section of `measurable_space`. Rename: `prod_singleton_singleton` -> `singleton_prod_singleton` Use `prod.swap` in the statement of `image_swap_prod`.