diff options
Diffstat (limited to 'Nominal/Permutations.lean')
| -rw-r--r-- | Nominal/Permutations.lean | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index f1115d3..6119df3 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -259,4 +259,16 @@ lemma PermSet.atom_set_swap_left {a b : 𝔸} {S : Set 𝔸} : a ∈ S ↔ b ∈ lemma PermSet.atom_set_swap_right {a b : 𝔸} {S : Set 𝔸} : b ∈ S ↔ a ∈ ⸨a, b⸩ • S := by rw [FPerm.swap_comm, atom_set_swap_left] +instance {X Y : Type} [SMul (FPerm 𝔸) X] [SMul (FPerm 𝔸) Y] : SMul (FPerm 𝔸) (X → Y) where + smul π f := fun x ↦ π • f (π⁻¹ • x) + +@[simp] lemma PermSet.smul_function {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] (π : FPerm 𝔸) + (f : X → Y) (x : X) : (π • f) x = π • f (π⁻¹ • x) := + rfl + +/-- Functions between (FPerm 𝔸)-sets form (FPerm 𝔸)-sets with (π • f) x = π • f (π⁻¹ • x). -/ +instance {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] : PermSet 𝔸 (X → Y) where + one_smul f := by ext x; simp + mul_smul π τ f := by ext x; simp [mul_smul] + end PermSet |