isCompact_closure — Mathlib

English

In a proper space, the closure of a bounded set is compact.

Русский

В правильном пространстве замыкание ограниченного множества компактно.

LaTeX

$$$IsCompact(closure(s))$ given $IsBounded(s)$.$$

Lean4

/-- The **Heine–Borel theorem**: In a proper space, the closure of a bounded set is compact. -/
theorem _root_.Bornology.IsBounded.isCompact_closure [ProperSpace α] (h : IsBounded s) : IsCompact (closure s) :=
  isCompact_of_isClosed_isBounded isClosed_closure h.closure

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