English
Alexander's subbasis theorem in the compact-space form: if T equals generateFrom(S) and a finite-subset condition holds for all P ⊆ S, then X is a compact space.
Русский
Теорема Александра о подбазе в виде компактного пространства: если T = generateFrom(S) и выполняется конечная подпоследовательность для всех P ⊆ S, то X компактно.
LaTeX
$$$T = \mathrm{generateFrom}(S) \land \Big( \forall P \subseteq S, \bigcup P = \mathrm{univ} \Rightarrow \exists Q \subseteq P, Q \text{Finite} \land \bigcup Q = \mathrm{univ} \Big) \Rightarrow \text{CompactSpace } X$$$
Lean4
/-- 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.
-/
theorem compactSpace_generateFrom [T : TopologicalSpace X] {S : Set (Set X)} (hTS : T = generateFrom S)
(h : ∀ P ⊆ S, ⋃₀ P = univ → ∃ Q ⊆ P, Q.Finite ∧ ⋃₀ Q = univ) : CompactSpace X :=
by
rw [← isCompact_univ_iff]
exact isCompact_generateFrom hTS <| by simpa
