Equiv.Perm.viaEmbedding, a noncomputable analogue of Equiv.Perm.viaFintypeEmbedding.

noncomputable def Equiv.Perm.viaEmbedding {α : Type u_1} {β : Type u_2} (e : Perm α) (ι : α ↪ β) : Perm β

Noncomputable version of Equiv.Perm.viaFintypeEmbedding that does not assume Fintype

Equations

• e.viaEmbedding ι = e.extendDomain (Equiv.ofInjective ι.toFun ⋯)

theorem Equiv.Perm.viaEmbedding_apply {α : Type u_1} {β : Type u_2} (e : Perm α) (ι : α ↪ β) (x : α) : (e.viaEmbedding ι) (ι x) = ι (e x)

theorem Equiv.Perm.viaEmbedding_apply_of_notMem {α : Type u_1} {β : Type u_2} (e : Perm α) (ι : α ↪ β) (x : β) (hx : ¬x ∈ Set.range ⇑ι) : (e.viaEmbedding ι) x = x

noncomputable def Equiv.Perm.viaEmbeddingHom {α : Type u_1} {β : Type u_2} (ι : α ↪ β) : Perm α →* Perm β

viaEmbedding as a group homomorphism

Equations

• Equiv.Perm.viaEmbeddingHom ι = Equiv.Perm.extendDomainHom (Equiv.ofInjective ι.toFun ⋯)

theorem Equiv.Perm.viaEmbeddingHom_apply {α : Type u_1} {β : Type u_2} (e : Perm α) (ι : α ↪ β) : (viaEmbeddingHom ι) e = e.viaEmbedding ι

theorem Equiv.Perm.viaEmbeddingHom_injective {α : Type u_1} {β : Type u_2} (ι : α ↪ β) : Function.Injective ⇑(viaEmbeddingHom ι)