English
The disjoint sum of two compactly generated spaces is compactly generated (reaffirmed).
Русский
Разделенная сумма двух компактно-генерируемых пространств снова компактно-генерируемое пространство.
LaTeX
$$$ (\operatorname{UCompactlyGeneratedSpace}(X)) \land (\operatorname{UCompactlyGeneratedSpace}(Y)) \Rightarrow \operatorname{UCompactlyGeneratedSpace}(X \oplus Y) $$$
Lean4
/-- The sum of two compactly generated spaces is compactly generated. -/
instance [UCompactlyGeneratedSpace.{u} X] [UCompactlyGeneratedSpace.{v} Y] :
UCompactlyGeneratedSpace.{max u v} (X ⊕ Y) :=
by
refine uCompactlyGeneratedSpace_of_isClosed fun s h ↦ isClosed_sum_iff.2 ⟨?_, ?_⟩
all_goals refine UCompactlyGeneratedSpace.isClosed fun S ⟨f, hf⟩ ↦ ?_
· let g : ULift.{v} S → X ⊕ Y := Sum.inl ∘ f ∘ ULift.down
have hg : Continuous g := continuous_inl.comp <| hf.comp continuous_uliftDown
exact (h (CompHaus.of (ULift.{v} S)) ⟨g, hg⟩).preimage continuous_uliftUp
· let g : ULift.{u} S → X ⊕ Y := Sum.inr ∘ f ∘ ULift.down
have hg : Continuous g := continuous_inr.comp <| hf.comp continuous_uliftDown
exact (h (CompHaus.of (ULift.{u} S)) ⟨g, hg⟩).preimage continuous_uliftUp
