isSigmaCompact_iff_isSigmaCompact_univ

English

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

Русский

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

LaTeX

$$$IsSigmaCompact s \\leftrightarrow IsSigmaCompact (univ : Set s)$$$

Lean4

/-- A subset `s` is σ-compact iff `s` (with the subspace topology) is a σ-compact space. -/
theorem isSigmaCompact_iff_isSigmaCompact_univ {s : Set X} : IsSigmaCompact s ↔ IsSigmaCompact (univ : Set s) := by
  rw [Subtype.isSigmaCompact_iff, image_univ, Subtype.range_coe]

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