completion — Mathlib

English

If X has ultra-uniformity, then UniformSpace.Completion X also has ultra-uniformity.

Русский

Если у пространства X есть ультра-равномерность, то и его завершение имеет ультра-равномерность.

LaTeX

$$$IsUltraUniformity\big(UniformSpace.Completion X\big)$$$

Lean4

instance completion [IsUltraUniformity X] : IsUltraUniformity (UniformSpace.Completion X) :=
  completion_iff.2 inferInstance

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