English
If X is compactly generated, then a map f: X → Y is continuous whenever f ∘ g is continuous for every continuous g from every compact Hausdorff space K into X.
Русский
Если X компактно-генерировано, то отображение f: X → Y непрерывно тогда и только тогда, когда композиция f ∘ g непрерывна для каждого непрерывного g: K → X, где K — компактное хаусдорфово пространство.
LaTeX
$$$[\\text{CompactlyGeneratedSpace}(X)] \\Rightarrow \\left( f: X \\to Y \\right) \\to \\left( \\forall K [\\text{TopologicalSpace } K][\\text{CompactSpace } K][\\text{T2Space } K] (g: K \\to X), \\text{Continuous } g \\Rightarrow \\text{Continuous } (f \\circ g) \\right) \\Rightarrow \\text{Continuous } f$$$
Lean4
/-- If `X` is compactly generated, to prove that `f : X → Y` is continuous it is enough to show
that for every compact Hausdorff space `K` and every continuous map `g : K → X`,
`f ∘ g` is continuous. -/
theorem continuous_from_compactlyGeneratedSpace [CompactlyGeneratedSpace X] (f : X → Y)
(h :
∀ (K : Type u) [TopologicalSpace K],
[CompactSpace K] → [T2Space K] → (∀ g : K → X, Continuous g → Continuous (f ∘ g))) :
Continuous f :=
continuous_from_uCompactlyGeneratedSpace f fun K ⟨g, hg⟩ ↦ h K g hg
