sumCongr_trans — Mathlib

English

The transitivity of sumCongr inPerm context: (sumCongr e f).trans (sumCongr g h) equals sumCongr (e.trans g) (f.trans h).

Русский

Транзитивность sumCongr в контексте перестановок: (sumCongr e f).trans (sumCongr g h) = sumCongr (e.trans g) (f.trans h).

LaTeX

$$sumCongr_trans {α β} (e : Equiv.Perm α) (f : Equiv.Perm β) (g : Equiv.Perm α) (h : Equiv.Perm β) : (sumCongr e f).trans (sumCongr g h) = sumCongr (e.trans g) (f.trans h)$$

Lean4

theorem sumCongr_trans {α β} (e : Equiv.Perm α) (f : Equiv.Perm β) (g : Equiv.Perm α) (h : Equiv.Perm β) :
    (sumCongr e f).trans (sumCongr g h) = sumCongr (e.trans g) (f.trans h) :=
  Equiv.sumCongr_trans e f g h

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