diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2025-10-22 18:24:29 +0200 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2025-10-22 18:24:29 +0200 |
| commit | aceb6d9d4b27c642057f025b03333ee375661609 (patch) | |
| tree | eb70823e52162a1046576d2e3ce338f19f244e0e | |
| parent | 1207e99c440de6af718a7fdef1810b726925cdb9 (diff) | |
some helper lemmas for fix
| -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'] |