English
ExtendSubtype converts an equivalence between two subtypes into a permutation of the ambient finite set α.
Русский
ExtendSubtype преобразует эквивалентность между двумя подтипами в перестановку окружающего конечного множества α.
LaTeX
$$$\text{extendSubtype} : (\text{Subtype } p \simeq \text{Subtype } q) \to \text{Perm}(\alpha)$$$
Lean4
/-- If `e` is an equivalence between two subtypes of a fintype `α`, `e.extendSubtype`
is a permutation of `α` acting like `e` on the subtypes and doing something arbitrary outside.
Note that when `p = q`, `Equiv.Perm.subtypeCongr e (Equiv.refl _)` can be used instead. -/
noncomputable abbrev extendSubtype (e : { x // p x } ≃ { x // q x }) : Perm α :=
subtypeCongr e e.toCompl
