mathlib

dc2a9659 - refactor(topology/bases): removing/adding the empty set from/to a basis (#17133)

refactor(topology/bases): removing/adding the empty set from/to a basis (#17133) + Add lemmas `is_topological_basis.insert/diff_empty` that allows adding the empty set to a basis and removing the empty set from a basis. + Remove `(⋂₀ f).nonempty` from `is_topological_basis_of_subbasis` and golf the proof. This condition is unnatural and was only used to exclude the empty set in [topological_space.second_countable_topology.to_separable_space](https://leanprover-community.github.io/mathlib_docs/topology/bases.html#topological_space.second_countable_topology.to_separable_space), because we want to choose a point from each set in the basis. As a result, the proof `exists_countable_basis` needs a slight modification.