Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_open.exists_lt_is_compact

Modification history

2021-05-26 21:50
src/measure_theory/regular.lean
feat(measure_theory/regular): more material on regular measures (#7680) …
Added is_open.exists_lt_is_compactView on Github →