mathlib

ba197e48 - feat(order/filter/*,topology/noetherian_space): add lemmas about `cofinite` (#16498)

feat(order/filter/*,topology/noetherian_space): add lemmas about `cofinite` (#16498) * A filter is disjoint with `cofinite` iff there exists a finite set that belongs to this filter. * An ultrafilter is either less than or equal to `cofinite`, or is equal to `pure a` for some `a`. * Any type with cofinite topology is a Noetherian (hence, is a compact) space.