t0Space — Mathlib

English

For a complete separated uniform space X, the underlying topological space is T0.

Русский

Для полного разделимого равномерного пространства X соответствующее топологическое пространство является T0.

LaTeX

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

Lean4

instance t0Space (X : CpltSepUniformSpace) : T0Space (toUniformSpace X).carrier :=
  CpltSepUniformSpace.isT0 X

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