associator_hom_fst — Mathlib

English

The associator morphism's hom component composed with fst yields the same as fst composed with fst.

Русский

Гом-компонента ассоциатора, композиция с fst, даёт то же самое, что и fst с fst.

LaTeX

$$$(\alpha_{X Y Z})^{\mathrm{hom}} \circ \mathrm{prod.fst} = \mathrm{prod.fst} \circ \mathrm{prod.fst}$$$

Lean4

@[reassoc]
theorem associator_hom_fst (X Y Z : C) : (α_ X Y Z).hom ≫ prod.fst = prod.fst ≫ prod.fst := by simp [associator_hom]

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