Theorems · Theorem · general topology

compactSpace_generateFrom

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

The CompactSpace version of Alexander's subbasis theorem. If X is a topological space with a subbasis S, then X is compact if for any open cover of X all of whose elements belong to S, there is a finite subcover.

Defined in

Mathlib.Topology.Compactness.Compact

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpace