finite_of_compact — Mathlib

English

In a compact space, a locally finite family of nonempty sets can only have finitely many nonempty members.

Русский

В компактном пространстве локально конечная семейство непустых множеств состоит из конечного числа непустых членов.

LaTeX

$$$ (univ : Set ι).Finite $$$

Lean4

/-- If `X` is a compact space, then a locally finite family of nonempty sets of `X` can have only
finitely many elements, `Set.Finite` version. -/
theorem finite_of_compact [CompactSpace X] {f : ι → Set X} (hf : LocallyFinite f) (hne : ∀ i, (f i).Nonempty) :
    (univ : Set ι).Finite := by simpa only [hne] using hf.finite_nonempty_of_compact

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