Theorem IsOpen.measure_zero_iff_eq_empty

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.measure_zero_iff_eq_emptyView on Github →