Commit 2026-03-10 12:16 237a3de1

feat(Topology/Compactness/CompactSystem): introduce compact Systems (#36013) A compact system is a set systems with the property that, whenever a countable intersections of sets in the set system is empty, there is a finite subset of sets with empty intersection. These are needed e.g. in measure theory if one wants to show sigma-additivity of a set function on a ring. Main result: The set of sets which are either compact and closed, or univ, is a compact system.