whiskerRight_comp_symm — Mathlib

English

A compatibility relation for whiskering on the right with respect to the associator: η whiskered by g and h equals the composite with associators and η whiskered on the composite g ≫ h.

Русский

Совместимость правого висения с ассоциатором: равенство двух способов висения ∙ η по g и h и через композицию g ≫ h.

LaTeX

$$$ η \\triangleright g \\triangleright h = (α_f g h)_{\\mathrm{hom}} \\circ (η \\triangleright (g \\gg h)) \\circ (α_{f'} g h)^{-1}$$$

Lean4

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

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