isCoseparator

Mathlib.CategoryTheory.Generator.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsCodetector.isCoseparator

English

If G is balanced and has coequalizers, IsCodetector G implies IsCoseparator G.

Русский

Если G сбалансирован и есть коэквализаторы, IsCodetector G ⇒ IsCoseparator G.

LaTeX

$$$$\text{IsCodetector}(G) \Rightarrow \text{IsCoseparator}(G).$$$$

Lean4

theorem isCoseparator [HasCoequalizers C] {G : C} : IsCodetector G → IsCoseparator G :=
  IsCodetecting.isCoseparating

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

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

Разделы

Аффилиация

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