Theorem IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed

Modification history

2024-02-28 16:59

Mathlib/Topology/Compactness/Compact.lean

feat(Mathlib.Topology.Compactness.Compact): add sInter version of Cantor's intersection theorem (#10956) …

Added IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed View on Github →