lift_fst — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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