diff options
| author | Hannes Schulze <contact@haschu.me> | 2026-04-14 16:04:44 +0200 |
|---|---|---|
| committer | Hannes Schulze <contact@haschu.me> | 2026-04-15 13:22:40 +0200 |
| commit | a5ff8efe5b5e314e0aa759318e5fb194e066f612 (patch) | |
| tree | 4d13dd84ac4ced2360a51799f0e5c846bd733872 /Nominal/Permutations.lean | |
| parent | 43942e78f4b3ed4cfca3b508f06161d0983c545e (diff) | |
update lean
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 |