theorem NominalSets.perm_lift {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] {Y : Type u_5} (eq : X ≃ Y) (π : Perm 𝔸) (y : Y) : perm π y = eq (perm π (eq.symm y))

@[simp]

theorem NominalSets.perm_one' {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] : perm 1 = id

@[simp]

theorem NominalSets.perm_injective {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (π : Perm 𝔸) : Function.Injective (perm π)

@[simp]

theorem NominalSets.perm_inj {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (π : Perm 𝔸) (x y : X) : perm π x = perm π y ↔ x = y

instance NominalSets.PermAction.instDiscretePermAction {𝔸 : Type u_1} {X : Type u_2} : DiscretePermAction 𝔸 X

instance NominalSets.Function.instDiscretePermActionForall {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] [DiscretePermAction 𝔸 X] [DiscretePermAction 𝔸 Y] : DiscretePermAction 𝔸 (X → Y)