associator_eqToHom_inv — Mathlib

English

Equality of equations yields equality of the associator's hom components: if e1,e2,e3 are equalities, the associatorhom components are equal after transporting by eqToHom.

Русский

Равенство равенств приводит к равенству компонент-ом ассоциатора: если e1,e2,e3 — равенства, их преобразование через eqToHom сохраняет равенство.

LaTeX

$$$(\\alpha_{e1,e2,e3}).hom = (eqToHom e1)^{-1} \\circ (eqToHom e3) \\circ ...$$$

Lean4

@[reassoc]
theorem associator_eqToHom_inv {x y z t : B} (e₁ : x = y) (e₂ : y = z) (e₃ : z = t) :
    (α_ (eqToHom e₁) (eqToHom e₂) (eqToHom e₃)).inv =
      eqToHom e₁ ◁ (eqToHomTransIso e₂ e₃).inv ≫
        (eqToHomTransIso e₁ (e₂.trans e₃)).inv ≫
          (eqToHomTransIso (e₁.trans e₂) e₃).hom ≫ (eqToHomTransIso e₁ e₂).hom ▷ eqToHom e₃ :=
  by
  subst_vars
  simp

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