Commit 2023-10-09 05:50 0cb70832

View on Github →

feat(MeasureTheory/../Prod): add lemmas about NullMeasurableSet (#7578) Also golf a proof. The informal proof was provided by Felix Weilacher on Zulip.

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Prod/Basic.lean

added theorem MeasureTheory.Measure.ae_ae_eq_curry_of_prod

added theorem MeasureTheory.Measure.ae_ae_eq_of_ae_eq_uncurry

added theorem MeasureTheory.Measure.nullMeasurableSet_prod

added theorem MeasureTheory.Measure.nullMeasurableSet_prod_of_ne_zero

added theorem MeasureTheory.Measure.set_prod_ae_eq

added theorem MeasureTheory.NullMeasurableSet.left_of_prod

added theorem MeasureTheory.NullMeasurableSet.right_of_prod