Commit 2026-03-27 17:46 a22c8fb5

feat(Topology/Compactness): add countably compact sets (#36174) This PR introduces the theory of countably compact sets and spaces. The motivation was the Eberlein–Šmulian theorem but of course this theory is of its own interest and there are many more applications. New definitions:

• IsCountablyCompact A: a set A is countably compact if every sequence in A has a cluster point in A.
• CountablyCompactSpace E: the whole space E is countably compact. Main results:
• IsCountablyCompact.elim_finite_subcover: finite subcover from any countable open cover.
• isCountablyCompact_iff_countable_open_cover: equivalence with the finite-subcover property.
• IsCompact.IsCountablyCompact: compact implies countably compact.
• IsSeqCompact.IsCountablyCompact: sequentially compact implies countably compact.
• IsCountablyCompact.isSeqCompact: countably compact implies sequentially compact in a first-countable space.
• isCountablyCompact_iff_infinite_subset_has_accPt: Bolzano–Weierstrass characterisation in a T₁ space.
• IsLindelof.isCompact: a countably compact Lindelöf set is compact.
• IsCountablyCompact.image: continuous images of countably compact sets are countably compact.
• Union stability: binary, Finset, Set.Finite, and iUnion variants.