Commit 2024-02-13 21:51 728e4391

feat(Topology/Order): add nhds_mkOfNhds_of_hasBasis (#10408)

• add TopologicalSpace.nhds_mkOfNhds_of_hasBasis
• add Trans instance for Filter.mem_of_superset
• change assumptions of TopologicalSpace.nhds_mkOfNhds, golf
  • the new assumption is equivalent to the old one with t ⊆ s removed
  • but is formulated in terms of Filter.Eventually