Theorem IsCompactSystem.iff_nonempty_iInter

Modification history

2026-03-10 12:16

Mathlib/Topology/Compactness/CompactSystem.lean

feat(Topology/Compactness/CompactSystem): introduce compact Systems (#36013) …

Added IsCompactSystem.iff_nonempty_iInter View on Github →