mathlib3

71c3e714 - refactor(topology/bases): use `structure` for `is_topological_basis (#6947)

refactor(topology/bases): use `structure` for `is_topological_basis (#6947) * turn `topological_space.is_topological_basis` into a `structure`; * rename `mem_nhds_of_is_topological_basis` to `is_topological_basis.mem_nhds_iff`; * rename `is_open_of_is_topological_basis` to `is_topological_basis.is_open`; * rename `mem_basis_subset_of_mem_open` to `is_topological_basis.exists_subset_of_mem_open`; * rename `sUnion_basis_of_is_open` to `is_topological_basis.open_eq_sUnion`, add prime version; * add `is_topological_basis.prod`; * add convenience lemma `is_topological_basis.second_countable_topology`; * rename `is_open_generated_countable_inter` to `exists_countable_basis`; * add `topological_space.countable_basis` and API around it; * add `@[simp]` to `opens.mem_supr`, add `opens.mem_Sup`; * golf