Theorems · Definition · logic and foundations

Equiv.Perm.sumCongr

{α : Type u_9} → {β : Type u_10} → Equiv.Perm α → Equiv.Perm β → Equiv.Perm (α ⊕ β)

Combine a permutation of α and of β into a permutation of α ⊕ β.

Defined in

Mathlib.Logic.Equiv.Sum

Cited by

18 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Quot.sound