English
If each X_i is a topological space and each X_i is UCompactlyGeneratedSpace, then the sigma-type Σ i, X_i is UCompactlyGeneratedSpace.
Русский
Если каждая X_i — топологическое пространство и каждая X_i — компактно-генерируемое, то сигма-тип Σ i, X_i компактно-генерируем.
LaTeX
$$$ (\forall i, \operatorname{TopologicalSpace}(X_i)) \land (\forall i, \operatorname{UCompactlyGeneratedSpace}(X_i)) \Rightarrow \operatorname{UCompactlyGeneratedSpace}(\Sigma i, X_i) $$$
Lean4
/-- A topological space `X` is compactly generated if a set `s` is closed when `f ⁻¹' s` is
closed for every continuous map `f : K → X`, where `K` is compact Hausdorff. -/
theorem uCompactlyGeneratedSpace_of_isClosed
(h : ∀ (s : Set X), (∀ (S : CompHaus.{u}) (f : C(S, X)), IsClosed (f ⁻¹' s)) → IsClosed s) :
UCompactlyGeneratedSpace.{u} X :=
uCompactlyGeneratedSpace_of_continuous_maps fun _ h' ↦
continuous_iff_isClosed.2 fun _ hs ↦ h _ fun S g ↦ hs.preimage (h' S g)
