Disjoint covers of profinite spaces

We show that if X is a profinite space, then any open covering of X can be refined to a finite covering by disjoint nonempty clopens.

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

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

theorem TopologicalSpace.IsOpenCover.exists_finite_nonempty_disjoint_clopen_cover {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X] {U : ι → Opens X} (hU : IsOpenCover U) : ∃ (n : ℕ) (W : Fin n → Clopens X), (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), ↑(W j) ⊆ ↑(U i)) ∧ Set.univ ⊆ ⋃ (j : Fin n), ↑(W j) ∧ Pairwise (Function.onFun Disjoint W)

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