English
Extend the domain of a permutation e by an embedding f: α ↪ β to obtain a permutation of β, keeping outside of Set.range(f) fixed.
Русский
Расширяем область определения перестановки e с помощью вложения f: α ↪ β, получая перестановку β, вне области Range(f) остаётся фиксированной.
LaTeX
$$$\text{viaFintypeEmbedding} : \text{Equiv.Perm } \beta = e.extendDomain f.toEquivRange$$$
Lean4
/-- Extend the domain of `e : Equiv.Perm α`, mapping it through `f : α ↪ β`.
Everything outside of `Set.range f` is kept fixed. Has poor computational performance,
due to exhaustive searching in constructed inverse due to using `Function.Embedding.toEquivRange`.
When a better `α ≃ Set.range f` is known, use `Equiv.Perm.viaSetRange`.
When `[Fintype α]` is not available, a noncomputable version is available as
`Equiv.Perm.viaEmbedding`.
-/
def viaFintypeEmbedding : Equiv.Perm β :=
e.extendDomain f.toEquivRange
