feat(topology/G_delta): add lemmas, minor golf (#9742)
* the complement to a countable set is a Gδ set;
* a closed set is a Gδ set;
* finite union of Gδ sets is a Gδ set;
* generalize some universe levels in `topology.basic`;
* golf a few proofs in `topology.uniform_space.basic`;
* add `filter.has_basis.bInter_bUnion_ball`.
