Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-12 13:05 5ef85df4

View on Github →

feat(topology/basic): add is_closed.interior_union and is_closed.interior_union' (#16599) <del>closure_inter_open will be renamed to is_open.closure_inter in #16598</del> Already merged. Would it be better to add some lemmas like interior (s ∪ t) = interior (s ∪ interior t)?

Estimated changes