completeSpace — Mathlib

English

If α is complete, then NonemptyCompacts α is complete.

Русский

Если α полно, то NonemptyCompacts α полно.

LaTeX

$$$[\\text{CompleteSpace }\\alpha] \\Rightarrow \\text{CompleteSpace}(\\text{NonemptyCompacts }\\alpha).$$$

Lean4

/-- In a complete space, the type of nonempty compact subsets is complete. This follows
from the same statement for closed subsets -/
instance completeSpace [CompleteSpace α] : CompleteSpace (NonemptyCompacts α) :=
  (completeSpace_iff_isComplete_range isometry_toCloseds.isUniformInducing).2 <| isClosed_in_closeds.isComplete

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