sigmaCompactSpace — Mathlib

English

If X is a sigma-compact space and s ⊆ X is closed, then the subspace s (with the subspace topology) is sigma-compact.

Русский

Если X — σ-компактное пространство и s ⊆ X закрыто, то подпространство s (с топологией подпространства) является σ-компактным.

LaTeX

$$$$\exists (C_n)_{n\in\mathbb{N}},\forall n, C_n\subseteq X\text{ compact},\ s = \bigcup_{n\in\mathbb{N}} (C_n \cap s).$$$$

Lean4

theorem sigmaCompactSpace {s : Set X} (hs : IsClosed s) : SigmaCompactSpace s :=
  hs.isClosedEmbedding_subtypeVal.sigmaCompactSpace

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