isClosed' — Mathlib

English

The sigma-type of a family of compactly generated spaces is compactly generated.

Русский

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

LaTeX

$$$\\text{CompactlyGeneratedSpace}(\\Sigma i, X_i)$$$

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' [CompactlyGeneratedSpace X] {s : Set X}
    (hs :
      ∀ (K : Type u) [TopologicalSpace K],
        [CompactSpace K] → [T2Space K] → ∀ (f : K → X), Continuous f → IsClosed (f ⁻¹' s)) :
    IsClosed s :=
  UCompactlyGeneratedSpace.isClosed fun S ⟨f, hf⟩ ↦ hs S f hf

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