Theorem Continuous.isOpenPosMeasure_map

Modification history

2023-07-14 13:16
Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
feat: for an open-positive measure, an open/closed subset is almost empty/full iff it is actually empty/full (#5746) …
Modified Continuous.isOpenPosMeasure_mapView on Github →
2023-06-04 05:44
Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
style: recover `Is` of `Foo` which is ported from `is_foo` (#4639) …
Added Continuous.isOpenPosMeasure_mapView on Github →