isSigmaCompact_iff_sigmaCompactSpace

English

A subset s is σ-compact iff the subspace s is a σ-compact space.

Русский

Подмножество s σ-компактно тогда и только тогда, когда подпространство s является σ-компактным пространством.

LaTeX

$$$IsSigmaCompact s \\leftrightarrow SigmaCompactSpace s$$$

Lean4

theorem isSigmaCompact_iff_sigmaCompactSpace {s : Set X} : IsSigmaCompact s ↔ SigmaCompactSpace s :=
  isSigmaCompact_iff_isSigmaCompact_univ.trans isSigmaCompact_univ_iff

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