op

Mathlib.Algebra.Homology.Opposite

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.Acyclic.op

English

K.Acyclic iff K.op.Acyclic; acyclicity is preserved under opposite.

Русский

Acyclicity сохраняется после взятия противоположного: K.Acyclic ⇔ K.op.Acyclic.

LaTeX

$$$K.Acyclic \\iff K^{op}.Acyclic$$$

Lean4

theorem op {K : HomologicalComplex V c} (h : K.Acyclic) : K.op.Acyclic := fun i ↦ (h i).op

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru