shift_neg_shift' — Mathlib

English

A variant of shift_neg_shift' expressing the relation in a different choice of X, Y and f.

Русский

Вариант shift_neg_shift', выражающий отношение в другом выборе X, Y и f.

LaTeX

$$theorem shift_neg_shift' (i : A) : ...$$

Lean4

theorem shift_neg_shift' (i : A) :
    f⟦-i⟧'⟦i⟧' =
      (shiftFunctorCompIsoId C (-i) i (neg_add_cancel i)).hom.app X ≫
        f ≫ (shiftFunctorCompIsoId C (-i) i (neg_add_cancel i)).inv.app Y :=
  (NatIso.naturality_2 (shiftFunctorCompIsoId C (-i) i (neg_add_cancel i)) f).symm

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