diff options
Diffstat (limited to 'Nominal/Instances/Basic.lean')
| -rw-r--r-- | Nominal/Instances/Basic.lean | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean index 2ebe9b1..d41e87f 100644 --- a/Nominal/Instances/Basic.lean +++ b/Nominal/Instances/Basic.lean @@ -140,11 +140,11 @@ instance : NominalSet ๐ธ (X ร Y) where lemma supp_comm {x : X} {y : Y} : NominalSet.supp ๐ธ (x, y) = NominalSet.supp ๐ธ (y, x) := by simp; apply Set.union_comm -lemma fst_equivariant : Equivariant ๐ธ (Prod.fst : X ร Y โ X) := by - simp [Equivariant] +lemma fst_equivariant : Function.Equivariant ๐ธ (Prod.fst : X ร Y โ X) := by + simp [Function.Equivariant] -lemma snd_equivariant : Equivariant ๐ธ (Prod.snd : X ร Y โ Y) := by - simp [Equivariant] +lemma snd_equivariant : Function.Equivariant ๐ธ (Prod.snd : X ร Y โ Y) := by + simp [Function.Equivariant] end Prod @@ -212,11 +212,11 @@ instance : NominalSet ๐ธ (X โ Y) where @[simp] lemma fresh_inr {a : ๐ธ} {y : Y} : a # (.inr y : X โ Y) โ a # y := by simp [NominalSet.IsFresh] -lemma inl_equivariant : Equivariant ๐ธ (Sum.inl : X โ X โ Y) := by - simp [Equivariant] +lemma inl_equivariant : Function.Equivariant ๐ธ (Sum.inl : X โ X โ Y) := by + simp [Function.Equivariant] -lemma inr_equivariant : Equivariant ๐ธ (Sum.inr : Y โ X โ Y) := by - simp [Equivariant] +lemma inr_equivariant : Function.Equivariant ๐ธ (Sum.inr : Y โ X โ Y) := by + simp [Function.Equivariant] end Sum @@ -251,8 +251,8 @@ instance : PermSet ๐ธ (Quotient setoid.toSetoid) where apply Quotient.ind simp [mul_smul] -lemma mk_equivariant : Equivariant ๐ธ (Quotient.mk setoid.toSetoid) := by - simp [Equivariant] +lemma mk_equivariant : Function.Equivariant ๐ธ (Quotient.mk setoid.toSetoid) := by + simp [Function.Equivariant] variable {X : Type} [NominalSet ๐ธ X] {setoid : EquivariantSetoid ๐ธ X} @@ -265,7 +265,7 @@ lemma supp {x : X} : NominalSet.supp ๐ธ (Quotient.mk setoid.toSetoid x) = {a | ยท intro ha x' hx' rw [โ Quotient.sound hx'] at ha have hsub : NominalSet.supp ๐ธ (Quotient.mk setoid.toSetoid x') โ NominalSet.supp ๐ธ x' := - Equivariant.supp_subset ๐ธ (mk_equivariant ๐ธ) + Function.Equivariant.supp_subset ๐ธ (mk_equivariant ๐ธ) exact hsub ha ยท contrapose; intro ha simp only [Set.mem_setOf_eq, Classical.not_imp, not_forall] |