mathlib3

5ef85df4 - feat(topology/basic): add `is_closed.interior_union` and `is_closed.interior_union'` (#16599)

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)`?