Theorems · Theorem · general topology

TopologicalSpace.IsOpenCover.exists_finite_clopen_cover

∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X]
  {U : ι → TopologicalSpace.Opens X},
  TopologicalSpace.IsOpenCover U → ∃ n V, (∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)) ∧ Set.univ ⊆ ⋃ j, ↑(V j)

Any open cover of a profinite space can be refined to a finite cover by clopens.

Defined in

Mathlib.Topology.Separation.DisjointCover

Cited by

1 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTotallyDisconnectedSpaceT2SpaceCompactSpace