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.