diff options
Diffstat (limited to 'Nominal/Instances.lean')
| -rw-r--r-- | Nominal/Instances.lean | 46 |
1 files changed, 19 insertions, 27 deletions
diff --git a/Nominal/Instances.lean b/Nominal/Instances.lean index 793baa4..bf1d372 100644 --- a/Nominal/Instances.lean +++ b/Nominal/Instances.lean @@ -23,34 +23,28 @@ instance : NominalSet 𝔸 𝔸 where fin_supp := by intro a use {a} - constructor - · exact NominalSet.supp_atoms' 𝔸 - · simp + exact ⟨NominalSet.supp_atoms' 𝔸, Set.finite_singleton a⟩ lemma NominalSet.supp_atoms [Infinite 𝔸] [DecidableEq 𝔸] {a : 𝔸} : supp 𝔸 a = {a} := by ext b; constructor · apply support_subset_supp · apply NominalSet.supp_atoms' - · simp - · suffices : a ∈ supp 𝔸 a - · simp; intro h; rw [h]; assumption - · intro S ⟨hsuppS, hfinS⟩ - by_contra ha - obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset ({a} ∪ hfinS.toFinset) - simp at hc - have hfix : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by - intro d hd - rw [show ⸨a,c⸩ • d = (Equiv.swap a c) d from rfl] - apply Equiv.Perm.supp_notin - simp [Equiv.Perm.supp_swap, Ne.symm hc.left] - exact ⟨ne_of_mem_of_not_mem hd ha, ne_of_mem_of_not_mem hd hc.right⟩ - have ha₁ : ⸨a, c⸩ • a = c := by - simp [show ⸨a,c⸩ • a = (Equiv.swap a c) a from rfl] - have ha₂ : ⸨a, c⸩ • a = a := by - specialize hsuppS hfix - simpa [PermSet.fix'] - rw [ha₁] at ha₂ - exact hc.left ha₂ + · apply Set.finite_singleton + · suffices a ∈ supp 𝔸 a by simp; intro h; rwa [h] + intro S ⟨hsuppS, hfinS⟩ + by_contra ha + -- Show that we can find a fresh c with (a c) ∈ fix S + obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset ({a} ∪ hfinS.toFinset) + simp at hc + have hfix : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by + intro d hd + apply Equiv.Perm.supp_notin + simp [FPerm.swap, Equiv.Perm.supp_swap, Ne.symm hc.left] + exact ⟨ne_of_mem_of_not_mem hd ha, ne_of_mem_of_not_mem hd hc.right⟩ + have h₁ : ⸨a, c⸩ • a = c := by simp [show ⸨a,c⸩ • a = (Equiv.swap a c) a from rfl] + have h₂ : ⸨a, c⸩ • a = a := by apply hsuppS; assumption + rw [h₁] at h₂ + exact hc.left h₂ end Atoms @@ -71,15 +65,13 @@ def NominalSet.discrete (X : Type) : DiscreteNominalSet 𝔸 X where use {} constructor · intro π hπ; simp [PermSet.fix']; rfl - · simp + · exact Set.finite_empty lemma NominalSet.supp_discrete {X : Type} [DiscreteNominalSet 𝔸 X] {x : X} : supp 𝔸 x = ∅ := by rw [← Set.subset_empty_iff] apply Set.sInter_subset_of_mem constructor - · intro π hπ - simp [PermSet.fix'] - exact DiscreteNominalSet.is_discrete x π + · intro π hπ; simp [PermSet.fix', DiscreteNominalSet.is_discrete] · exact Set.finite_empty /-- We consider Unit a discrete nominal set. -/ |