Theorems · Theorem · general topology

IsCompact.elim_directed_cover

∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v} [hι : Nonempty ι],
  IsCompact s →
    ∀ (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → Directed (fun x1 x2 => x1 ⊆ x2) U → ∃ i, s ⊆ U i

For every open directed cover of a compact set, there exists a single element of the cover which itself includes the set.

Defined in

Mathlib.Topology.Compactness.Compact

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNonempty