exact_succ — Mathlib

English

The two-step complex built from d_n and d_{n+1} is exact.

Русский

Двухшаговый комплекс, построенный из d_n и d_{n+1}, является точным.

LaTeX

$$$$\\forall n, \\text{ShortComplex.mk}(\\dots).\\text{Exact}.$$$$

Lean4

theorem exact_succ (n : ℕ) : (ShortComplex.mk _ _ (I.cocomplex.d_comp_d n (n + 1) (n + 2))).Exact :=
  (HomologicalComplex.exactAt_iff' _ n (n + 1) (n + 2) (by simp) (by simp only [CochainComplex.next]; rfl)).1
    (I.cocomplex_exactAt_succ n)

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