Commit 2024-02-28 16:59 0bbdc654

feat(Mathlib.Topology.Compactness.Compact): add sInter version of Cantor's intersection theorem (#10956) The iInter version of Cantor's intersection theorem is already present: IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed. The proof of the added sInter version takes advantage of the iInter version. Much of the addition due to conversation with Sebastien Gouezel on Zulip.