English
If the topology on X is coinduced by a continuous map f: X → Y and X is compactly generated, then Y is compactly generated.
Русский
Если топология X когенерирована непрерывным отображением f: X → Y и X компактно-генерируемо, то Y тоже компактно-генерируемо.
LaTeX
$$$\\text{CompactlyGeneratedSpace}(X) \\Rightarrow \\big( f: X \\to Y, \\text{Continuous } f \\land (t_Y = \\text{coinduced } f t_X) \\Rightarrow \\text{CompactlyGeneratedSpace}(Y) \\big)$$$
Lean4
/-- If the topology of `X` is coinduced by a continuous function whose domain is
compactly generated, then so is `X`. -/
theorem compactlyGeneratedSpace_of_coinduced {X : Type u} [tX : TopologicalSpace X] {Y : Type u}
[tY : TopologicalSpace Y] [CompactlyGeneratedSpace X] {f : X → Y} (hf : Continuous f) (ht : tY = coinduced f tX) :
CompactlyGeneratedSpace Y :=
uCompactlyGeneratedSpace_of_coinduced hf ht
