ιMapObjOrZero_eq_zero

Mathlib.CategoryTheory.GradedObject

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GradedObject.ιMapObjOrZero_eq_zero

English

If p i ≠ j, then ιMapObjOrZero p i j is the zero morphism.

Русский

Если p i ≠ j, то ιMapObjOrZero p i j равен нулю.

LaTeX

$$$p(i) \\neq j \\Rightarrow X.\\\\mathrm{ιMapObjOrZero}\\; p\\; i\\; j = 0$$$

Lean4

theorem ιMapObjOrZero_eq_zero (h : p i ≠ j) : X.ιMapObjOrZero p i j = 0 :=
  dif_neg h

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

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

Разделы

Аффилиация

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