English
In a compact space, for any assignment of neighborhoods U(x) of each x, there exists a finite subcollection whose interiors cover the whole space.
Русский
В компактном пространстве для произвольного присвоения окрестностей U(x) существует конечная подколлекция, чьи внутренности покрывают всё пространство.
LaTeX
$$$\\exists t : Finset\,X, \\bigcup_{x \\in t} \\operatorname{interior}(U(x)) = \\mathrm{univ}$$$
Lean4
theorem finite_cover_nhds_interior [CompactSpace X] {U : X → Set X} (hU : ∀ x, U x ∈ 𝓝 x) :
∃ t : Finset X, ⋃ x ∈ t, interior (U x) = univ :=
let ⟨t, ht⟩ :=
isCompact_univ.elim_finite_subcover (fun x => interior (U x)) (fun _ => isOpen_interior) fun x _ =>
mem_iUnion.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x)⟩
⟨t, univ_subset_iff.1 ht⟩
