diff options
| -rw-r--r-- | Nominal/Basic.lean | 39 |
1 files changed, 20 insertions, 19 deletions
diff --git a/Nominal/Basic.lean b/Nominal/Basic.lean index 1a7f6ac..dde26fc 100644 --- a/Nominal/Basic.lean +++ b/Nominal/Basic.lean @@ -76,15 +76,19 @@ def HasSupport (x : X) (S : Set 𝔸) : Prop := lemma support_iff {x : X} {S : Set 𝔸} : HasSupport 𝔸 x S ↔ ∀ (π : FPerm 𝔸), (∀ x ∈ S, π x = x) → π ∈ fix' 𝔸 x := by constructor · intro hsupp π hπ - aesop + exact hsupp hπ · intro hsupp π hπ - aesop + exact hsupp π hπ lemma support_subset {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S ⊆ T → HasSupport 𝔸 x T := by intro hS hsub π hπ apply hS - intro a - aesop + intro a ha + exact hπ a (hsub ha) + +#check Set.Finite.exists_injOn_of_encard_le +#check Set.injOn_iff_injective +#check Function.partialInv_of_injective lemma support_inter {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite → HasSupport 𝔸 x T → T.Finite → HasSupport 𝔸 x (S ∩ T) := by sorry @@ -202,27 +206,24 @@ lemma NominalSet.supp_atoms [Infinite 𝔸] [DecidableEq 𝔸] {a : 𝔸} : supp · apply NominalSet.supp_atoms' · simp · suffices : a ∈ supp 𝔸 a - -- TODO: Shorten · simp; intro h; rw [h]; assumption · intro S ⟨hsuppS, hfinS⟩ - by_contra - have hfin : ({a} ∪ S).Finite := by - apply Set.finite_union.mpr; simp [hfinS] - obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset hfin.toFinset - have h₁ : c ≠ a := by aesop - have h₂ : c ∉ S := by aesop - have h₃ : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by + 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 - rw [Equiv.Perm.supp_swap] - aesop - have h₄ : ⸨a, c⸩ • a = c := by + 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] - unfold PermSet.HasSupport at hsuppS - specialize hsuppS h₃ - simp [PermSet.fix'] at hsuppS - aesop + have ha₂ : ⸨a, c⸩ • a = a := by + specialize hsuppS hfix + simpa [PermSet.fix'] + rw [ha₁] at ha₂ + exact hc.left ha₂ class DiscreteNominalSet (X : Type) extends NominalSet 𝔸 X, DiscretePermSet 𝔸 X |