shift_shift — Mathlib

English

Shifting by b and then by a equals shifting by a + b; if a + b = c, then (P.shift b).shift a = P.shift c.

Русский

Сдвиг на b, затем на a, совпадает со сдвигом на a + b; если a + b = c, то (P.shift b).shift a = P.shift c.

LaTeX

$$$(P.shift b).shift a = P.shift (a + b)$$$

Lean4

theorem shift_shift (a b c : A) (h : a + b = c) [P.IsClosedUnderIsomorphisms] : (P.shift b).shift a = P.shift c :=
  by
  ext X
  exact P.prop_iff_of_iso ((shiftFunctorAdd' C a b c h).symm.app X)

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