add_eq_left_addition — Mathlib

English

The equality f + g = biprod.lift f g ≫ biprod.desc (𝟙_Y) (𝟙_Y) expresses that addition can be realized via the universal properties of biproducts.

Русский

Равенство f + g = biprod.lift f g ≫ biprod.desc (𝟙_Y) (𝟙_Y) выражает, что сложение реализуется через универсальные свойства биопродуктов.

LaTeX

$$$f + g = \mathrm{biprod}.lift\, f\, g \;\circ\; \mathrm{biprod}.desc(\mathrm{Id}_Y, \mathrm{Id}_Y)$$$

Lean4

theorem add_eq_left_addition (f g : X ⟶ Y) : f + g = biprod.lift f g ≫ biprod.desc (𝟙 Y) (𝟙 Y) :=
  congr_fun₂ (EckmannHilton.mul (isUnital_leftAdd X Y) (isUnital_rightAdd X Y) (distrib X Y)).symm f g

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