Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_open.exists_Union_is_closed

Modification history

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