op — Mathlib · SciLib

English

If K is a complex and h: K.ExactAt i holds, then K.op.ExactAt i holds as well; i.e., exactness is preserved under taking opposite.

Русский

Если K — комплекс и K.ExactAt i, то и K^{op}.ExactAt i хранится; точность сохраняется при взятии противоположного комплекса.

LaTeX

$$$K^{op}.ExactAt(i) \\iff K.ExactAt(i)$$$

Lean4

theorem op {K : HomologicalComplex V c} {i : ι} (h : K.ExactAt i) : K.op.ExactAt i :=
  ShortComplex.Exact.op h

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