map_snd — Mathlib

English

Let W × X and Y × Z be binary products. For f: W → Y and g: X → Z, we have (prod.map f g) ∘ prod.snd = prod.snd ∘ g.

Русский

Пусть W × X и Y × Z — бинарные произведения. Для f: W → Y и g: X → Z выполняется (prod.map f g) ∘ prod.snd = prod.snd ∘ g.

LaTeX

$$$prod.map \\ f \\ g \\circ prod.snd = prod.snd \\circ g$$$

Lean4

@[reassoc (attr := simp)]
theorem map_snd {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
    prod.map f g ≫ prod.snd = prod.snd ≫ g :=
  limMap_π _ _

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