class RenamingSets.RenameAction (𝔸 : Type u_1) (X : Type u_2) : Type (max u_1 u_2)

A type with a (nominal) renaming action is equipped with

• rename : Ren 𝔸 → X → X
  1. A renaming operation, such that
• rename_one (x : X) : rename 1 x = x
  2. applying the identity renaming is the identity, and
• rename_mul (f g : Ren 𝔸) (x : X) : rename f (rename g x) = rename (f * g) x
  3. composition of renamings is equal to renaming by the composition.

instance RenamingSets.RenameAction.instInhabited {𝔸 : Type u_1} {X : Type u_2} : Inhabited (RenameAction 𝔸 X)

Equations

• RenamingSets.RenameAction.instInhabited = { default := { rename := fun (x : RenamingSets.Ren 𝔸) (x_1 : X) => x_1, rename_one := ⋯, rename_mul := ⋯ } }

@[simp]

theorem RenamingSets.RenameAction.default_rename {𝔸 : Type u_1} {X : Type u_2} (x✝ : Ren 𝔸) (x : X) : rename x✝ x = x

instance RenamingSets.RenameAction.inst {𝔸 : Type u_1} : RenameAction 𝔸 𝔸

Equations

• RenamingSets.RenameAction.inst = { rename := fun (σ : RenamingSets.Ren 𝔸) => ⇑σ, rename_one := ⋯, rename_mul := ⋯ }

@[simp]

theorem RenamingSets.RenameAction.rename_def {𝔸 : Type u_1} (σ : Ren 𝔸) (a : 𝔸) : rename σ a = σ a

instance RenamingSets.Bool.instRenameActionBool {𝔸 : Type u_1} : RenameAction 𝔸 Bool

Equations

• RenamingSets.Bool.instRenameActionBool = default

instance RenamingSets.Empty.instRenameActionEmpty {𝔸 : Type u_1} : RenameAction 𝔸 Empty

Equations

• RenamingSets.Empty.instRenameActionEmpty = default

instance RenamingSets.PEmpty.instRenameActionPEmpty {𝔸 : Type u_1} : RenameAction 𝔸 PEmpty.{u_5 + 1}

Equations

• RenamingSets.PEmpty.instRenameActionPEmpty = default

instance RenamingSets.Unit.instRenameActionUnit {𝔸 : Type u_1} : RenameAction 𝔸 Unit

Equations

• RenamingSets.Unit.instRenameActionUnit = default

instance RenamingSets.PUnit.instRenameActionPUnit {𝔸 : Type u_1} : RenameAction 𝔸 PUnit.{u_5 + 1}

Equations

• RenamingSets.PUnit.instRenameActionPUnit = default

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

A type with a discrete renaming action has a renaming action such that:

• rename_discrete (σ : Ren 𝔸) (x : X) : rename σ x = x

  The renaming action does nothing.

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

A type with a discrete renaming action has a renaming action such that:

Equations

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