English
If the topology on Y is coinduced by a continuous map f from X, and X is compactly generated, then Y is compactly generated.
Русский
Если топология на Y является когруппированной (коиндуцированной) по непрерывному отображению f из X, и X компактно-генерируемо, то Y компактно-генерируемо.
LaTeX
$$$ [\operatorname{UCompactlyGeneratedSpace}(X)] \{f: X \to Y\} (hf: \operatorname{Continuous}(f)) (ht: t_Y = \operatorname{coinduced} f t_X) \Rightarrow \operatorname{UCompactlyGeneratedSpace}(Y) $$$
Lean4
/-- If the topology of `X` is coinduced by a continuous function whose domain is
compactly generated, then so is `X`. -/
theorem uCompactlyGeneratedSpace_of_coinduced [UCompactlyGeneratedSpace.{u} X] {f : X → Y} (hf : Continuous f)
(ht : tY = coinduced f tX) : UCompactlyGeneratedSpace.{u} Y :=
by
refine uCompactlyGeneratedSpace_of_isClosed fun s h ↦ ?_
rw [ht, isClosed_coinduced]
exact UCompactlyGeneratedSpace.isClosed fun _ ⟨g, hg⟩ ↦ h _ ⟨_, hf.comp hg⟩
