isCompact_of_isClosed_isBounded — Mathlib

English

A closed and bounded set in a proper space is compact.

Русский

Замкнутое и ограниченное множество в корректном пространстве компактно.

LaTeX

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

Lean4

/-- The **Heine–Borel theorem**: In a proper space, a closed bounded set is compact. -/
theorem isCompact_of_isClosed_isBounded [ProperSpace α] (hc : IsClosed s) (hb : IsBounded s) : IsCompact s :=
  by
  rcases eq_empty_or_nonempty s with (rfl | ⟨x, -⟩)
  · exact isCompact_empty
  · rcases hb.subset_closedBall x with ⟨r, hr⟩
    exact (isCompact_closedBall x r).of_isClosed_subset hc hr

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