diff options
Diffstat (limited to 'Nominal/Instances/Basic.lean')
| -rw-r--r-- | Nominal/Instances/Basic.lean | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean index dcca75b..64b6425 100644 --- a/Nominal/Instances/Basic.lean +++ b/Nominal/Instances/Basic.lean @@ -70,6 +70,21 @@ def NominalSet.mkDiscrete (X : Type) : NominalSet.Discrete ๐ธ X where ยท intro ฯ hฯ; simp only [PermSet.fix', Set.mem_setOf_eq]; rfl ยท exact Set.finite_empty +instance {X : Type} [NominalSet.Discrete ๐ธ X] [Finite X] : OrbitFinite ๐ธ X where + fin_orbits := Finite.of_equiv X + { toFun x := Quotient.mk _ x + invFun x := x.out + left_inv x := by + suffices โ (x y : X), MulAction.orbitRel (FPerm ๐ธ) X x y โ x = y by + apply this + rw [โ Quotient.eq] + apply Quotient.out_eq + intro x y โจฯ, hฯโฉ + simp only [NominalSet.Discrete.is_discrete] at hฯ + exact hฯ.symm + right_inv x := by simp + } + @[simp] lemma NominalSet.Discrete.supp {X : Type} [NominalSet.Discrete ๐ธ X] {x : X} : supp ๐ธ x = โ
:= by rw [โ Set.subset_empty_iff] apply Set.sInter_subset_of_mem |