hasLeftHomology_iff_op — Mathlib

English

A ShortComplex S has left homology if and only if its opposite has right homology.

Русский

Короткий комплекс S имеет левую гомологию тогда и только тогда, когда его противоположность имеет правую гомологию.

LaTeX

$$$ HasLeftHomology(S) \iff HasRightHomology(S^{op}) $$$

Lean4

theorem hasLeftHomology_iff_op (S : ShortComplex C) : S.HasLeftHomology ↔ S.op.HasRightHomology :=
  ⟨fun _ => inferInstance, fun _ => HasLeftHomology.mk' S.op.rightHomologyData.unop⟩

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