isComplex₂_iff — Mathlib

English

For S in ComposableArrows C 2, S.IsComplex is equivalent to S.map' 0 1 ≫ S.map' 1 2 = 0.

Русский

Для S из ComposableArrows C 2 изоморфизм эквивалентен тому, что S.map' 0 1 ≫ S.map' 1 2 = 0.

LaTeX

$$$S \in \mathrm{ComposableArrows}(C,2) \Rightarrow (S \mathrm{IsComplex} \iff S.map' 0 1 \circ S.map' 1 2 = 0)$$$

Lean4

theorem isComplex₂_iff (S : ComposableArrows C 2) : S.IsComplex ↔ S.map' 0 1 ≫ S.map' 1 2 = 0 :=
  by
  constructor
  · intro h
    exact h.zero 0 (by cutsat)
  · intro h
    refine IsComplex.mk (fun i hi => ?_)
    obtain rfl : i = 0 := by cutsat
    exact h

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