# Commit 2020-06-25 12:26 3f868fab

View on Github →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`

.