lift_lift_associator_inv — Mathlib

English

With the same setup as Lift Associator, the inverse of the associator gives lift f (lift g h) ≫ α_{Y,Z,W}.inv = lift (lift f g) h.

Русский

При той же конфигурации, что и Lift Associator, обратный ассоциатор даёт lift f (lift g h) ≫ α_{Y,Z,W}.inv = lift (lift f g) h.

LaTeX

$$$lift\; f\ (lift\ g\ h) \;\gg\; (\alpha_{Y,Z,W})^{-1} = lift\(lift\ f\ g)\ h$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_lift_associator_inv {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W) :
    lift f (lift g h) ≫ (α_ Y Z W).inv = lift (lift f g) h := by cat_disch

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