English
If X is compactly generated and for every set s, whenever f^{-1}(s) is closed for all continuous f: K → X with K compact Hausdorff, then s is closed, then X is compactly generated.
Русский
Если X компактно-генерировано и для каждого множества s выполняется: если f^{-1}(s) замкнуто при всех непрерывных отображениях f: K → X (с K компактно-хаусдорфово), то s замкнуто, тогда X компактно-генерировано.
LaTeX
$$$[\\text{CompactlyGeneratedSpace}(X)] \\to \\left( \\forall s, \\Big( \\forall K [\\text{TopologicalSpace } K], [\\text{CompactSpace } K] \\to [\\text{T2Space } K] \\to (f: K \\to X), \\text{Continuous } f \\to \\text{IsClosed}(f^{-1}'s) \\Big) \\Rightarrow \\text{IsClosed}(s) \\right)$$$
Lean4
/-- A topological space `X` is compactly generated if a set `s` is closed when `f ⁻¹' s` is
closed for every continuous map `f : K → X`, where `K` is compact Hausdorff. -/
theorem compactlyGeneratedSpace_of_isClosed
(h :
∀ (s : Set X),
(∀ (K : Type u) [TopologicalSpace K],
[CompactSpace K] → [T2Space K] → ∀ (f : K → X), Continuous f → IsClosed (f ⁻¹' s)) →
IsClosed s) :
CompactlyGeneratedSpace X :=
uCompactlyGeneratedSpace_of_isClosed fun s h' ↦ h s fun K _ _ _ f hf ↦ h' (CompHaus.of K) ⟨f, hf⟩
