IsSupportOf

theorem NominalSets.isSupportOf_def {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (A : Finset 𝔸) (x : X) : IsSupportOf A x ↔ ∀ (π : Perm 𝔸), (∀ a ∈ A, π a = a) → perm π x = x

@[simp]

theorem NominalSets.isSupportOf_perm {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DecidableEq 𝔸] (A : Finset 𝔸) (π : Perm 𝔸) (x : X) : IsSupportOf A (perm π x) ↔ IsSupportOf (Finset.image (⇑π⁻¹) A) x

@[simp]

theorem NominalSets.isSupportOf_univ {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [Fintype 𝔸] (x : X) : IsSupportOf Finset.univ x

theorem NominalSets.isSupportOf_monotone {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (x : X) : Monotone fun (x_1 : Finset 𝔸) => IsSupportOf x_1 x

theorem NominalSets.isSupportOf_swap {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DecidableEq 𝔸] (A : Finset 𝔸) (x : X) : IsSupportOf A x ↔ ∀ {a b : 𝔸}, a ∉ A → b ∉ A → perm (Perm.swap a b) x = x

theorem NominalSets.isSupportOf_union_left {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DecidableEq 𝔸] {A B : Finset 𝔸} {x : X} (h : IsSupportOf A x) : IsSupportOf (A ∪ B) x

theorem NominalSets.isSupportOf_union_right {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DecidableEq 𝔸] {A B : Finset 𝔸} {x : X} (h : IsSupportOf B x) : IsSupportOf (A ∪ B) x

theorem NominalSets.isSupportOf_inter {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [PermAction 𝔸 X] [DecidableEq 𝔸] [Infinite 𝔸] {A B : Finset 𝔸} {x : X} (hA : IsSupportOf A x) (hB : IsSupportOf B x) : IsSupportOf (A ∩ B) x

@[simp]

theorem NominalSets.isSupportOf_discrete {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DiscretePermAction 𝔸 X] {A : Finset 𝔸} (x : X) : IsSupportOf A x

theorem NominalSets.isSupportOf_lift {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] {Y : Type u_6} (eq : X ≃ Y) (A : Finset 𝔸) (y : Y) : IsSupportOf A y ↔ IsSupportOf A (eq.symm y)

IsSupported

theorem NominalSets.isSupported_def {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (x : X) : IsSupported 𝔸 x ↔ ∃ (A : Finset 𝔸), IsSupportOf A x

@[simp]

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

@[simp]

theorem NominalSets.isSupported_discrete {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DiscretePermAction 𝔸 X] (x : X) : IsSupported 𝔸 x

theorem NominalSets.isSupported_lift {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] {Y : Type u_6} (eq : X ≃ Y) (y : Y) : IsSupported 𝔸 y ↔ IsSupported 𝔸 (eq.symm y)

IsSupportedF

theorem NominalSets.isSupportedF_def {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (f : X → Y) : IsSupportedF 𝔸 f ↔ ∃ (A : Finset 𝔸), ∀ (π : Perm 𝔸), (∀ a ∈ A, π a = a) → ∀ (x : X), perm π (f x) = f (perm π x)

@[simp]

theorem NominalSets.isSupportedF_id {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] : IsSupportedF 𝔸 id

@[simp]

theorem NominalSets.isSupportedF_id' {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] : IsSupportedF 𝔸 fun (x : X) => x

theorem NominalSets.isSupportedF_comp {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [PermAction 𝔸 X] [PermAction 𝔸 Y] [PermAction 𝔸 Z] {f : Y → Z} (hf : IsSupportedF 𝔸 f) {g : X → Y} (hg : IsSupportedF 𝔸 g) : IsSupportedF 𝔸 (f ∘ g)

theorem NominalSets.isSupportedF_comp' {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [PermAction 𝔸 X] [PermAction 𝔸 Y] [PermAction 𝔸 Z] {f : Y → Z} (hf : IsSupportedF 𝔸 f) {g : X → Y} (hg : IsSupportedF 𝔸 g) : IsSupportedF 𝔸 fun (x : X) => f (g x)

@[simp]

theorem NominalSets.isSupportedF_const {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] [Nominal 𝔸 Y] (y : Y) : IsSupportedF 𝔸 (Function.const X y)

@[simp]

theorem NominalSets.isSupportedF_const' {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] [Nominal 𝔸 Y] (y : Y) : IsSupportedF 𝔸 fun (x : X) => y

Equivariance

@[simp]

theorem NominalSets.isSupportOf_iff_equivariant {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (f : X → Y) : IsSupportOf ∅ f ↔ Equivariant 𝔸 f

@[simp]

theorem NominalSets.equivariant_id {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] : Equivariant 𝔸 id

@[simp]

theorem NominalSets.equivariant_id' {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] : Equivariant 𝔸 fun (x : X) => x

theorem NominalSets.equivariant_comp {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [PermAction 𝔸 X] [PermAction 𝔸 Y] [PermAction 𝔸 Z] {f : Y → Z} (hf : Equivariant 𝔸 f) {g : X → Y} (hg : Equivariant 𝔸 g) : Equivariant 𝔸 (f ∘ g)

theorem NominalSets.equivariant_comp' {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [PermAction 𝔸 X] [PermAction 𝔸 Y] [PermAction 𝔸 Z] {f : Y → Z} (hf : Equivariant 𝔸 f) {g : X → Y} (hg : Equivariant 𝔸 g) : Equivariant 𝔸 fun (x : X) => f (g x)

@[simp]

theorem NominalSets.equivariant_const {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] [DiscretePermAction 𝔸 Y] (y : Y) : Equivariant 𝔸 (Function.const X y)

@[simp]

theorem NominalSets.equivariant_const' {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] [DiscretePermAction 𝔸 Y] (y : Y) : Equivariant 𝔸 fun (x : X) => y

Nominal

instance NominalSets.PermAction.instNominal {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [Nominal 𝔸 X] (eq : X ≃ Y) : Nominal 𝔸 Y

instance NominalSets.PermAction.instNominal_1 {𝔸 : Type u_1} : Nominal 𝔸 𝔸

instance NominalSets.DiscretePermAction.instNominal {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DiscretePermAction 𝔸 X] : Nominal 𝔸 X

supp

theorem NominalSets.mem_supp {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [Nominal 𝔸 X] (a : 𝔸) (x : X) : a ∈ supp 𝔸 x ↔ ∀ (A : Finset 𝔸), IsSupportOf A x → a ∈ A

theorem NominalSets.mem_supp' {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DecidableEq 𝔸] [Nominal 𝔸 X] (a : 𝔸) (x : X) : a ∈ supp 𝔸 x ↔ {b : 𝔸 | perm (Perm.swap a b) x ≠ x}.Infinite

theorem NominalSets.supp_min {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [Nominal 𝔸 X] {A : Finset 𝔸} {x : X} (h : IsSupportOf A x) : supp 𝔸 x ⊆ A

@[simp]

theorem NominalSets.isSupportOf_supp {X : Type u_2} (𝔸 : Type u_6) [PermAction 𝔸 X] [Nominal 𝔸 X] [Infinite 𝔸] (x : X) : IsSupportOf (supp 𝔸 x) x