nonempty_sInter_of_directed_nonempty_isCompact_isClosed

English

Let S be a nonempty directed family of nonempty compact closed subsets of X. Then the intersection over all members of S is nonempty: ⋂U∈S U ≠ ∅.

Русский

Пусть S — непустая направленная по включению семья непустых компактно-замкнутых подмножеств X. Тогда пересечение всех её членов непусто: ⋂U∈S U ≠ ∅.

LaTeX

$$$\\\\bigcap_{U \\in S} U \\\\neq \\\\emptyset$$$

Lean4

/-- Cantor's intersection theorem for `sInter`:
the intersection of a directed family of nonempty compact closed sets is nonempty. -/
theorem nonempty_sInter_of_directed_nonempty_isCompact_isClosed {S : Set (Set X)} [hS : Nonempty S]
    (hSd : DirectedOn (· ⊇ ·) S) (hSn : ∀ U ∈ S, U.Nonempty) (hSc : ∀ U ∈ S, IsCompact U) (hScl : ∀ U ∈ S, IsClosed U) :
    (⋂₀ S).Nonempty := by
  rw [sInter_eq_iInter]
  exact
    IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ (DirectedOn.directed_val hSd)
      (fun i ↦ hSn i i.2) (fun i ↦ hSc i i.2) (fun i ↦ hScl i i.2)

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