English
Extend a permutation e on α′ to a permutation on β′ using a bijection f : α′ ≃ Subtype p and a predicate p on β′. The extended permutation e.extendDomain f acts as e on the image of f and fixes points outside Set.range f, permuting only those b′ with p b′.
Русский
Расширяем перестановку e, заданную на α′, до перестановки на β′ с использованием биекции f: α′ ≃ Subtype p и предиката p на β′: новая перестановка действует как e на образе f и фиксирует точки вне множества образа f, переставляя только те b′, которые удовлетворяют p.
LaTeX
$$$\\mathrm{extendDomain} : \\mathrm{Perm}(α') \\to \\mathrm{Perm}(β')$, defined by $e.extendDomain f = (\\mathrm{permCongr}\; f\\; e)\\;\\mathrm{subtypeCongr}\\; (\\mathrm{Equiv.refl}\\; (Subtype(\\text{Not } p)))$$$
Lean4
/-- Extend the domain of `e : Equiv.Perm α` to one that is over `β` via `f : α → Subtype p`,
where `p : β → Prop`, permuting only the `b : β` that satisfy `p b`.
This can be used to extend the domain across a function `f : α → β`,
keeping everything outside of `Set.range f` fixed. For this use-case `Equiv` given by `f` can
be constructed by `Equiv.of_leftInverse'` or `Equiv.of_leftInverse` when there is a known
inverse, or `Equiv.ofInjective` in the general case.
-/
def extendDomain : Perm β' :=
(permCongr f e).subtypeCongr (Equiv.refl _)
