Commit 2021-04-22 06:38 3fb9823d
View on Github →feat(topology/subset_properties): variant of elim_nhds_subcover for compact_space (#7304)
I put this in the compact_space namespace, although dot notation won't work so if preferred I can move it back to _root_.