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/Support.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'Nominal/Support.lean')

diff --git a/Nominal/Support.lean b/Nominal/Support.lean
index fde20c7..bb2ec92 100644
--- a/Nominal/Support.lean
+++ b/Nominal/Support.lean
@@ -33,6 +33,11 @@ def fix (A : Set X) : Set (FPerm 𝔸) :=
 def HasSupport (x : X) (S : Set 𝔸) : Prop :=
   fix 𝔸 S ⊆ fix' 𝔸 x
 
+lemma perm_fixes_iff_inv_fixes {X : Type} [PermSet 𝔸 X] (π : FPerm 𝔸) (x : X) : π • x = x ↔ π⁻¹ • x = x := by
+  constructor
+  · intro h; nth_rw 1 [← h]; simp
+  · intro h; nth_rw 1 [← h]; simp
+
 /-- fix is antitone: If S ⊆ T, then fix S ⊇ fix T. -/
 lemma fix_antitone {X : Type} [PermSet 𝔸 X] {S T : Set X} : S ⊆ T → PermSet.fix 𝔸 T ⊆ PermSet.fix 𝔸 S := by
   intro hsub π hπ x hx
@@ -48,6 +53,11 @@ lemma fix_antitone_mem {X : Type} [PermSet 𝔸 X] {S T : Set X} {π : FPerm 
 lemma fix_union {X : Type} [PermSet 𝔸 X] {S T : Set X} : PermSet.fix 𝔸 (S ∪ T) ⊆ PermSet.fix 𝔸 S ∩ PermSet.fix 𝔸 T := by
   apply Set.subset_inter <;> all_goals simp [fix_antitone]
 
+lemma fix_inv {X : Type} [PermSet 𝔸 X] {S : Set X} {π : FPerm 𝔸} : π ∈ PermSet.fix 𝔸 S ↔ π⁻¹ ∈ PermSet.fix 𝔸 S := by
+  constructor
+  · intro h x hx; rw [← perm_fixes_iff_inv_fixes]; exact h x hx
+  · intro h x hx; rw [perm_fixes_iff_inv_fixes]; exact h x hx
+
 /-- Alternative definition with fix 𝔸 S unfolded. -/
 lemma support_iff {x : X} {S : Set 𝔸} : HasSupport 𝔸 x S ↔ ∀ (π : FPerm 𝔸), (∀ x ∈ S, π x = x) → π ∈ fix' 𝔸 x := by
   simp [HasSupport, fix, fix']
-- 
cgit v1.3.1