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
.