Commit 2023-05-21 16:29 d05ddafb

View on Github →

feat: port MeasureTheory.Measure.Regular (#4101)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/Regular.lean

added theorem IsOpen.exists_lt_isClosed

added theorem IsOpen.exists_lt_isCompact

added theorem IsOpen.measure_eq_iSup_isClosed

added theorem IsOpen.measure_eq_iSup_isCompact

added theorem MeasurableSet.exists_isClosed_diff_lt

added theorem MeasurableSet.exists_isClosed_lt_add

added theorem MeasurableSet.exists_isCompact_diff_lt

added theorem MeasurableSet.exists_isCompact_lt_add

added theorem MeasurableSet.exists_isOpen_diff_lt

added theorem MeasurableSet.exists_lt_isClosed_of_ne_top

added theorem MeasurableSet.exists_lt_isCompact_of_ne_top

added theorem MeasurableSet.measure_eq_iSup_isClosed_of_ne_top

added theorem MeasurableSet.measure_eq_iSup_isCompact_of_ne_top

added theorem MeasureTheory.Measure.InnerRegular.exists_subset_lt_add

added theorem MeasureTheory.Measure.InnerRegular.isCompact_isClosed

added theorem MeasureTheory.Measure.InnerRegular.map

added theorem MeasureTheory.Measure.InnerRegular.measurableSet_of_open

added theorem MeasureTheory.Measure.InnerRegular.measure_eq_iSup

added theorem MeasureTheory.Measure.InnerRegular.of_pseudoEMetricSpace

added theorem MeasureTheory.Measure.InnerRegular.smul

added theorem MeasureTheory.Measure.InnerRegular.trans

added theorem MeasureTheory.Measure.InnerRegular.weaklyRegular_of_finite

added def MeasureTheory.Measure.InnerRegular

added theorem MeasureTheory.Measure.Regular.exists_compact_not_null

added theorem MeasureTheory.Measure.Regular.innerRegular_measurable

added theorem MeasureTheory.Measure.WeaklyRegular.innerRegular_measurable

added theorem MeasureTheory.Measure.WeaklyRegular.restrict_of_measurableSet

added theorem Set.exists_isOpen_le_add

added theorem Set.exists_isOpen_lt_add

added theorem Set.exists_isOpen_lt_of_lt

added theorem Set.measure_eq_iInf_isOpen