instance RenamingSets.Prod.instRenameActionProd {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] : RenameAction 𝔸 (X × Y)

Equations

• RenamingSets.Prod.instRenameActionProd = { rename := fun (σ : RenamingSets.Ren 𝔸) (x : X × Y) => (RenamingSets.rename σ x.1, RenamingSets.rename σ x.2), rename_one := ⋯, rename_mul := ⋯ }

theorem RenamingSets.Prod.rename_def {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] (σ : Ren 𝔸) (x : X × Y) : rename σ x = (rename σ x.1, rename σ x.2)

@[simp]

theorem RenamingSets.Prod.rename_mk {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] (σ : Ren 𝔸) (x : X) (y : Y) : rename σ (x, y) = (rename σ x, rename σ y)

@[simp]

theorem RenamingSets.Prod.isSupportOf_mk {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] (A : Finset 𝔸) (x : X) (y : Y) : IsSupportOf A (x, y) ↔ IsSupportOf A x ∧ IsSupportOf A y

@[simp]

theorem RenamingSets.Prod.isSupported_mk {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] (x : X) (y : Y) : IsSupported 𝔸 (x, y) ↔ IsSupported 𝔸 x ∧ IsSupported 𝔸 y

@[simp]

theorem RenamingSets.Prod.isSupportOfF_fst {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] (A : Finset 𝔸) : IsSupportOfF A Prod.fst

@[simp]

theorem RenamingSets.Prod.equivariant_fst {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] : Equivariant 𝔸 Prod.fst

@[simp]

theorem RenamingSets.Prod.isSupportedF_fst {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] : IsSupportedF 𝔸 Prod.fst

@[simp]

theorem RenamingSets.Prod.equivariant_fst' {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenameAction 𝔸 Z] {f : X → Y × Z} (hf : Equivariant 𝔸 f) : Equivariant 𝔸 fun (x : X) => (f x).1

@[simp]

theorem RenamingSets.Prod.isSupportedF_fst' {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenameAction 𝔸 Z] {f : X → Y × Z} (hf : IsSupportedF 𝔸 f) : IsSupportedF 𝔸 fun (x : X) => (f x).1

@[simp]

theorem RenamingSets.Prod.isSupportOfF_snd {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] (A : Finset 𝔸) : IsSupportOfF A Prod.snd

@[simp]

theorem RenamingSets.Prod.equivariant_snd {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] : Equivariant 𝔸 Prod.snd

@[simp]

theorem RenamingSets.Prod.isSupportedF_snd {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] : IsSupportedF 𝔸 Prod.snd

@[simp]

theorem RenamingSets.Prod.equivariant_snd' {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenameAction 𝔸 Z] {f : X → Y × Z} (hf : Equivariant 𝔸 f) : Equivariant 𝔸 fun (x : X) => (f x).2

@[simp]

theorem RenamingSets.Prod.isSupportedF_snd' {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenameAction 𝔸 Z] {f : X → Y × Z} (hf : IsSupportedF 𝔸 f) : IsSupportedF 𝔸 fun (x : X) => (f x).2

@[simp]

theorem RenamingSets.Prod.isSupportOfF_mk {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenameAction 𝔸 Z] (A : Finset 𝔸) {f : X → Y} (hf : IsSupportOfF A f) {g : X → Z} (hg : IsSupportOfF A g) : IsSupportOfF A fun (x : X) => (f x, g x)

@[simp]

theorem RenamingSets.Prod.equivariant_mk {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenameAction 𝔸 Z] {f : X → Y} (hf : Equivariant 𝔸 f) {g : X → Z} (hg : Equivariant 𝔸 g) : Equivariant 𝔸 fun (x : X) => (f x, g x)

@[simp]

theorem RenamingSets.Prod.isSupportedF_mk {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenameAction 𝔸 Z] {f : X → Y} (hf : IsSupportedF 𝔸 f) {g : X → Z} (hg : IsSupportedF 𝔸 g) : IsSupportedF 𝔸 fun (x : X) => (f x, g x)

instance RenamingSets.Prod.instRenamingSetProd {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenamingSet 𝔸 X] [RenamingSet 𝔸 Y] : RenamingSet 𝔸 (X × Y)

@[simp]

theorem RenamingSets.Prod.supp_mk {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenamingSet 𝔸 X] [RenamingSet 𝔸 Y] [DecidableEq 𝔸] (x : X) (y : Y) : supp 𝔸 (x, y) = supp 𝔸 x ∪ supp 𝔸 y