isCompact_of_isClosed — Mathlib

English

If s is totally bounded and closed in a complete space α, then s is compact.

Русский

Если подмножество s является полностью ограниченным и замкнутым в полном пространстве α, то оно компактно.

LaTeX

$$$TotallyBounded(s) \land IsClosed(s) \Rightarrow IsCompact(s)$$$

Lean4

theorem isCompact_of_isClosed [CompleteSpace α] {s : Set α} (ht : TotallyBounded s) (hc : IsClosed s) : IsCompact s :=
  ht.isCompact_of_isComplete hc.isComplete

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