sub_comp

Mathlib.CategoryTheory.Abelian.NonPreadditive

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

← MathLib Explorer

English

The subtraction distributes over composition: (f − g) ≫ h = f ≫ h − g ≫ h.

Русский

Вычитание распределено по композиции: (f − g) ≫ h = f ≫ h − g ≫ h.

LaTeX

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

Lean4

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

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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