isCodetector

Mathlib.CategoryTheory.Generator.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsCoseparator.isCodetector

English

If G is balanced, IsCodetector G implies IsCoseparator G.

Русский

Если G сбалансирован, IsCodetector G ⇒ IsCoseparator G.

LaTeX

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

Lean4

theorem isCodetector [Balanced C] {G : C} : IsCoseparator G → IsCodetector G :=
  IsCoseparating.isCodetecting

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

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

Разделы

Аффилиация

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