Theorem isCompactSystem_insert_univ_isCompact_isClosed

Modification history

2026-03-10 12:16
Mathlib/Topology/Compactness/CompactSystem.lean
feat(Topology/Compactness/CompactSystem): introduce compact Systems (#36013) …
Added isCompactSystem_insert_univ_isCompact_isClosedView on Github →