English
Alexander's subbasis theorem: If 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 using elements of S there is a finite subcover.
Русский
Теорема подбазы Алекандра: пусть X — топологическое пространство с подбазой S, и s ⊆ X. Тогда s kompakt, если для любого открытого покрытия s элементами из S существует конечная подп covering.
LaTeX
$$$T = \\operatorname{generateFrom} S \\Rightarrow \\forall s,\\left(\\forall P \\subseteq S,\\ s \\subseteq \\bigcup P \\Rightarrow \\exists Q \\subseteq P,\\ Q \\text{ finite} \\land s \\subseteq \\bigcup Q\\right) \\Rightarrow \\operatorname{IsCompact}(s)$$$
Lean4
/-- **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.
-/
theorem isCompact_generateFrom [T : TopologicalSpace X] {S : Set (Set X)} (hTS : T = generateFrom S) {s : Set X}
(h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q) : IsCompact s :=
by
rw [isCompact_iff_ultrafilter_le_nhds', hTS]
intro F hsF
by_contra hF
have hSF : ∀ x ∈ s, ∃ t, x ∈ t ∧ t ∈ S ∧ t ∉ F := by simpa [nhds_generateFrom] using hF
choose! U hxU hSU hUF using hSF
obtain ⟨Q, hQU, hQ, hsQ⟩ :=
h (U '' s) (by simpa [Set.subset_def]) (fun x hx ↦ Set.mem_sUnion_of_mem (hxU _ hx) (by aesop))
have : ∀ s ∈ Q, s ∉ F := fun s hsQ ↦ (hQU hsQ).choose_spec.2 ▸ hUF _ (hQU hsQ).choose_spec.1
have hQF : ⋂₀ (compl '' Q) ∈ F.sets := by simpa [Filter.biInter_mem hQ, F.compl_mem_iff_notMem]
have : ⋃₀ Q ∉ F := by simpa [-Set.sInter_image, ← Set.compl_sUnion, hsQ, F.compl_mem_iff_notMem] using hQF
exact this (F.mem_of_superset hsF hsQ)
