Commit 2025-05-14 22:22 2aa8eec3
View on Github →feat(Topology/Subbasis): prove Alexander Subbasis Theorem (#24856)
Prove the Alexander Subbasis Theorem: if X has a topology T and T = generateFrom S, then X is compact if any open cover of X with elements in S has a finite subcover.