inr_desc

Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

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

← MathLib Explorer

English

For X ⊞ Y, composing biprod.inr with biprod.desc f g yields g.

Русский

Для X ⊞ Y композиция biprod.inr с biprod.desc f g даёт g.

LaTeX

$$$ \biprod.inr \; \circ \biprod.desc f g = g $$$

Lean4

@[reassoc (attr := simp)]
theorem inr_desc {W X Y : C} [HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : biprod.inr ≫ biprod.desc f g = g :=
  (BinaryBiproduct.isColimit X Y).fac _ ⟨WalkingPair.right⟩

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

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

Разделы

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

Аффилиация

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