From aceb6d9d4b27c642057f025b03333ee375661609 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Wed, 22 Oct 2025 18:24:29 +0200
Subject: some helper lemmas for fix

---
 Nominal/Support.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'Nominal')

diff --git a/Nominal/Support.lean b/Nominal/Support.lean
index d8058e0..0df541c 100644
--- a/Nominal/Support.lean
+++ b/Nominal/Support.lean
@@ -33,6 +33,15 @@ def fix (A : Set X) : Set (FPerm 𝔸) :=
 def HasSupport (x : X) (S : Set 𝔸) : Prop :=
   fix 𝔸 S ⊆ fix' 𝔸 x
 
+/-- 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
+  exact hπ x (hsub hx)
+
+/-- If π fixes S ∪ T, it fixes both S and T. -/
+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]
+
 /-- 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