isCodetector_coseparator

Mathlib.CategoryTheory.Generator.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.isCodetector_coseparator

English

If C is Balanced and has a coseparator, then the coseparator C is a codetector.

Русский

Если C сбалансирована и имеет косепаратор, то косепаратор C является кодетектором.

LaTeX

$$$\mathrm{IsCodetector}(\operatorname{coseparator} C)$$$

Lean4

theorem isCodetector_coseparator [Balanced C] [HasCoseparator C] : IsCodetector (coseparator C) :=
  isCoseparator_coseparator C |>.isCodetector

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru