commShift_of_inverse — Mathlib

English

If the inverse of E carries a CommShift A structure, then E itself carries a CommShift A structure.

Русский

Если биекция обратной эквивалентности E обладает структурой CommShift A, то и сама E обладает такой структурой.

LaTeX

$$$E\\,\\mathrm{CommShift}(A)$$$

Lean4

theorem commShift_of_inverse [E.inverse.CommShift A] :
    letI := E.commShiftFunctor A
    E.CommShift A :=
  by
  letI := E.commShiftFunctor A
  have := E.symm.commShift_of_functor A
  exact inferInstanceAs (E.symm.symm.CommShift A)

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