mathlib

2a9d5695 - feat(topology/separation): add `disjoint_nhds_nhds` (#15635)

feat(topology/separation): add `disjoint_nhds_nhds` (#15635) Prove that a topological space is a Hausdorff space if and only iff the neighborhood filters of distinct points are disjoint. Use existing API about filters to golf some proofs.