f'_i — Mathlib

English

Let S be a short complex equipped with left homology data h. Then the composition of the left-homology map f' with i recovers f, i.e., h.f' ∘ h.i = S.f.

Русский

Пусть S — короткий комплекс с данными левой гомологической структуры h. Тогда композиция отображений f' и i восстанавливает f, то есть h.f' ∘ h.i = S.f.

LaTeX

$$$ h.f' \\circ h.i = S.f $$$

Lean4

@[reassoc (attr := simp)]
theorem f'_i : h.f' ≫ h.i = S.f :=
  liftK_i _ _ _

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