{pi,prod}): drop some measurability assumptions (#10241)

Commit

4 years ago

feat(measure_theory/constructions/{pi,prod}): drop some measurability assumptions (#10241) Some lemmas (most notably `prod_prod` and `pi_pi`) are true for non-measurable sets as well.

Author

urkud

Parents

eadd4400

mathlib bbbefe4e - feat(measure_theory/constructions/{pi,prod}): drop some measurability assumptions (#10241)

mathlib
bbbefe4e - feat(measure_theory/constructions/{pi,prod}): drop some measurability assumptions (#10241)