toComposableArrows — Mathlib

English

For a short complex S, the associated pair of arrows f and g form a composable pair; this is encoded by the construction.

Русский

Для короткого комплекса S соответствующая пара стрел f и g образует компонуемую пару; это задаётся конструкцией.

LaTeX

$$$ toComposableArrows(S) = \text{ComposableArrows.mk}_2\ (S.f)\ (S.g) $$$

Lean4

/-- The composable arrows associated to a short complex. -/
@[simps!]
def toComposableArrows (S : ShortComplex C) : ComposableArrows C 2 :=
  ComposableArrows.mk₂ S.f S.g

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