diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2025-10-26 01:19:45 +0200 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2025-10-26 01:20:20 +0200 |
| commit | 10edba2c0365a6858a74da22042c98f9d5fa1acc (patch) | |
| tree | e8d1b29734b02cf654d91f6b33921915e108b296 /Nominal/Permutations.lean | |
| parent | c3700706466cb8fb9ed287ea066b656caacdc9c7 (diff) | |
simplify FPerm computations
Diffstat (limited to 'Nominal/Permutations.lean')
| -rw-r--r-- | Nominal/Permutations.lean | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index 62d7470..1726ed7 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -138,13 +138,20 @@ lemma swap_mul_self {a b : X} : ⸨a, b⸩ * ⸨a, b⸩ = 1 := by apply ext simp [swap] -/-- If c is not equal to a or b, then (a b) leaves c unchanged. -/ -lemma swap_neq {a b c : X} : c ≠ a → c ≠ b → ⸨a, b⸩ c = c := by +/-- Lifting of Equiv.swap_apply_of_ne_of_ne to finite permutations. -/ +lemma swap_apply_of_ne_of_ne {a b c : X} : c ≠ a → c ≠ b → ⸨a, b⸩ c = c := by intro ha hb - apply Equiv.Perm.supp_notin - simp only [swap, Equiv.Perm.supp_swap, ne_eq, ite_not, Set.mem_ite_empty_left, Set.mem_insert_iff, Set.mem_singleton_iff, not_and, not_or] - intro _ - exact ⟨ha, hb⟩ + simp [swap, Equiv.swap_apply_of_ne_of_ne, ha, hb] + +/-- Lifting of Equiv.swap_apply_left to finite permutations. -/ +@[simp] +lemma swap_apply_left (a b : X) : ⸨a, b⸩ a = b := by + simp [swap] + +/-- Lifting of Equiv.swap_apply_right to finite permutations. -/ +@[simp] +lemma swap_apply_right (a b : X) : ⸨a, b⸩ b = a := by + simp [swap] end FPerm |