comp_sub

Mathlib.CategoryTheory.Abelian.NonPreadditive

URI: https://scilib.ai/kg/mathlib#CategoryTheory.NonPreadditiveAbelian.comp_sub

English

For f: X ⟶ Y, g, h: Y ⟶ Z, f − g ≫ h = f ≫ h − g ≫ h.

Русский

Для f: X ⟶ Y, g,h: Y ⟶ Z имеем: (f − g) ≫ h = f ≫ h − g ≫ h.

LaTeX

$$$ (f - g) \!\!\!\!\!\! \!\!\!\! \!\!\! \!\!\! h = f h - g h $$$

Lean4

theorem comp_sub {X Y Z : C} (f : X ⟶ Y) (g h : Y ⟶ Z) : f ≫ (g - h) = f ≫ g - f ≫ h := by
  rw [sub_def, ← Category.assoc, prod.comp_lift, sub_def]

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

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

Разделы

Аффилиация

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