leftUnitor_inv_whiskerRight — Mathlib

English

The inverse left unitor whiskered on the right is equal to the composition of the inverse left unitor on X ⊗ Y with the associator's inverse.

Русский

Обратный левый единичный элемент, взятый справа, равен композиции обратного левого унитора на X ⊗ Y с обратной ассоциаторной инверсией.

LaTeX

$$$(\\lambda_X)^{-1} \\;\\triangleright\\; Y = (\\lambda_{X \\otimes Y})^{-1} \\;\\circ\\; α_{X, \\mathbf{1}, Y}^{-1}$$$

Lean4

@[reassoc, simp]
theorem leftUnitor_inv_whiskerRight (X Y : C) : (λ_ X).inv ▷ Y = (λ_ (X ⊗ Y)).inv ≫ (α_ (𝟙_ C) X Y).inv :=
  eq_of_inv_eq_inv (by simp)

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