Commit 2023-07-14 13:16 a1a257dd

View on Github →

feat: for an open-positive measure, an open/closed subset is almost empty/full iff it is actually empty/full (#5746) Also invert the import order so that MeasureTheory.Measure.OpenPos imports MeasureTheory.Constructions.BorelSpace.Basic rather than the other way around.

Estimated changes

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

deleted theorem Continuous.isOpenPosMeasure_map

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

Modified Mathlib/MeasureTheory/Measure/OpenPos.lean

added theorem Continuous.isOpenPosMeasure_map

added theorem IsClosed.ae_eq_univ_iff_eq

added theorem IsClosed.measure_eq_one_iff_eq_univ

added theorem IsClosed.measure_eq_univ_iff_eq

added theorem IsOpen.ae_eq_empty_iff_eq

added theorem IsOpen.measure_zero_iff_eq_empty