From 2e5f7e22761bd30857bbe067862a8b256805ecd8 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <contact@haschu.me>
Date: Wed, 15 Apr 2026 16:18:07 +0200
Subject: fs constructions

---
 Nominal/Permutations.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'Nominal/Permutations.lean')

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
-- 
cgit v1.3.1