sumCongr — Mathlib

English

Combine two permutations ea : α ≃ α and eb : β ≃ β into a permutation on α ⊕ β; the result is the standard sumCongr on Perms.

Русский

Объединяем две перестановки ea: α ≃ α и eb: β ≃ β в перестановку на α ⊕ β; получаем стандартное sumCongr для перестановок.

LaTeX

$$sumCongr {α β} (ea : Equiv.Perm α) (eb : Equiv.Perm β) : Equiv.Perm (Sum α β)$$

Lean4

/-- Combine a permutation of `α` and of `β` into a permutation of `α ⊕ β`. -/
abbrev sumCongr {α β} (ea : Equiv.Perm α) (eb : Equiv.Perm β) : Equiv.Perm (α ⊕ β) :=
  Equiv.sumCongr ea eb

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