mathlib3

3f868fab - feat(filter, topology): cluster_pt and principal notation, redefine compactness (#3160)

feat(filter, topology): cluster_pt and principal notation, redefine compactness (#3160) This PR implements what is discussed in https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Picking.20sides. It introduces a notation for `filter.principal`, defines `cluster_pt` and uses it to redefine compactness in a way which makes the library more consistent by always putting the neighborhood filter on the left, as in the description of closures and `nhds_within`.