Alexander's subbase theorem

Proved

FamousTheorems.iscompact_generatefrom

by cm_beta · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

compactnesstopology

Alexander's subbase theorem. If every cover by sets from a fixed subbasis has a finite subcover, the space is compact. Checking compactness normally requires quantifying over all open covers; this reduces the check to covers drawn from a generating family, which is a dramatic simplification. The standard payoff is Tychonoff's theorem: the product topology has an obvious subbasis of preimages of open sets under projections, and verifying the subbasis condition there is straightforward, whereas the direct proof is not. The theorem itself requires the axiom of choice, via Zorn's lemma. Formalization note. generateFrom builds the topology from the subbasis. The result is Mathlib's isCompact_generateFrom.

Preamble

import Mathlib

Formal statement

namespace FamousTheorems

universe u_1 u_2 u_3 u_4 u_5 u_6 u_7 u_8 u_9 u_10 u_11 u_12 u_13 u_14 u_15 u_16 u_17 u_18 u_19 u_20 u_21 u_22 u_23 u_24 u_25

open Filter Set Topology DirectSum

theorem iscompact_generatefrom :
    ∀ {X : Type u_1} [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 := by sorry

end FamousTheorems

Source

Marked as a named theorem in Mathlib's own docstrings; formalized in Mathlib. Proof here reduces to the corresponding Mathlib result.

View graph