Commit 2026-01-06 17:14 a12fb3df

View on Github →

feat(Topology): sandwich lemmas for profinite sets (#32660) We add two lemmas:

  • exists_clopen_of_closed_subset_open: in a totally disconnected compact Hausdorff space X, if Z ⊆ U are subsets with Z closed and U open, there exists a clopen C with Z ⊆ C ⊆ U.
  • exists_clopen_partition_of_clopen_cover: Let X be a totally disconnected compact Hausdorff space, D i ⊆ X a finite family of clopens, and Z i ⊆ D i closed. Assume that the Z i are pairwise disjoint. Then there exist clopens Z i ⊆ C i ⊆ D i with the C i disjoint, and such that ∪ D i ⊆ ∪ C i. These are required to prove injectivity of light profinite sets, see #31754

Estimated changes