Theorems · Theorem · general topology

isCompact_iff_finite_subcover

∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s ↔ ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i

A set s is compact if and only if for every open cover of s, there exists a finite subcover.

Defined in

Mathlib.Topology.Compactness.Compact

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpace