isCoseparator_coseparator

Mathlib.CategoryTheory.Generator.Basic

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

English

If C has a coseparator, then coseparator C is a coseparator.

Русский

Пусть C имеет косепаратор; тогда косепаратор C является косепаратором.

LaTeX

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

Lean4

theorem isCoseparator_coseparator [HasCoseparator C] : IsCoseparator (coseparator C) :=
  HasCoseparator.hasCoseparator.choose_spec

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

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

Разделы

Аффилиация

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