Theorems · Theorem · general topology

isCompact_generateFrom

∀ {X : Type u} [T : TopologicalSpace X] {S : Set (Set X)},
  T = TopologicalSpace.generateFrom S → ∀ {s : Set X}, (∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q) → IsCompact s

Alexander's subbasis theorem. Suppose X is a topological space with a subbasis S and s is a subset of X. Then s is compact if for any open cover of s with all elements taken from S, there is a finite subcover.

Defined in

Mathlib.Topology.Compactness.Compact

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpace