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

@[simp]

theorem NominalSets.isSupported_iff_isSupportedF {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (f : X → Y) : IsSupported 𝔸 f ↔ IsSupportedF 𝔸 f

theorem NominalSets.isSupportedF_pi {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [PermAction 𝔸 X] [PermAction 𝔸 Y] [PermAction 𝔸 Z] {f : X → Y → Z} (hf : IsSupportedF 𝔸 fun (x : X × Y) => match x with | (x, y) => f x y) : IsSupportedF 𝔸 f

@[simp]

theorem NominalSets.isSupportedF_pi_iff {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [PermAction 𝔸 X] [PermAction 𝔸 Y] [PermAction 𝔸 Z] (f : X → Y → Z) : IsSupportedF 𝔸 f ↔ IsSupportedF 𝔸 fun (x : X × Y) => match x with | (x, y) => f x y

theorem NominalSets.isSupportOf_apply {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] {A : Finset 𝔸} {f : X → Y} {x : X} (hf : IsSupportOf A f) (hx : IsSupportOf A x) : IsSupportOf A (f x)

theorem NominalSets.supp_apply {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] [DecidableEq 𝔸] [Nominal 𝔸 X] [Nominal 𝔸 Y] (A : Finset 𝔸) (f : X → Y) (hf : IsSupportOf A f) (x : X) : supp 𝔸 (f x) \ supp 𝔸 x ⊆ A