instance NominalSets.Finset.instPermActionFinset {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DecidableEq X] : PermAction 𝔸 (Finset X)

Equations

• NominalSets.Finset.instPermActionFinset = { perm := fun (π : NominalSets.Perm 𝔸) (s : Finset X) => Finset.image (NominalSets.perm π) s, perm_one := ⋯, perm_mul := ⋯ }

theorem NominalSets.Finset.perm_def {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DecidableEq X] (π : Perm 𝔸) (s : Finset X) : perm π s = Finset.image (perm π) s

@[simp]

theorem NominalSets.Finset.mem_perm {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DecidableEq X] (x : X) (π : Perm 𝔸) (s : Finset X) : x ∈ perm π s ↔ perm π⁻¹ x ∈ s

@[simp]

theorem NominalSets.Finset.perm_empty {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DecidableEq X] (π : Perm 𝔸) : perm π ∅ = ∅

@[simp]

theorem NominalSets.Finset.perm_insert {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DecidableEq X] (π : Perm 𝔸) (x : X) (s : Finset X) : perm π (insert x s) = insert (perm π x) (perm π s)

instance NominalSets.Finset.instDiscretePermActionFinset {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DecidableEq X] [DiscretePermAction 𝔸 X] : DiscretePermAction 𝔸 (Finset X)

@[simp]

theorem NominalSets.Finset.isSupportOf_empty {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DecidableEq X] (A : Finset 𝔸) : IsSupportOf A ∅

@[simp]

theorem NominalSets.Finset.isSupported_empty {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DecidableEq X] : IsSupported 𝔸 ∅

instance NominalSets.Finset.instNominalFinset {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DecidableEq X] [Nominal 𝔸 X] : Nominal 𝔸 (Finset X)

@[simp]

theorem NominalSets.Finset.perm_supp {𝔸 : Type u_1} {X : Type u_3} [PermAction 𝔸 X] [DecidableEq 𝔸] [Nominal 𝔸 X] (π : Perm 𝔸) (x : X) : perm π (supp 𝔸 x) = supp 𝔸 (perm π x)