Commit 2025-12-22 22:40 e0b01525

refactor(Topology/Sequences): generalize seq-compactness lemmas to metrizable space (#30233)

• IsSeqCompact.isCompact
• UniformSpace.isCompact_iff_isSeqCompact
• UniformSpace.compactSpace_iff_seqCompactSpace These are lemmas on uniform spaces which has countable uniformity, so can be generalized to pseudo-metrizable space. From CLT