lift_snd — Mathlib

English

For a binary biproduct X ⊞ Y, the second component of biprod.lift f g is g.

Русский

Для би-произведения X ⊞ Y второй компонент biprod.lift f g равен g.

LaTeX

$$$ (\biprod.lift f g) \;\; \; \; \; \; \circ \; \biprod.snd = g $$$

Lean4

@[reassoc (attr := simp)]
theorem lift_snd {W X Y : C} [HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : biprod.lift f g ≫ biprod.snd = g :=
  (BinaryBiproduct.isLimit X Y).fac _ ⟨WalkingPair.right⟩

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