English
If X is compactly generated and every map f: X → Y is continuous whenever f ∘ g is continuous for all g from compact Hausdorff spaces, then X is compactly generated.
Русский
Если X компактно-генерировано и любой отображение f: X → Y непрерывно, когда f ∘ g непрерывно для всех g из компактных хаусдорфовых пространств, то X компактно-генерировано.
LaTeX
$$$\\forall X [\\text{TopologicalSpace } X], \\big( \\forall Y [\\text{TopologicalSpace } Y], (f: X \\to Y) \\,\\to\\, (\\forall K [\\text{TopologicalSpace } K], [\\text{CompactSpace } K] \\to [\\text{T2Space } K] \\to (\\forall g: K \\to X, \\text{Continuous } g \\to \\text{Continuous } (f \\circ g))) \\to \\text{Continuous } f \\big) \\Rightarrow \\text{CompactlyGeneratedSpace}(X)$$
Lean4
/-- Let `f : X → Y`. Suppose that to prove that `f` is continuous, it suffices to show that
for every compact Hausdorff space `K` and every continuous map `g : K → X`, `f ∘ g` is continuous.
Then `X` is compactly generated. -/
theorem compactlyGeneratedSpace_of_continuous_maps
(h :
∀ {Y : Type u} [TopologicalSpace Y] (f : X → Y),
(∀ (K : Type u) [TopologicalSpace K],
[CompactSpace K] → [T2Space K] → (∀ g : K → X, Continuous g → Continuous (f ∘ g))) →
Continuous f) :
CompactlyGeneratedSpace X :=
uCompactlyGeneratedSpace_of_continuous_maps fun f h' ↦ h f fun K _ _ _ g hg ↦ h' (CompHaus.of K) ⟨g, hg⟩
