isDetector_separator — Mathlib

English

If C is a balanced category with a separator, then the separator C is a detector.

Русский

Пусть C — сбалансированная категория, обладающая разделителем. Тогда разделитель C является детектором.

LaTeX

$$$\mathrm{IsDetector}(\operatorname{separator} C)$$$

Lean4

theorem isDetector_separator [Balanced C] [HasSeparator C] : IsDetector (separator C) :=
  isSeparator_separator C |>.isDetector

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