inl_map — Mathlib

English

For a coproduct W ⨿ X and Y ⊿ Z with maps f: W → Y and g: X → Z, the map inl composed with map f g equals f composed with inl, i.e., coprod.inl ≫ coprod.map f g = f ≫ coprod.inl.

Русский

Пусть W ⨿ X и Y ⨿ Z — копроды; для f: W → Y и g: X → Z выполняется coprod.inl ≫ coprod.map f g = f ≫ coprod.inl.

LaTeX

$$$\forall W,X,Y,Z\; [HasBinaryCoproduct W X]\; [HasBinaryCoproduct Y Z]\; (f: W\to Y) (g: X\to Z),\; coprod.inl ≫ coprod.map f g = f ≫ coprod.inl.$$$

Lean4

@[reassoc (attr := simp)]
theorem inl_map {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
    coprod.inl ≫ coprod.map f g = f ≫ coprod.inl :=
  ι_colimMap _ _

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