composableArrows₅_exact — Mathlib

English

Exactness of the two-term sequence at i for the first short exact sequence S1.

Русский

Точность двухчленной последовательности на i для первого короткого точного ряда S1.

LaTeX

$$composableArrows₂_exact S₁ i$$

Lean4

theorem composableArrows₅_exact (i j : ι) (hij : c.Rel i j) : (composableArrows₅ hS₁ i j hij).Exact :=
  exact_of_δ₀ (hS₁.homology_exact₂ i).exact_toComposableArrows
    (exact_of_δ₀ (hS₁.homology_exact₃ i j hij).exact_toComposableArrows
      (exact_of_δ₀ (hS₁.homology_exact₁ i j hij).exact_toComposableArrows
        (hS₁.homology_exact₂ j).exact_toComposableArrows))

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