Theorems · Theorem · general topology

IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed

∀ {X : Type u} [inst : TopologicalSpace X] {ι : Type v} [hι : Nonempty ι] (t : ι → Set X),
  Directed (fun x1 x2 => x1 ⊇ x2) t →
    (∀ (i : ι), (t i).Nonempty) → (∀ (i : ι), IsCompact (t i)) → (∀ (i : ι), IsClosed (t i)) → (⋂ i, t i).Nonempty

Cantor's intersection theorem for iInter: the intersection of a directed family of nonempty compact closed sets is nonempty.

Defined in

Mathlib.Topology.Compactness.Compact

Cited by

11 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceNonempty