structure NominalSets.IsSupportOf {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (A : Finset 𝔸) (x : X) : Prop

A finite support of an element x is, intuitively, any superset of x's free variables.

• eq (π : Perm 𝔸) : (∀ a ∈ A, π a = a) → perm π x = x

  Any permutation which preserves the support acts as the identity.

def NominalSets.«termIsSupportOf[_]» : Lean.ParserDescr

A finite support of an element x is, intuitively, any superset of x's free variables.

Equations

• One or more equations did not get rendered due to their size.

inductive NominalSets.IsSupported (𝔸 : Type u_1) {X : Type u_2} [PermAction 𝔸 X] (x : X) : Prop

An element is supported if it has a support.

• intro {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] {x : X} (A : Finset 𝔸) : IsSupportOf A x → IsSupported 𝔸 x

  Introduces a proof of supported-ness.

def NominalSets.«termIsSupported[_]» : Lean.ParserDescr

An element is supported if it has a support.

Equations

• One or more equations did not get rendered due to their size.

inductive NominalSets.IsSupportedF (𝔸 : Type u_1) {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (f : X → Y) : Prop

Like IsSupported, specialized for functions.

• intro {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] {f : X → Y} (A : Finset 𝔸) : (∀ (π : Perm 𝔸), (∀ a ∈ A, π a = a) → ∀ (x : X), perm π (f x) = f (perm π x)) → IsSupportedF 𝔸 f

  Introduces a proof of supported-ness.

structure NominalSets.Equivariant (𝔸 : Type u_1) {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (f : X → Y) : Prop

An equivariant function preserves permutations.

• eq (π : Perm 𝔸) (x : X) : perm π (f x) = f (perm π x)

  f preserves permutations.

class NominalSets.Nominal (𝔸 : Type u_5) (X : Type u_6) [PermAction 𝔸 X] : Prop

Every element of a nominal type has a support.

• supported (x : X) : IsSupported 𝔸 x

  Every element has a support.

def NominalSets.«termNominal[_]» : Lean.ParserDescr

Every element of a nominal type has a support.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NominalSets.supp {X : Type u_2} (𝔸 : Type u_5) [PermAction 𝔸 X] [Nominal 𝔸 X] (x : X) : Finset 𝔸

Every finitely-supported element has a minimal support.

Equations

• NominalSets.supp 𝔸 x = ⋯.toFinset