associator_hom_congr — Mathlib

English

Inverse associator is compatible with equalities: the inverse of the associator with f,g,h equals the transport of the inverse of the primed associator via eqToHom.

Русский

Обратный ассоциатор совместим с равенствами: обратный ассоциатор для f,g,h равен транспорту обратного ассоциатора для f',g',h' через eqToHom.

LaTeX

$$$(\\alpha_{f,g,h}^{-1}) = eqToHom(\\cdot) \\circ (\\alpha_{f',g',h'}^{-1}) \\circ eqToHom(\\cdot)$$$

Lean4

theorem associator_hom_congr {x y z t : B} {f f' : x ⟶ y} {g g' : y ⟶ z} {h h' : z ⟶ t} (ef : f = f') (eg : g = g')
    (eh : h = h') : (α_ f g h).hom = eqToHom (by grind) ≫ (α_ f' g' h').hom ≫ eqToHom (by grind) :=
  by
  subst_vars
  simp

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