structure NominalSets.Restrict (𝔸 : Type u_1) (X : Type u_2) [PermAction 𝔸 X] : Type u_2

For any PermAction type X, we can form a Supported type 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.

theorem NominalSets.Restrict.ext_iff {𝔸 : Type u_1} {X : Type u_2} {inst✝ : PermAction 𝔸 X} {x y : Restrict 𝔸 X} : x = y ↔ ↑x = ↑y

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

instance NominalSets.Restrict.instCoeOut {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] : CoeOut (Restrict 𝔸 X) X

Equations

• NominalSets.Restrict.instCoeOut = { coe := NominalSets.Restrict.val }

instance NominalSets.Restrict.instCoeFunForall {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] : CoeFun (Restrict 𝔸 (X → Y)) fun (x : Restrict 𝔸 (X → Y)) => X → Y

Equations

• NominalSets.Restrict.instCoeFunForall = { coe := NominalSets.Restrict.val }

instance NominalSets.Restrict.instCoeFun {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [CoeFun X fun (x : X) => Y] : CoeFun (Restrict 𝔸 X) fun (x : Restrict 𝔸 X) => Y

Equations

• NominalSets.Restrict.instCoeFun = { coe := fun (x : NominalSets.Restrict 𝔸 X) => CoeFun.coe ↑x }

instance NominalSets.Restrict.instPermAction {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] : PermAction 𝔸 (Restrict 𝔸 X)

Equations

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

@[simp]

theorem NominalSets.Restrict.perm_val {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (π : Perm 𝔸) (x : Restrict 𝔸 X) : ↑(perm π x) = perm π ↑x

@[simp]

theorem NominalSets.Restrict.isSupportOf {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (A : Finset 𝔸) (x : Restrict 𝔸 X) : IsSupportOf A x ↔ IsSupportOf A ↑x

instance NominalSets.Restrict.instNominal {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] : Nominal 𝔸 (Restrict 𝔸 X)

@[simp]

theorem NominalSets.Restrict.isSupportedF_val {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] : IsSupportedF 𝔸 val

@[simp]

theorem NominalSets.Restrict.isSupportedF_val' {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (f : Restrict 𝔸 (X → Y)) : IsSupportedF 𝔸 ↑f

@[simp]

theorem NominalSets.Restrict.isSupportedF_iff {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (f : X → Restrict 𝔸 Y) : IsSupportedF 𝔸 f ↔ IsSupportedF 𝔸 fun (x : X) => ↑(f x)

theorem NominalSets.Restrict.isSupportedF_mk {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] {f : X → Y} (hf : IsSupportedF 𝔸 f) (p : ∀ (x : X), IsSupported 𝔸 (f x)) : IsSupportedF 𝔸 fun (x : X) => { val := f x, isSupported_val := ⋯ }

theorem NominalSets.Restrict.isSupportedF_eval {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [PermAction 𝔸 X] [PermAction 𝔸 Y] [PermAction 𝔸 Z] {f : X → Restrict 𝔸 (Y → Z)} (hf : IsSupportedF 𝔸 f) {g : X → Y} (hg : IsSupportedF 𝔸 g) : IsSupportedF 𝔸 fun (x : X) => ↑(f x) (g x)