mathlib

dc1ac244 - feat(topology/subset_properties): lemmas about `disjoint`, `nhds_set`, and `is_compact` (#16591)

feat(topology/subset_properties): lemmas about `disjoint`, `nhds_set`, and `is_compact` (#16591) The set neighborhoods filter of a compact set is disjoint with a filter `l` if and only if the neighborhoods filter of each point of this set is disjoint with `l`.