noncomputable def NominalSets.Perm.supp {𝔸 : Type u_1} (π : Perm 𝔸) : Finset 𝔸

The support of a permutation is the set of atoms that are modified.

Equations

• π.supp = ⋯.toFinset

@[simp]

theorem NominalSets.Perm.mem_supp {𝔸 : Type u_1} (π : Perm 𝔸) (a : 𝔸) : a ∈ π.supp ↔ π a ≠ a

@[simp]

theorem NominalSets.Perm.isSupportOf_supp {𝔸 : Type u_1} (π : Perm 𝔸) : IsSupportOf π.supp π

instance NominalSets.Perm.instNominal {𝔸 : Type u_1} : Nominal 𝔸 (Perm 𝔸)

@[simp]

theorem NominalSets.Perm.supp_eq {𝔸 : Type u_1} [Infinite 𝔸] (π : Perm 𝔸) : NominalSets.supp 𝔸 π = π.supp