exact_toComposableArrows — Mathlib

English

If S is a ShortComplex C and S.Exact holds, then S.toComposableArrows.Exact holds as well.

Русский

Если S — краткий комплекс и S.Exact, то S.toComposableArrows.Exact тоже выполняется.

LaTeX

$$$\text{If } S \text{ is a ShortComplex with } S.Exact, \text{ then } S^{\mathrm{to\,comp}} \text{ is exact.}$$$

Lean4

theorem _root_.CategoryTheory.ShortComplex.Exact.exact_toComposableArrows {S : ShortComplex C} (hS : S.Exact) :
    S.toComposableArrows.Exact :=
  exact₂_mk _ _ hS

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