RenamingSets.Restrict

structure RenamingSets.Restrict (𝔸 : Type u_1) (X : Type u_2) [RenameAction 𝔸 X] :

For any RenameAction type X, we can form a RenamingSet Restrict 𝔸 X which is simply X restricted to those elements which have a finite support.

val : X
The underlying element.
isSupported_val : IsSupported 𝔸 ↑self
The element has a finite support.

Instances For

source

theorem RenamingSets.Restrict.ext {𝔸 : Type u_1} {X : Type u_2} {inst✝ : RenameAction 𝔸 X} {x y : Restrict 𝔸 X} (val : ↑x = ↑y) :

x = y

source

theorem RenamingSets.Restrict.ext_iff {𝔸 : Type u_1} {X : Type u_2} {inst✝ : RenameAction 𝔸 X} {x y : Restrict 𝔸 X} :

x = y ↔ ↑x = ↑y

source

instance RenamingSets.Restrict.instCoeOut {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] :

CoeOut (Restrict 𝔸 X) X

Equations

RenamingSets.Restrict.instCoeOut = { coe := RenamingSets.Restrict.val }

source

instance RenamingSets.Restrict.instRenameAction {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] :

RenameAction 𝔸 (Restrict 𝔸 X)

Equations

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

source

@[simp]

theorem RenamingSets.Restrict.rename_val {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] (σ : Ren 𝔸) (x : Restrict 𝔸 X) :

↑(rename σ x) = rename σ ↑x

source

@[simp]

theorem RenamingSets.Restrict.isSupportOf {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] (A : Finset 𝔸) (x : Restrict 𝔸 X) :

IsSupportOf A x ↔ IsSupportOf A ↑x

source

instance RenamingSets.Restrict.instRenamingSet {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] :

RenamingSet 𝔸 (Restrict 𝔸 X)

source

@[simp]

theorem RenamingSets.Restrict.isSupportedF_val {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] :

IsSupportedF 𝔸 val

source

@[simp]

theorem RenamingSets.Restrict.isSupportedF_iff {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] (f : X → Restrict 𝔸 Y) :

IsSupportedF 𝔸 f ↔ IsSupportedF 𝔸 fun (x : X) => ↑(f x)

source

theorem RenamingSets.Restrict.isSupportedF_mk {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] {f : X → Y} (hf : IsSupportedF 𝔸 f) (p : ∀ (x : X), IsSupported 𝔸 (f x)) :

IsSupportedF 𝔸 fun (x : X) => { val := f x, isSupported_val := ⋯ }