English
Let X be a profinite space, i.e., totally disconnected, compact, and Hausdorff. Then every open cover U = {U_i} of X admits a finite refinement by clopen sets. More precisely, there exist n and clopen sets V_j (j = 1,...,n) such that for each j there is an i with V_j ⊆ U_i, and X is contained in the union of all V_j.
Русский
Пусть X — профинированное пространство (полное, компактное, Хаусдорфово), то есть совокупность открытых множеств U_i покрывает X. Тогда существует конечное вложение клиоп-покрытия: найдутся n и клип-помножества V_j (j = 1,...,n) такие, что для каждого j существует i с V_j ⊆ U_i, и X = ⋃_{j=1}^n V_j.
LaTeX
$$$\\exists n \\in \\mathbb{N},\\ \\exists V: \\mathrm{Fin}(n) \\to \\mathrm{Clopen}(X),\\ (\\forall j: \\mathrm{Fin}(n),\\ \\exists i,\\ V(j) \\subseteq U(i))\\ \\wedge\\ X \\subseteq \\bigcup_{j=0}^{n-1} V(j).$$$
Lean4
/-- Any open cover of a profinite space can be refined to a finite cover by clopens. -/
theorem exists_finite_clopen_cover (hU : IsOpenCover U) :
∃ (n : ℕ) (V : Fin n → Clopens X), (∀ j, ∃ i, (V j : Set X) ⊆ U i) ∧ univ ⊆ ⋃ j, (V j : Set X) := by
-- Choose an index `r x` for each point in `X` such that `∀ x, x ∈ U (r x)`.
choose r hr using hU.exists_mem
choose V hV hVx hVU using fun x ↦
compact_exists_isClopen_in_isOpen (U _).isOpen
(hr x)
-- Apply compactness to extract a finite subset of the `V`s which covers `X`.
obtain ⟨t, ht⟩ : ∃ t, univ ⊆ ⋃ i ∈ t, V i :=
isCompact_univ.elim_finite_subcover V (fun x ↦ (hV x).2)
(fun x _ ↦ mem_iUnion.mpr ⟨x, hVx x⟩)
-- Biject it noncanonically with `Fin n` for some `n`.
refine ⟨_, fun j ↦ ⟨_, hV (t.equivFin.symm j)⟩, fun j ↦ ⟨_, hVU _⟩, fun x hx ↦ ?_⟩
obtain ⟨m, hm, hm'⟩ := mem_iUnion₂.mp (ht hx)
exact Set.mem_iUnion_of_mem (t.equivFin ⟨m, hm⟩) (by simpa)
