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

A set A is a support of an element x if applying any two renamings behaves identically as long as the renamings agree on A.

Intuitively, A can be thought of as a superset of x's free variables.

• eq ⦃f g : Ren 𝔸⦄ : (∀ a ∈ A, f a = g a) → rename f x = rename g x

  Applying any two renamings behaves identically as long as the renamings agree on A.

structure RenamingSets.IsSupportOfF {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] (A : Finset 𝔸) (f : X → Y) : Prop

An alternative formulation of support for functions.

NOTE: IsSupportOfF is actually only equivalent to IsSupportOf when the function in question satisfies IsSupportedF.

• eq ⦃σ : Ren 𝔸⦄ : (∀ a ∈ A, σ a = a) → ∀ (x : X), rename σ (f x) = f (rename σ x)

  Any renaming which does not touch the support commutes with the function.

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

An element x : X is supported if it has a finite support.

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

  Applying any two renamings behaves identically as long as the renamings agree on A.

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

An alternative formulation of supportedness for functions.

NOTE: This is actually a stronger condition that IsSupported.

• intro {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] {f : X → Y} (A : Finset 𝔸) : IsSupportOfF A f → IsSupportedF 𝔸 f

  Any renaming which does not touch the support commutes with the function.

inductive RenamingSets.Equivariant (𝔸 : Type u_1) {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] (f : X → Y) : Prop

A function f : X → Y is equivariant if it preserves renamings.

• intro {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] {f : X → Y} : IsSupportOfF ∅ f → Equivariant 𝔸 f

  Renamings are preserved by f.

class RenamingSets.RenamingSet (𝔸 : Type u_5) (X : Type u_6) [RenameAction 𝔸 X] : Prop

A (nominal) renaming set is a type with a renaming action such that every element has a support.

• isSupported (x : X) : IsSupported 𝔸 x

  Every element has a support.

def RenamingSets.«termRenamingSet[_]» : Lean.ParserDescr

A (nominal) renaming set is a type with a renaming action such that every element has a support.

Equations

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

noncomputable def RenamingSets.supp {X : Type u_2} (𝔸 : Type u_5) [RenameAction 𝔸 X] [RenamingSet 𝔸 X] (x : X) : Finset 𝔸

Every renaming set has a minimal support, denoted by supp.

Equations

• RenamingSets.supp 𝔸 x = ⋯.toFinset