diff options
Diffstat (limited to 'Nominal/Permutations.lean')
| -rw-r--r-- | Nominal/Permutations.lean | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index c8fdd86..4a3e88f 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -141,16 +141,21 @@ class PermSet (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] -/-- The set of atoms itself forms a (FPerm 𝔸)-Set. -/ +/-- The set of atoms itself forms an (FPerm 𝔸)-Set. -/ instance : PermSet 𝔸 𝔸 where smul π a := π a one_smul := by intro; rfl mul_smul := by intro _ _ _; rfl -/-- The set of finite permutations forms a (FPerm 𝔸)-Set. -/ +/-- The set of finite permutations forms an (FPerm 𝔸)-Set. -/ instance : PermSet 𝔸 (FPerm 𝔸) where smul π τ := π * τ one_smul := by intro; rfl mul_smul := by intro _ _ _; rfl +open Pointwise + +/-- The powerset of an (FPerm 𝔸)-Set forms an (FPerm 𝔸)-Set using pointwise permutation. -/ +instance {X : Type} [PermSet 𝔸 X] : PermSet 𝔸 (Set X) where + end PermSet |