finite_cover_nhds — Mathlib

English

In a compact space X, for any family of neighborhoods U(x) of x, there exists a finite subfamily whose interiors cover X.

Русский

В компактном пространстве существует конечное подпокрытие интерьоров Neighborhood interiors.

LaTeX

$$$\\exists t : Finset\,X, \\bigcup_{x \\in t} \\operatorname{interior}(U(x)) = \\mathrm{univ}$$$

Lean4

theorem finite_cover_nhds [CompactSpace X] {U : X → Set X} (hU : ∀ x, U x ∈ 𝓝 x) :
    ∃ t : Finset X, ⋃ x ∈ t, U x = univ :=
  let ⟨t, ht⟩ := finite_cover_nhds_interior hU
  ⟨t, univ_subset_iff.1 <| ht.symm.subset.trans <| iUnion₂_mono fun _ _ => interior_subset⟩

Похожие утверждения