Commit 2021-04-01 01:24 71c3e714

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