diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2025-10-22 23:34:14 +0200 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2025-10-22 23:34:14 +0200 |
| commit | 281326b9b7eb6561526f02ff37eab9c39aa83b58 (patch) | |
| tree | e97e1bd1c1ca95d7775a988af3a65a90e50fa94e /Nominal/Permutations.lean | |
| parent | b1a5137ed3f2d7810a1670d2e3888e8a87d89b02 (diff) | |
always require infinite, countable, equality-decidable atoms
Diffstat (limited to 'Nominal/Permutations.lean')
| -rw-r--r-- | Nominal/Permutations.lean | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index dd9b9d2..c8fdd86 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -136,10 +136,10 @@ Sets equipped with a permutation operation. -/ section PermSet -variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] - /-- A set X equipped with a group action •: (FPerm 𝔸) × X → X. -/ -class PermSet (X : Type) extends MulAction (FPerm 𝔸) X +class PermSet (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] (X : Type) extends MulAction (FPerm 𝔸) X + +variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] /-- The set of atoms itself forms a (FPerm 𝔸)-Set. -/ instance : PermSet 𝔸 𝔸 where |