hom — Mathlib

English

Constructor for ComposableArrows C 5: given arrows f,g,h,i,j, define mk₅ f g h i j = (mk₄ g h i j).precomp f.

Русский

Конструктор mk₅ для ComposableArrows C 5: дано стрелы f,g,h,i,j, определяется mk₅ f g h i j = (mk₄ g h i j).precomp f.

LaTeX

$$$ \text{mk}_5 f\,g\,h\,i\,j = (\text{mk}_4\, g\, h\, i\, j).\text{precomp } f $$$

Lean4

/-- The canonical map `F.left ⟶ F.right` for `F : ComposableArrows C n`. -/
abbrev hom : F.left ⟶ F.right :=
  map' F 0 n

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