Theorem IsOpen.ae_eq_empty_iff_eq

Modification history

2023-07-14 13:16
Mathlib/MeasureTheory/Measure/OpenPos.lean
feat: for an open-positive measure, an open/closed subset is almost empty/full iff it is actually empty/full (#5746) …
Added IsOpen.ae_eq_empty_iff_eqView on Github →