finite_nonempty_of_compact — Mathlib

English

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

Русский

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

LaTeX

$$$ \\{i \\mid (f(i)).Nonempty\\}.Finite $$$

Lean4

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

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