isSigmaCompact_univ_iff — Mathlib

English

A topological space is σ-compact iff its universal subset is σ-compact.

Русский

Топологическое пространство σ-компактно тогда и только тогда, когда его универзум как подпространство σ-компактно.

LaTeX

$$$IsSigmaCompact (univ : Set X) \\leftrightarrow SigmaCompactSpace X$$$

Lean4

/-- A topological space is σ-compact iff `univ` is σ-compact. -/
theorem isSigmaCompact_univ_iff : IsSigmaCompact (univ : Set X) ↔ SigmaCompactSpace X :=
  ⟨fun h => ⟨h⟩, fun h => h.1⟩

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