exactAt_op_iff — Mathlib

English

The equivalence between exactAt for K and for K.op holds universally: K.op.ExactAt i iff K.ExactAt i.

Русский

Эквивалентность точности в i-й степени между K и K.op, то есть K.op.ExactAt i эквивалентно K.ExactAt i.

LaTeX

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

Lean4

@[simp]
theorem exactAt_op_iff (K : HomologicalComplex V c) {i : ι} : K.op.ExactAt i ↔ K.ExactAt i :=
  ⟨fun h ↦ h.unop, fun h ↦ h.op⟩

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