mathlib

14749964 - feat(topology/basic): add `nhds_basis_closeds` (#14083)

feat(topology/basic): add `nhds_basis_closeds` (#14083) * add `nhds_basis_closeds`; * golf 2 proofs; * move `topological_space.seq_tendsto_iff` to `topology.basic`, rename it to `tendsto_at_top_nhds`.