instance NominalSets.Set.instPermActionSet {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] : PermAction 𝔸 (Set X)

Equations

• NominalSets.Set.instPermActionSet = { perm := fun (π : NominalSets.Perm 𝔸) (s : Set X) => NominalSets.perm π '' s, perm_one := ⋯, perm_mul := ⋯ }

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

@[simp]

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

@[simp]

theorem NominalSets.Set.perm_union {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (π : Perm 𝔸) (s t : Set X) : perm π (s ∪ t) = perm π s ∪ perm π t

@[simp]

theorem NominalSets.Set.perm_inter {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (π : Perm 𝔸) (s t : Set X) : perm π (s ∩ t) = perm π s ∩ perm π t

@[simp]

theorem NominalSets.Set.perm_compl {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (π : Perm 𝔸) (s : Set X) : perm π sᶜ = (perm π s)ᶜ

theorem NominalSets.Set.finite {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (π : Perm 𝔸) {s : Set X} (hs : s.Finite) : (perm π s).Finite

instance NominalSets.Set.instDiscretePermActionSet {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DiscretePermAction 𝔸 X] : DiscretePermAction 𝔸 (Set X)