Commit 2023-05-10 01:01 68ec2198

View on Github →

feat: port MeasureTheory.Measure.OpenPos (#3820)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/OpenPos.lean

added theorem Continuous.ae_eq_iff_eq

added theorem EMetric.measure_ball_pos

added theorem EMetric.measure_closedBall_pos

added theorem IsOpen.eq_empty_of_measure_zero

added theorem IsOpen.measure_eq_zero_iff

added theorem IsOpen.measure_ne_zero

added theorem IsOpen.measure_pos

added theorem IsOpen.measure_pos_iff

added theorem LE.le.isOpenPosMeasure

added theorem MeasureTheory.Measure.eqOn_Icc_of_ae_eq

added theorem MeasureTheory.Measure.eqOn_Ico_of_ae_eq

added theorem MeasureTheory.Measure.eqOn_Ioc_of_ae_eq

added theorem MeasureTheory.Measure.eqOn_Ioo_of_ae_eq

added theorem MeasureTheory.Measure.eqOn_of_ae_eq

added theorem MeasureTheory.Measure.eqOn_open_of_ae_eq

added theorem MeasureTheory.Measure.eq_of_ae_eq

added theorem MeasureTheory.Measure.interior_eq_empty_of_null

added theorem MeasureTheory.Measure.measure_Iio_pos

added theorem MeasureTheory.Measure.measure_Ioi_pos

added theorem MeasureTheory.Measure.measure_Ioo_eq_zero

added theorem MeasureTheory.Measure.measure_Ioo_pos

added theorem MeasureTheory.Measure.measure_pos_of_mem_nhds

added theorem MeasureTheory.Measure.measure_pos_of_nonempty_interior

added theorem MeasureTheory.Measure.openPosMeasure_smul

added theorem Metric.measure_ball_pos

added theorem Metric.measure_closedBall_pos