exact_C₁_up — Mathlib

English

The upper part of the first column is exact (repeat statement for snake input).

Русский

Верхняя часть первой колонки точна (повтор утверждения для входа змейки).

LaTeX

$$$\text{Exact}(\text{UpperFirstColumn})$$$

Lean4

/-- The upper part of the first column of the snake diagram is exact. -/
theorem exact_C₁_up : (ShortComplex.mk S.v₀₁.τ₁ S.v₁₂.τ₁ (by rw [← comp_τ₁, S.w₀₂, zero_τ₁])).Exact :=
  exact_of_f_is_kernel _ S.h₀τ₁

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