viaEmbedding — Mathlib

English

The viaEmbedding construction extends a permutation on α to a permutation on β using an embedding α ↪ β by extending domain along the embedding.

Русский

Конструкция viaEmbedding расширяет перестановку на α до перестановки на β, используя вложение α ↪ β, за счет расширения области определения вдоль вложения.

LaTeX

$$$\text{viaEmbedding}(\iota,e) \in \operatorname{Perm}(\beta)\quad\text{is the extension of } e \text{ along } \iota$$$

Lean4

/-- Noncomputable version of `Equiv.Perm.viaFintypeEmbedding` that does not assume `Fintype` -/
noncomputable def viaEmbedding : Perm β :=
  extendDomain e (ofInjective ι.1 ι.2)

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