Commit 2023-05-09 05:50 773a35f7

View on Github →

feat: port MeasureTheory.Measure.MeasureSpace (#3324) This PR also renames instances in MeasureTheory.MeasurableSpace.

Estimated changes

added theorem Finset.measure_zero
added theorem MeasurableEquiv.map_ae
added theorem MeasureTheory.ae_mono
added theorem MeasureTheory.ae_neBot
added theorem MeasureTheory.ae_zero
added theorem MeasureTheory.le_trim
added theorem indicator_meas_zero
added theorem map_comap_subtype_coe
added theorem measure_Icc_lt_top
added theorem measure_Ico_lt_top
added theorem measure_Ioc_lt_top
added theorem measure_Ioo_lt_top
added theorem volume_preimage_coe
added theorem volume_set_coe_def