associator_inv_naturality_right — Mathlib

English

Dual right naturality: f ◁ g ◁ η and the inverses of associators satisfy an exchange with whiskering and η.

Русский

Двойной правой натурализм: взаимодeствие через η и ассоциатор через висение слева и справа.

LaTeX

$$$ f ◁ g ◁ η \\; ≫ (α_f g h')^{-1} = (α_f g h)^{-1} ≫ (f ≫ g) ◁ η $$$

Lean4

@[reassoc]
theorem associator_inv_naturality_right (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h') :
    f ◁ g ◁ η ≫ (α_ f g h').inv = (α_ f g h).inv ≫ (f ≫ g) ◁ η := by simp

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