isSeparator_separator — Mathlib

English

If a category C has a separator, then the canonical separator object separator C is indeed a separator.

Русский

Если в категории C существует разделитель, то канонический объект separator C действительно является разделителем.

LaTeX

$$$[HasSeparator\\ C] \\Rightarrow \\mathrm{IsSeparator}(\\mathrm{separator}\\, C)$$$

Lean4

theorem isSeparator_separator [HasSeparator C] : IsSeparator (separator C) :=
  HasSeparator.hasSeparator.choose_spec

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