hasImage_zero

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.hasImage_zero

English

There is an image factorisation for the zero morphism 0: X → Y.

Русский

Существование факторизации образа для нулевого морфизма 0: X → Y.

LaTeX

$$$HasImage(0:X\to Y)$$$

Lean4

instance hasImage_zero {X Y : C} : HasImage (0 : X ⟶ Y) :=
  HasImage.mk <| imageFactorisationZero _ _

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

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

Разделы

Аффилиация

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