Theorem IsClosed.measure_eq_one_iff_eq_univ

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