isCompact_iff_isClosed_bounded — Mathlib

English

In a proper Hausdorff space, a set is compact iff it is closed and bounded.

Русский

В правильном Гаусдорфовом пространстве множество компактно тогда и только тогда, когда оно замкнуто и ограничено.

LaTeX

$$$IsCompact(s) \\iff (IsClosed(s) \\land IsBounded(s)).$$$

Lean4

/-- The **Heine–Borel theorem**:
In a proper Hausdorff space, a set is compact if and only if it is closed and bounded. -/
theorem isCompact_iff_isClosed_bounded [T2Space α] [ProperSpace α] : IsCompact s ↔ IsClosed s ∧ IsBounded s :=
  ⟨fun h => ⟨h.isClosed, h.isBounded⟩, fun h => isCompact_of_isClosed_isBounded h.1 h.2⟩

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