instCompleteSpace — Mathlib

English

If α is a complete uniform space, then its separation quotient SeparationQuotient(α) is complete.

Русский

Пусть α — полное равномерное пространство. Тогда сепараторное фактор-пространство SeparationQuotient(α) также полно.

LaTeX

$$$\text{If } \alpha \text{ is a complete uniform space, then } \operatorname{SeparationQuotient}(\alpha) \text{ is complete.}$$$

Lean4

instance instCompleteSpace [CompleteSpace α] : CompleteSpace (SeparationQuotient α) :=
  completeSpace_iff.2 ‹_›

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