associator_hom_fst — Mathlib

English

The associator morphism interacts with fst by a simple relation: (α_XYZ).hom ; fst ≈ fst ; fst.

Русский

Отображение ассоциатора взаимодействует с fst по простой связи: (α_{X,Y,Z})^hom ; fst = fst ; fst.

LaTeX

$$(α_X Y Z).hom ≫ fst _ _ = fst _ _ ≫ fst _ _$$

Lean4

@[reassoc (attr := simp)]
theorem associator_hom_fst (X Y Z : C) : (α_ X Y Z).hom ≫ fst _ _ = fst _ _ ≫ fst _ _ := by
  simp [fst_def, ← whiskerLeft_rightUnitor_assoc, -whiskerLeft_rightUnitor, ← whiskerLeft_comp_assoc]

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