Equiv.Perm.viaEmbedding, a noncomputable analogue of Equiv.Perm.viaFintypeEmbedding. #
noncomputable def
Equiv.Perm.viaEmbedding
{α : Type u_1}
{β : Type u_2}
(e : 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 (_ : Function.Injective ι.toFun))
theorem
Equiv.Perm.viaEmbedding_apply
{α : Type u_2}
{β : Type u_1}
(e : Equiv.Perm α)
(ι : α ↪ β)
(x : α)
:
↑(Equiv.Perm.viaEmbedding e ι) (↑ι x) = ↑ι (↑e x)
theorem
Equiv.Perm.viaEmbedding_apply_of_not_mem
{α : Type u_2}
{β : Type u_1}
(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 (_ : Function.Injective ι.toFun))
theorem
Equiv.Perm.viaEmbeddingHom_apply
{α : Type u_2}
{β : Type u_1}
(e : Equiv.Perm α)
(ι : α ↪ β)
:
↑(Equiv.Perm.viaEmbeddingHom ι) e = Equiv.Perm.viaEmbedding e ι