exact₂_mk — Mathlib

English

If S is a ComposableArrows C 2, w is an equality between the compositions into zero, and h is the exact ShortComplex.mk, then S.Exact.

Русский

Если S — композиционные стрелки C2, w — равенство нулю композиций, и h — точный ShortComplex.mk, то S точен.

LaTeX

$$$(S:\mathrm{ComposableArrows}(C,2)) \Rightarrow (w: \mathrm{Eq}(\mathrm{comp}(S.map' 0 1, S.map' 1 2)) 0) \rightarrow (h: (\mathrm{ShortComplex.mk} \; \_ \; \_ \; w).\mathrm{Exact}) \Rightarrow S.\mathrm{Exact}$$$

Lean4

theorem exact₂_mk (S : ComposableArrows C 2) (w : S.map' 0 1 ≫ S.map' 1 2 = 0) (h : (ShortComplex.mk _ _ w).Exact) :
    S.Exact :=
  (S.exact₂_iff (S.isComplex₂_mk w)).2 h

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