compactSpace_of_finite_subfamily_closed

English

If a family of closed sets has the finite intersection property in a space X, and certain finite-indexed subfamilies have empty intersection, then X is compact.

Русский

Если семейство замкнутых множеств обладает свойством конечной пересечения и некоторые конечные подпоследовательности имеют пустое пересечение, то пространство X компактно.

LaTeX

$$$(\forall t : ι → Set X), (\forall i, IsClosed (t i)) \rightarrow (⋂ i, t i) = ∅ \rightarrow ∃ u : Finset ι, (⋂ i ∈ u, t i) = ∅ \Rightarrow \text{CompactSpace } X$$$

Lean4

theorem compactSpace_of_finite_subfamily_closed
    (h : ∀ {ι : Type u} (t : ι → Set X), (∀ i, IsClosed (t i)) → ⋂ i, t i = ∅ → ∃ u : Finset ι, ⋂ i ∈ u, t i = ∅) :
    CompactSpace X where isCompact_univ := isCompact_of_finite_subfamily_closed fun t => by simpa using h t

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