ι_π_of_ne

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Pi.ι_π_of_ne

English

If b ≠ c, then Pi.ι f b ≫ Pi.π f c = 0 (zero morphism).

Русский

Если b ≠ c, то Pi.ι f b ≫ Pi.π f c = 0 (нулевой морфизм).

LaTeX

$$$\text{If } b \neq c,\quad Pi.ι f b \;\circ\; Pi.π f c = 0$$$

Lean4

@[reassoc]
theorem ι_π_of_ne {b c : β} (h : b ≠ c) : Pi.ι f b ≫ Pi.π f c = 0 := by simp [Pi.ι, Function.update_of_ne h.symm]

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

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

Разделы

Аффилиация

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