diff options
Diffstat (limited to 'Nominal/Instances/Basic.lean')
| -rw-r--r-- | Nominal/Instances/Basic.lean | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean index b627c1b..7a88eeb 100644 --- a/Nominal/Instances/Basic.lean +++ b/Nominal/Instances/Basic.lean @@ -59,6 +59,7 @@ Every set can be made into a discrete nominal set, where supp x = โ
. -/ section Discrete +@[reducible] def NominalSet.mkDiscrete (X : Type) : NominalSet.Discrete ๐ธ X where smul ฯ x := x one_smul := by intro; rfl @@ -330,6 +331,7 @@ instance : PermSet ๐ธ (Quotient setoid) where instance instMkEquivariant : Function.Equivariant ๐ธ (Quotient.mk setoid) := by constructor; simp +@[reducible] def lift_equivariant {Y : Type} [PermSet ๐ธ Y] (f : X โ Y) [Function.Equivariant ๐ธ f] (h : โ (a b : X), a โ b โ f a = f b) : @@ -392,11 +394,11 @@ instance : PermSet ๐ธ S where rw [โ Set.equivariant ๐ธ S] exact x.propโฉ one_smul x := by - apply Subtype.eq + apply Subtype.ext exact MulAction.one_smul x.val mul_smul ฯ ฯ x := by - apply Subtype.eq - exact MulAction.mul_smul ฯ ฯ x.val + apply Subtype.ext + exact SemigroupAction.mul_smul ฯ ฯ x.val @[simp] lemma smul_val (ฯ : FPerm ๐ธ) (x : S) : (ฯ โข x).val = ฯ โข x.val := rfl @@ -410,7 +412,7 @@ instance : NominalSet ๐ธ S where use NominalSet.supp ๐ธ x.val constructor ยท intro ฯ hฯ - apply Subtype.eq + apply Subtype.ext exact NominalSet.supp_is_support ๐ธ hฯ ยท exact NominalSet.supp_finite ๐ธ |