inr_map — Mathlib

English

Similarly, coprod.inr ≫ coprod.map f g = g ≫ coprod.inr for f: W → Y and g: X → Z in a binary coproduct setting.

Русский

Аналогично coprod.inr ≫ coprod.map f g = g ≫ coprod.inr.

LaTeX

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

Lean4

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

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