English
A open cover of a profinite space can be refined to a finite cover by pairwise disjoint nonempty clopen sets.
Русский
Покрытие открытое пространства профинитного типа можно сузить до конечного покрытия попарно непустыми клиноподпространствами.
LaTeX
$$$\exists n\exists (V: Fin n \to Clopens X),\; (\forall j, \exists i, V_j \subset U_i) \land univ \subseteq \bigcup_j V_j.$$$
Lean4
/-- Any open cover of a profinite space can be refined to a finite cover by pairwise disjoint
nonempty clopens. -/
theorem exists_finite_nonempty_disjoint_clopen_cover (hU : IsOpenCover U) :
∃ (n : ℕ) (W : Fin n → Clopens X),
(∀ j, W j ≠ ⊥ ∧ ∃ i, (W j : Set X) ⊆ U i) ∧ (univ : Set X) ⊆ ⋃ j, ↑(W j) ∧ Pairwise (Disjoint on W) :=
by
classical
obtain ⟨n, V, hVle, hVun⟩ := hU.exists_finite_clopen_cover
obtain ⟨W, hWle, hWun, hWd⟩ := Fintype.exists_disjointed_le V
simp only [← SetLike.coe_set_eq, Clopens.coe_finset_sup, Finset.mem_univ, iUnion_true] at hWun
let t : Finset (Fin n) := {j | W j ≠ ⊥}
refine ⟨#t, fun k ↦ W (t.equivFin.symm k), fun k ↦ ⟨?_, ?_⟩, fun x hx ↦ ?_, ?_⟩
· exact (Finset.mem_filter.mp (t.equivFin.symm k).2).2
·
exact
match hVle (t.equivFin.symm k) with
| ⟨i, hi⟩ => ⟨i, subset_trans (hWle _) hi⟩
· obtain ⟨j, hj⟩ := mem_iUnion.mp <| (hWun ▸ hVun) hx
have : W j ≠ ⊥ := by simpa [← SetLike.coe_ne_coe, ← Set.nonempty_iff_ne_empty] using ⟨x, hj⟩
exact mem_iUnion.mpr ⟨t.equivFin ⟨j, Finset.mem_filter.mpr ⟨Finset.mem_univ _, this⟩⟩, by simpa⟩
· exact hWd.comp_of_injective <| Subtype.val_injective.comp t.equivFin.symm.injective
