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

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

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

Equations

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

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

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

noncomputable def Equiv.Perm.viaEmbeddingHom {α : Type u_1} {β : Type u_2} (ι : α ↪ β) : Equiv.Perm α →* Equiv.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 : Equiv.Perm α) (ι : α ↪ β) : (Equiv.Perm.viaEmbeddingHom ι) e = Equiv.Perm.viaEmbedding e ι

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