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