diag_comp — Mathlib

English

Let X and Y have a binary coproduct X ⨿ X. For a morphism f: X → Y, the codiagonal codiag X decomposes as coprod.desc f f, i.e., codiag X ≫ f = coprod.desc f f.

Русский

Пусть X имеет копродукцию X ⨿ X; при любом отображении f: X → Y верно, что codiag X ≫ f = coprod.desc f f.

LaTeX

$$$\forall X,Y\; [HasBinaryCoproduct X X]\; (f: X\to Y): codiag X \;≫\; f = coprod.desc f f.$$$

Lean4

theorem diag_comp {X Y : C} [HasBinaryCoproduct X X] (f : X ⟶ Y) : codiag X ≫ f = coprod.desc f f := by simp

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