mathlib

697c8dd9 - refactor(topology/basic): use dot notation in `is_open.union` and friends (#7647)

refactor(topology/basic): use dot notation in `is_open.union` and friends (#7647) The fact that the union of two open sets is open is called `is_open_union`. We rename it to `is_open.union` to enable dot notation. Same with `is_open_inter`, `is_closed_union` and `is_closed_inter` and `is_clopen_union` and `is_clopen_inter` and `is_clopen_diff`.