hcomp_eq_whiskerLeft_comp_whiskerRight

English

Equality between horizontal composition and whiskers: α ◫ β = whiskerLeft F β ≫ whiskerRight α K.

Русский

Равенство между горизонтальной композицией и отбрасываниями: α ◫ β = whiskerLeft F β ≫ whiskerRight α K.

LaTeX

$$$\\alpha \\;\\square\\; \\beta = \\mathrm{whiskerLeft}\\,F\\,\\beta \\;\\; ≫ \\; \\mathrm{whiskerRight}\\,\\alpha\\,K.$$$

Lean4

theorem hcomp_eq_whiskerLeft_comp_whiskerRight {F G : C ⥤ D} {H K : D ⥤ E} (α : F ⟶ G) (β : H ⟶ K) :
    α ◫ β = whiskerLeft F β ≫ whiskerRight α K := by
  ext
  simp

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