diff options
Diffstat (limited to 'Nominal/Instances.lean')
| -rw-r--r-- | Nominal/Instances.lean | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/Nominal/Instances.lean b/Nominal/Instances.lean index e28fe28..b637b32 100644 --- a/Nominal/Instances.lean +++ b/Nominal/Instances.lean @@ -1,5 +1,6 @@ import Mathlib import Nominal.Support +import Nominal.Equivariance /-! # Instances @@ -132,6 +133,12 @@ instance : NominalSet πΈ (X Γ Y) where lemma NominalSet.supp_product_comm {x : X} {y : Y} : supp πΈ (x, y) = supp πΈ (y, x) := by simp; apply Set.union_comm +lemma Prod.fst_equivariant : Equivariant πΈ (Prod.fst : X Γ Y β X) := by + simp [Equivariant] + +lemma Prod.snd_equivariant : Equivariant πΈ (Prod.snd : X Γ Y β Y) := by + simp [Equivariant] + end Products /-! @@ -190,4 +197,10 @@ instance : NominalSet πΈ (X β Y) where @[simp] lemma NominalSet.fresh_coproductβ {a : πΈ} {y : Y} : a # (.inr y : X β Y) β a # y := by simp [IsFresh] +lemma Sum.inl_equivariant : Equivariant πΈ (Sum.inl : X β X β Y) := by + simp [Equivariant] + +lemma Sum.inr_equivariant : Equivariant πΈ (Sum.inr : Y β X β Y) := by + simp [Equivariant] + end Coproducts |