instance
RenamingSets.Sum.instRenameActionSum
{𝔸 : Type u_1}
{X : Type u_2}
[RenameAction 𝔸 X]
{Y : Type u_3}
[RenameAction 𝔸 Y]
:
RenameAction 𝔸 (X ⊕ Y)
Equations
- RenamingSets.Sum.instRenameActionSum = { rename := fun (σ : RenamingSets.Ren 𝔸) => Sum.map (RenamingSets.rename σ) (RenamingSets.rename σ), rename_one := ⋯, rename_mul := ⋯ }
theorem
RenamingSets.Sum.rename_def
{𝔸 : Type u_1}
{X : Type u_2}
[RenameAction 𝔸 X]
{Y : Type u_3}
[RenameAction 𝔸 Y]
(σ : Ren 𝔸)
(a✝ : X ⊕ Y)
:
@[simp]
theorem
RenamingSets.Sum.rename_inl
{𝔸 : Type u_1}
{X : Type u_2}
[RenameAction 𝔸 X]
{Y : Type u_3}
[RenameAction 𝔸 Y]
(σ : Ren 𝔸)
(x : X)
:
@[simp]
theorem
RenamingSets.Sum.isSupportOf_inl
{𝔸 : Type u_1}
{X : Type u_2}
[RenameAction 𝔸 X]
{Y : Type u_3}
[RenameAction 𝔸 Y]
(A : Finset 𝔸)
(x : X)
:
@[simp]
theorem
RenamingSets.Sum.isSupported_inl
{𝔸 : Type u_1}
{X : Type u_2}
[RenameAction 𝔸 X]
{Y : Type u_3}
[RenameAction 𝔸 Y]
(x : X)
:
@[simp]
theorem
RenamingSets.Sum.isSupportOfF_inl
{𝔸 : Type u_1}
{X : Type u_2}
[RenameAction 𝔸 X]
{Y : Type u_3}
[RenameAction 𝔸 Y]
(A : Finset 𝔸)
:
@[simp]
theorem
RenamingSets.Sum.isSupportedF_inl
{𝔸 : Type u_1}
{X : Type u_2}
[RenameAction 𝔸 X]
{Y : Type u_3}
[RenameAction 𝔸 Y]
:
@[simp]
theorem
RenamingSets.Sum.isSupportedF_inl'
{𝔸 : Type u_1}
{X : Type u_2}
[RenameAction 𝔸 X]
{Y : Type u_3}
[RenameAction 𝔸 Y]
{Z : Type u_4}
[RenameAction 𝔸 Z]
{f : X → Y}
(hf : IsSupportedF 𝔸 f)
:
IsSupportedF 𝔸 fun (x : X) => Sum.inl (f x)
@[simp]
theorem
RenamingSets.Sum.rename_inr
{𝔸 : Type u_1}
{X : Type u_2}
[RenameAction 𝔸 X]
{Y : Type u_3}
[RenameAction 𝔸 Y]
(σ : Ren 𝔸)
(x : Y)
:
@[simp]
theorem
RenamingSets.Sum.isSupportOf_inr
{𝔸 : Type u_1}
{X : Type u_2}
[RenameAction 𝔸 X]
{Y : Type u_3}
[RenameAction 𝔸 Y]
(A : Finset 𝔸)
(x : Y)
:
@[simp]
theorem
RenamingSets.Sum.isSupported_inr
{𝔸 : Type u_1}
{X : Type u_2}
[RenameAction 𝔸 X]
{Y : Type u_3}
[RenameAction 𝔸 Y]
(x : Y)
:
@[simp]
theorem
RenamingSets.Sum.isSupportOfF_inr
{𝔸 : Type u_1}
{X : Type u_2}
[RenameAction 𝔸 X]
{Y : Type u_3}
[RenameAction 𝔸 Y]
(A : Finset 𝔸)
:
@[simp]
theorem
RenamingSets.Sum.isSupportedF_inr
{𝔸 : Type u_1}
{X : Type u_2}
[RenameAction 𝔸 X]
{Y : Type u_3}
[RenameAction 𝔸 Y]
:
@[simp]
theorem
RenamingSets.Sum.isSupportedF_inr'
{𝔸 : Type u_1}
{X : Type u_2}
[RenameAction 𝔸 X]
{Y : Type u_3}
[RenameAction 𝔸 Y]
{Z : Type u_4}
[RenameAction 𝔸 Z]
{f : X → Z}
(hf : IsSupportedF 𝔸 f)
:
IsSupportedF 𝔸 fun (x : X) => Sum.inr (f x)
@[simp]
theorem
RenamingSets.Sum.isSupportOfF_elim
{𝔸 : Type u_1}
{X : Type u_2}
[RenameAction 𝔸 X]
{Y : Type u_3}
[RenameAction 𝔸 Y]
{Z : Type u_4}
[RenameAction 𝔸 Z]
{W : Type u_5}
[RenameAction 𝔸 W]
(A : Finset 𝔸)
{f : X → Y → W}
(hf :
IsSupportOfF A fun (x : X × Y) =>
match x with
| (x, y) => f x y)
{g : X → Z → W}
(hg :
IsSupportOfF A fun (x : X × Z) =>
match x with
| (x, y) => g x y)
{h : X → Y ⊕ Z}
(hh : IsSupportOfF A h)
:
IsSupportOfF A fun (x : X) => Sum.elim (f x) (g x) (h x)
@[simp]
theorem
RenamingSets.Sum.isSupportedF_mk
{𝔸 : Type u_1}
{X : Type u_2}
[RenameAction 𝔸 X]
{Y : Type u_3}
[RenameAction 𝔸 Y]
{Z : Type u_4}
[RenameAction 𝔸 Z]
{W : Type u_5}
[RenameAction 𝔸 W]
{f : X → Y → W}
(hf :
IsSupportedF 𝔸 fun (x : X × Y) =>
match x with
| (x, y) => f x y)
{g : X → Z → W}
(hg :
IsSupportedF 𝔸 fun (x : X × Z) =>
match x with
| (x, y) => g x y)
{h : X → Y ⊕ Z}
(hh : IsSupportedF 𝔸 h)
:
IsSupportedF 𝔸 fun (x : X) => Sum.elim (f x) (g x) (h x)
instance
RenamingSets.Sum.instRenamingSetSum
{𝔸 : Type u_1}
{X : Type u_2}
[RenameAction 𝔸 X]
{Y : Type u_3}
[RenameAction 𝔸 Y]
[RenamingSet 𝔸 X]
[RenamingSet 𝔸 Y]
:
RenamingSet 𝔸 (X ⊕ Y)
@[simp]
theorem
RenamingSets.Sum.supp_inl
{𝔸 : Type u_1}
{X : Type u_2}
[RenameAction 𝔸 X]
{Y : Type u_3}
[RenameAction 𝔸 Y]
[RenamingSet 𝔸 X]
[RenamingSet 𝔸 Y]
(x : X)
:
@[simp]
theorem
RenamingSets.Sum.supp_inr
{𝔸 : Type u_1}
{X : Type u_2}
[RenameAction 𝔸 X]
{Y : Type u_3}
[RenameAction 𝔸 Y]
[RenamingSet 𝔸 X]
[RenamingSet 𝔸 Y]
(x : Y)
: