instSymm — Mathlib

English

If E is an equivalence with CommShift, then E.symm is also CommShift; the CommShift structure transfers to the inverse equivalence.

Русский

Если E является эквивалентностью с CommShift, то E.symm также имеет CommShift; структура CommShift переходит к обратной эквивалентности.

LaTeX

$$$[E.CommShift A] \\Rightarrow E.symm.CommShift A$$$

Lean4

/-- If an equivalence `E : C ≌ D` is compatible with shifts, so is `E.symm`.
-/
instance [E.CommShift A] : E.symm.CommShift A :=
  mk' E.symm A (inferInstanceAs (NatTrans.CommShift E.counitIso.inv A))

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