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

Equations

• NominalSets.List.instPermActionList = { perm := fun (π : NominalSets.Perm 𝔸) => List.map (NominalSets.perm π), perm_one := ⋯, perm_mul := ⋯ }

theorem NominalSets.List.perm_def {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (π : Perm 𝔸) (l : List X) : perm π l = List.map (perm π) l

@[simp]

theorem NominalSets.List.perm_nil {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (π : Perm 𝔸) : perm π [] = []

@[simp]

theorem NominalSets.List.perm_cons {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (π : Perm 𝔸) (x : X) (xs : List X) : perm π (x :: xs) = perm π x :: perm π xs

@[simp]

theorem NominalSets.List.perm_foldr {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (π : Perm 𝔸) (f : X → Y → Y) (z : Y) (xs : List X) : perm π (List.foldr f z xs) = List.foldr (perm π f) (perm π z) (perm π xs)

@[simp]

theorem NominalSets.List.getElem?_perm {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (π : Perm 𝔸) (xs : List X) (i : ℕ) : perm π xs[i]? = (perm π xs)[i]?

@[simp]

theorem NominalSets.List.perm_append {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (π : Perm 𝔸) (xs ys : List X) : perm π (xs ++ ys) = perm π xs ++ perm π ys

instance NominalSets.List.instDiscretePermActionList {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DiscretePermAction 𝔸 X] : DiscretePermAction 𝔸 (List X)

@[simp]

theorem NominalSets.List.isSupportOf_nil {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (A : Finset 𝔸) : IsSupportOf A []

@[simp]

theorem NominalSets.List.isSupportOf_cons {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (A : Finset 𝔸) (x : X) (xs : List X) : IsSupportOf A (x :: xs) ↔ IsSupportOf A x ∧ IsSupportOf A xs

@[simp]

theorem NominalSets.List.isSupported_nil {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] : IsSupported 𝔸 []

@[simp]

theorem NominalSets.List.isSupported_cons {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (x : X) (xs : List X) : IsSupported 𝔸 (x :: xs) ↔ IsSupported 𝔸 x ∧ IsSupported 𝔸 xs

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

@[simp]

theorem NominalSets.List.supp_nil {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [Nominal 𝔸 X] : supp 𝔸 [] = ∅

@[simp]

theorem NominalSets.List.supp_cons {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] [DecidableEq 𝔸] [Nominal 𝔸 X] (x : X) (xs : List X) : supp 𝔸 (x :: xs) = supp 𝔸 x ∪ supp 𝔸 xs

@[simp]

theorem NominalSets.List.isSupportedF_nil {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] : IsSupportedF 𝔸 fun (x : X) => []

@[simp]

theorem NominalSets.List.isSupportedF_cons {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] : IsSupportedF 𝔸 fun (x : X × List X) => match x with | (x, xs) => x :: xs

theorem NominalSets.List.isSupportedF_foldr {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [PermAction 𝔸 X] [PermAction 𝔸 Y] [PermAction 𝔸 Z] {f : X → Y → Z → Z} (hf : IsSupportedF 𝔸 fun (x : X × Y × Z) => match x with | (x, y, z) => f x y z) {g : X → Z} (hg : IsSupportedF 𝔸 g) {h : X → List Y} (hh : IsSupportedF 𝔸 h) : IsSupportedF 𝔸 fun (x : X) => List.foldr (f x) (g x) (h x)

@[simp]

theorem NominalSets.List.isSupportedF_getElem? {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] : IsSupportedF 𝔸 fun (x : List X × ℕ) => x.1[x.2]?

@[simp]

theorem NominalSets.List.isSupportedF_append {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] : IsSupportedF 𝔸 fun (x : List X × List X) => x.1 ++ x.2

theorem NominalSets.List.isSupportedF_map {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [PermAction 𝔸 X] [PermAction 𝔸 Y] [PermAction 𝔸 Z] {f : X → Y → Z} (hf : IsSupportedF 𝔸 fun (x : X × Y) => match x with | (x, y) => f x y) {g : X → List Y} (hg : IsSupportedF 𝔸 g) : IsSupportedF 𝔸 fun (x : X) => List.map (f x) (g x)