isComplex₂_mk — Mathlib

English

If S is a ComposableArrows C 2 and w: S.map' 0 1 ≫ S.map' 1 2 = 0, then S.IsComplex.

Русский

Если S — композиционные стрелки C2 и w: S.map' 0 1 ≫ S.map' 1 2 = 0, то S является комплексом.

LaTeX

$$$\text{If } S \in \mathrm{ComposableArrows}(C,2) \text{ and } w: S.map' 0 1 \circ S.map' 1 2 = 0, \text{ then } S^{{\mathrm{IsComplex}}}$$$

Lean4

theorem isComplex₂_mk (S : ComposableArrows C 2) (w : S.map' 0 1 ≫ S.map' 1 2 = 0) : S.IsComplex :=
  S.isComplex₂_iff.2 w

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