diff options
| -rw-r--r-- | Nominal/Support.lean | 9 |
1 files changed, 9 insertions, 0 deletions
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'] |