exact₁ — Mathlib

English

If S is a ComposableArrows C 2, and w expresses that the first two arrows compose to zero (S.map' 0 1 ≫ S.map' 1 2 = 0), and ShortComplex.mk with w is exact, then S is exact.

Русский

Если S — композиционные стрелки в C длины 2, выражение w говорит, что первая пара стрелок композируется в нуль, и ShortComplex.mk с w точен, тогда S точен.

LaTeX

$$$\text{If } S \in \mathrm{ComposableArrows}(C,2),\ w: S.map' 0 1 \;\; S.map' 1 2 = 0,\ h: (\mathrm{ShortComplex.mk} \; \_ \; \_ \; w) \text{ is exact} \Rightarrow S.\mathrm{Exact}$$$

Lean4

theorem exact₁ (S : ComposableArrows C 1) : S.Exact
    where
  toIsComplex := S.isComplex₁
  exact i hi := by exfalso; omega

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