isCompact_of_isComplete — Mathlib

English

Let s be a subset of α. If s is totally bounded and complete, then s is compact.

Русский

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

LaTeX

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

Lean4

theorem isCompact_of_isComplete {s : Set α} (ht : TotallyBounded s) (hc : IsComplete s) : IsCompact s :=
  isCompact_iff_totallyBounded_isComplete.mpr ⟨ht, hc⟩

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