Theorems · Theorem · general topology

IsCompact.elim_finite_subcover_image

∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] {s : Set X} {b : Set ι} {c : ι → Set X},
  IsCompact s → (∀ i ∈ b, IsOpen (c i)) → s ⊆ ⋃ i ∈ b, c i → ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i

For every open cover of a compact set, there exists a finite subcover.

Defined in

Mathlib.Topology.Compactness.Compact

Cited by

8 results in Mathlib

Foundations

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

Assumes

TopologicalSpace