assoc — Mathlib

English

The associativity constraint for composition in the SimplicialThickening context holds as usual.

Русский

Общепринятое свойство ассоциативности для композиции в контексте SimplicialThickening.

LaTeX

$$$$ (\alpha_{(\mathrm{Hom} i j),(\mathrm{Hom} j k),(\mathrm{Hom} k l)})^{-1} \circ (\mathrm{comp}_{i j k} \triangleright \mathrm{Hom}(k l)) \circ \mathrm{comp}_{i k l} = \mathrm{Hom} i j \triangleright \mathrm{comp}_{j k l} \circ \mathrm{comp}_{i j l} $$$$

Lean4

@[simp]
theorem assoc (i j k l : SimplicialThickening J) :
    (α_ (Hom i j) (Hom j k) (Hom k l)).inv ≫ comp i j k ▷ Hom k l ≫ comp i k l = Hom i j ◁ comp j k l ≫ comp i j l := by
  aesop

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