English
If X is a UCompactlyGeneratedSpace, then f: X → Y is continuous provided that it is continuous when precomposed with every continuous map from a compact Hausdorff space.
Русский
Если X является UCompactlyGeneratedSpace, то отображение f: X → Y непрерывно, если оно непрерывно после предваренного композициями с любым непрерывным отображением из компактного хаусдорфова пространства.
LaTeX
$$$ [UCompactlyGeneratedSpace(X)] \Rightarrow \forall f:X \to Y,\ (\forall (S:CompHaus) (g:ContinuousMap S.toTop.carrier X), Continuous (f \circ g)) \Rightarrow \operatorname{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_uCompactlyGeneratedSpace [UCompactlyGeneratedSpace.{u} X] (f : X → Y)
(h : ∀ (S : CompHaus.{u}) (g : C(S, X)), Continuous (f ∘ g)) : Continuous f :=
by
apply continuous_le_dom UCompactlyGeneratedSpace.le_compactlyGenerated
exact continuous_from_compactlyGenerated f h
