Commit 2022-07-26 11:31 2a9d5695

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.