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

Equations

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

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

@[simp]

theorem NominalSets.Rose.perm_mk {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (π : Perm 𝔸) (x : X) (xs : List (Rose X)) : perm π { label := x, children := xs } = { label := perm π x, children := perm π xs }

@[simp]

theorem NominalSets.Rose.perm_fold {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (π : Perm 𝔸) (f : X → List Y → Y) (t : Rose X) : perm π (Rose.fold f t) = Rose.fold (perm π f) (perm π t)

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

@[simp]

theorem NominalSets.Rose.isSupportOf_mk {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (A : Finset 𝔸) (x : X) (xs : List (Rose X)) : IsSupportOf A { label := x, children := xs } ↔ IsSupportOf A x ∧ IsSupportOf A xs

@[simp]

theorem NominalSets.Rose.isSupported_mk {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (x : X) (xs : List (Rose X)) : IsSupported 𝔸 { label := x, children := xs } ↔ IsSupported 𝔸 x ∧ IsSupported 𝔸 xs

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

@[simp]

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

@[simp]

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

theorem NominalSets.Rose.isSupportedF_mk' {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] {f : X → Y} (hf : IsSupportedF 𝔸 f) {g : X → List (Rose Y)} (hg : IsSupportedF 𝔸 g) : IsSupportedF 𝔸 fun (x : X) => { label := f x, children := g x }

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

@[simp]

theorem NominalSets.Rose.isSupportedF_label {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] : IsSupportedF 𝔸 Rose.label

@[simp]

theorem NominalSets.Rose.isSupportedF_children {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] : IsSupportedF 𝔸 Rose.children

@[simp]

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

@[simp]

theorem NominalSets.Rose.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 → Rose Z} (hf : IsSupportedF 𝔸 fun (x : X × Y) => match x with | (x, y) => f x y) {g : X → Rose Y} (hg : IsSupportedF 𝔸 g) : IsSupportedF 𝔸 fun (x : X) => Rose.map (f x) (g x)