Theorem IsClosed.measure_eq_univ_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 IsClosed.measure_eq_univ_iff_eqView on Github →