tensorLeftTensor_inv_app — Mathlib

English

The inverse of the left-associated tensor functor at an object Z is the inverse associator.

Русский

Обратный к лево-ассоциированному тензору на объекте Z равен обратному ассоциатору.

LaTeX

$$$ (\\text{tensorLeftTensor } X Y)^{-1} .\\; Z = (\\text{associator } X Y Z)^{-1}. $$$

Lean4

@[simp]
theorem tensorLeftTensor_inv_app (X Y Z : C) : (tensorLeftTensor X Y).inv.app Z = (associator X Y Z).inv := by
  simp [tensorLeftTensor]

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