Commit 2021-11-10 14:52 bbbefe4e

View on Github →

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.

Estimated changes

Modified src/data/equiv/list.lean

modified theorem encodable.length_sorted_univ

modified theorem encodable.mem_sorted_univ

modified theorem encodable.sorted_univ_nodup

added theorem encodable.sorted_univ_to_finset

Modified src/measure_theory/constructions/pi.lean

added theorem measure_theory.measure.pi'_eq_pi

modified theorem measure_theory.measure.pi'_pi

deleted theorem measure_theory.measure.pi'_pi_le

modified theorem measure_theory.measure.pi_ball

modified theorem measure_theory.measure.pi_closed_ball

modified theorem measure_theory.measure.pi_pi

added theorem measure_theory.measure.pi_pi_aux

modified theorem measure_theory.measure.pi_univ

deleted theorem measure_theory.measure.tprod_tprod_le

Modified src/measure_theory/constructions/prod.lean

modified theorem measure_theory.measure.prod_prod

deleted theorem measure_theory.measure.prod_prod_le

modified theorem measure_theory.measure.prod_restrict

modified theorem measure_theory.measure.restrict_prod_eq_prod_univ

added theorem measure_theory.set_integral_prod

Modified src/measure_theory/group/arithmetic.lean

added theorem measurable_set.inv

Modified src/measure_theory/group/prod.lean

modified theorem measure_theory.measure_inv_null

modified theorem measure_theory.measure_mul_right_ne_zero

modified theorem measure_theory.measure_mul_right_null

deleted theorem measure_theory.measure_null_of_measure_inv_null

added theorem measure_theory.quasi_measure_preserving_inv

Modified src/measure_theory/measure/haar_lebesgue.lean

Modified src/measure_theory/measure/hausdorff.lean

Modified src/measure_theory/measure/lebesgue.lean

Modified src/measure_theory/measure/measure_space.lean

added theorem measure_theory.measure.quasi_measure_preserving.preimage_null