isClosed — Mathlib

English

The sum (coproduct) of two compactly generated spaces is compactly generated.

Русский

Сумма двух компактно-генерируемых пространств сохраняет это свойство.

LaTeX

$$$ (\operatorname{UCompactlyGeneratedSpace}(X)) \land (\operatorname{UCompactlyGeneratedSpace}(Y)) \Rightarrow \operatorname{UCompactlyGeneratedSpace}(X \oplus Y) $$$

Lean4

/-- In a compactly generated space `X`, a set `s` is closed when `f ⁻¹' s` is
closed for every continuous map `f : K → X`, where `K` is compact Hausdorff. -/
theorem isClosed [UCompactlyGeneratedSpace.{u} X] {s : Set X}
    (hs : ∀ (S : CompHaus.{u}) (f : C(S, X)), IsClosed (f ⁻¹' s)) : IsClosed s :=
  by
  rw [eq_compactlyGenerated (X := X), TopologicalSpace.compactlyGenerated, isClosed_coinduced, isClosed_sigma_iff]
  exact fun ⟨S, f⟩ ↦ hs S f

Похожие утверждения