diff options
Diffstat (limited to 'Nominal/Support.lean')
| -rw-r--r-- | Nominal/Support.lean | 10 |
1 files changed, 10 insertions, 0 deletions
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'] |