e_assoc — Mathlib

English

Associativity laws for enriched composition (two forms).

Русский

Законы ассоциативности для обогащенного умножения (два варианта).

LaTeX

$$$\text{e_assoc}$ and $\text{e_assoc'}$ express the two forms of associativity for enriched composition.$$

Lean4

@[reassoc (attr := simp)]
theorem e_assoc (W X Y Z : C) :
    (α_ _ _ _).inv ≫ eComp V W X Y ▷ _ ≫ eComp V W Y Z = _ ◁ eComp V X Y Z ≫ eComp V W X Z :=
  EnrichedCategory.assoc W X Y Z

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