isClosed — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- In a compactly generated space `X`, a set `s` is closed when `s ∩ K` is
closed for every compact set `K`. -/
theorem isClosed [CompactlyGeneratedSpace X] {s : Set X} (hs : ∀ ⦃K⦄, IsCompact K → IsClosed (s ∩ K)) : IsClosed s :=
  by
  refine isClosed' fun K _ _ _ f hf ↦ ?_
  rw [← Set.preimage_inter_range]
  exact (hs (isCompact_range hf)).preimage hf

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