instIsSplitMonoBiprodComparison'

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.instIsSplitMonoBiprodComparison'

English

The map biprodComparison' F X Y is split mono (i.e., has a right inverse).

Русский

Отображение biprodComparison' F X Y является разложимым моно.

LaTeX

$$$\\text{IsSplitMono}(\\text{biprodComparison}'(F,X,Y))$$$

Lean4

instance : IsSplitMono (biprodComparison' F X Y) :=
  IsSplitMono.mk' (splitMonoBiprodComparison' F X Y)

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

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

Разделы

Аффилиация

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