isCodetector_codetector

Mathlib.CategoryTheory.Generator.Basic

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

English

If C has a codetector, then IsCodetector (codetector C).

Русский

Если C имеет кодетектор, то codetector C является кодетектором.

LaTeX

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

Lean4

theorem isCodetector_codetector [HasCodetector C] : IsCodetector (codetector C) :=
  HasCodetector.hasCodetector.choose_spec

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

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

Разделы

Аффилиация

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