completeSpace — Mathlib

English

The complete space structure on a completion of a complete space X, when transported to the underlying uniform space, is complete.

Русский

Полноту пространства с помощью дополнения сохраняется при переходе к базовому равномерному пространству.

LaTeX

$$$\forall X:\ CpltSepUniformSpace,\ CompleteSpace( toUniformSpace X ).carrier$$$

Lean4

instance completeSpace (X : CpltSepUniformSpace) : CompleteSpace (toUniformSpace X).carrier :=
  CpltSepUniformSpace.isCompleteSpace X

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