inl_v_descShortComplex_f — Mathlib

English

For all integers i, j with j = i − 1, the v-component of inl f composed with the f-component of the descending map vanishes: (inl f).v i j h ≫ (descShortComplex S).f j = 0.

Русский

Для всех целых i, j с условием j = i − 1, диагональная компонента v в inl f после descShortComplex равна нулю: (inl f).v i j h ≫ (descShortComplex S).f j = 0.

LaTeX

$$$\forall i,j \in \mathbb{Z},\; i+(-1)=j \Rightarrow (inl(S.f)).v i j h \; ≫ \; (descShortComplex(S)).f j = 0$$$

Lean4

@[reassoc (attr := simp)]
theorem inl_v_descShortComplex_f (i j : ℤ) (h : i + (-1) = j) : (inl S.f).v i j h ≫ (descShortComplex S).f j = 0 := by
  simp [descShortComplex]

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