diff options
Diffstat (limited to 'Nominal/Permutations.lean')
| -rw-r--r-- | Nominal/Permutations.lean | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index 0a4974a..f1115d3 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -42,7 +42,7 @@ lemma supp_one : (1 : Equiv.Perm X).supp = ∅ := by /-- The support of the inverse function is the same as the function's support. -/ lemma supp_inv (π : Equiv.Perm X) : π⁻¹.supp = π.supp := by - simp [supp, set_support_inv_eq] + simp [supp, set_support_symm_eq] /-- The support of two concatenated permutations is a subset of the individual supports as a union. -/ lemma supp_mul_subset (π τ : Equiv.Perm X) : (π * τ).supp ⊆ π.supp ∪ τ.supp := by @@ -199,10 +199,10 @@ instance : PermSet 𝔸 𝔸 where instance : OrbitFinite 𝔸 𝔸 where fin_orbits := Finite.of_equiv Unit - { toFun _ := Quotient.mk _ (inferInstanceAs (Nonempty 𝔸)).some + { toFun _ := Quotient.mk _ (inferInstance : Nonempty 𝔸).some invFun _ := () right_inv := by - let chosen := (inferInstanceAs (Nonempty 𝔸)).some + let chosen := (inferInstance : Nonempty 𝔸).some apply Quotient.ind; intro a rw [Quotient.eq] show chosen ∈ MulAction.orbit (FPerm 𝔸) a |