t0Space — Mathlib

English

Let α be a uniform space. Then the completion of α, denoted Completion α, is a T0-space.

Русский

Пусть α — пространство с равномерной структурой. Его дополнение Completion α является T0-пространством.

LaTeX

$$$\\forall \\alpha\\; [\\text{UniformSpace }\\alpha]\\; T_0(\\mathrm{Completion}(\\alpha))$$$

Lean4

instance t0Space : T0Space (Completion α) :=
  SeparationQuotient.instT0Space

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