English
The sum of two compactly generated spaces is again compactly generated.
Русский
Сумма двух компактно-генерируемых пространств опять компактно-генерируемое пространство.
LaTeX
$$$ \forall X Y,\ [\operatorname{UCompactlyGeneratedSpace}(X)] \land [\operatorname{UCompactlyGeneratedSpace}(Y)] \Rightarrow \operatorname{UCompactlyGeneratedSpace}(X \oplus Y) $$$
Lean4
/-- In a compactly generated space `X`, a set `s` is open when `f ⁻¹' s` is
open for every continuous map `f : K → X`, where `K` is compact Hausdorff. -/
theorem isOpen [UCompactlyGeneratedSpace.{u} X] {s : Set X}
(hs : ∀ (S : CompHaus.{u}) (f : C(S, X)), IsOpen (f ⁻¹' s)) : IsOpen s :=
by
rw [eq_compactlyGenerated (X := X), TopologicalSpace.compactlyGenerated, isOpen_coinduced, isOpen_sigma_iff]
exact fun ⟨S, f⟩ ↦ hs S f
