diff options
Diffstat (limited to 'Nominal/Support.lean')
| -rw-r--r-- | Nominal/Support.lean | 65 |
1 files changed, 27 insertions, 38 deletions
diff --git a/Nominal/Support.lean b/Nominal/Support.lean index 6a1d4d9..d8058e0 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -35,11 +35,7 @@ def HasSupport (x : X) (S : Set 𝔸) : Prop := /-- Alternative definition with fix 𝔸 S unfolded. -/ lemma support_iff {x : X} {S : Set 𝔸} : HasSupport 𝔸 x S ↔ ∀ (π : FPerm 𝔸), (∀ x ∈ S, π x = x) → π ∈ fix' 𝔸 x := by - constructor - · intro hsupp π hπ - exact hsupp hπ - · intro hsupp π hπ - exact hsupp π hπ + simp [HasSupport, fix, fix'] /-- If a support is a subset of another set, that set is also a support. -/ lemma support_superset {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S ⊆ T → HasSupport 𝔸 x T := by @@ -155,21 +151,15 @@ lemma support_sInter [Infinite 𝔸] {x : X} {C : Set (Set 𝔸)}: C.Finite → · have : DecidableEq (Set 𝔸) := Classical.typeDecidableEq (Set 𝔸) apply Finset.Nonempty.induction · intro S hS - rw [show ⋂₀ ({S} : Finset (Set 𝔸)).toSet = S by simp] - apply hS - simp + rw [Finset.coe_singleton S, Set.sInter_singleton S] + apply hS S (Finset.mem_singleton.mpr rfl) · intro S C' hS hC' hsing rw [Finset.coe_insert S C', Set.sInter_insert S ↑C'] - have hother : (∀ S ∈ C', HasSupport 𝔸 x S ∧ S.Finite) := by - intro S' hS' - apply hsing - exact Finset.mem_insert_of_mem hS' - specialize hC' hother - specialize hsing S (by simp) + specialize hC' (fun S' hS' => hsing S' (Finset.mem_insert_of_mem hS')) + specialize hsing S (Finset.mem_insert_self S C') constructor - · apply support_inter 𝔸 hsing.left hsing.right hC'.left hC'.right - · apply Set.Finite.inter_of_left - exact hsing.right + · exact support_inter 𝔸 hsing.left hsing.right hC'.left hC'.right + · apply Set.Finite.inter_of_left hsing.right end PermSet @@ -182,8 +172,6 @@ Nominal sets are then just (FPerm 𝔸)-Sets where all elements are finitely sup -/ section NominalSet -variable (𝔸 : Type) - /-- An (FPerm 𝔸)-Set X is nominal if every x ∈ X is finitely supported. -/ class NominalSet (X : Type) extends PermSet 𝔸 X where fin_supp : ∀ (x : X), ∃ (S : Set 𝔸), PermSet.HasSupport 𝔸 x S ∧ S.Finite @@ -206,31 +194,32 @@ lemma supp_finite {x : X} : (supp 𝔸 x).Finite := by obtain ⟨S, ⟨hsuppS, hfinS⟩⟩ := nom.fin_supp x apply Set.Finite.subset · exact hfinS - · grind + · apply Set.sInter_subset_of_mem + exact Set.mem_sep hsuppS hfinS + +/-- We can restrict the supp definition to subsets of a single finite support. -/ +private lemma supp_equiv_finite [Infinite 𝔸] {x : X} {S : Set 𝔸} : PermSet.HasSupport 𝔸 x S → S.Finite → supp 𝔸 x = ⋂₀ { T : Set 𝔸 | T ⊆ S ∧ PermSet.HasSupport 𝔸 x T ∧ T.Finite } := by + intro hsuppS hfinS + unfold supp; ext a + constructor + · intro h T hT + exact h T hT.out.right + · intro h T hT + suffices a ∈ S ∩ T by apply Set.mem_of_mem_inter_right; assumption + apply h + constructor + · exact Set.inter_subset_left + · constructor + · exact PermSet.support_inter 𝔸 hsuppS hfinS hT.out.left hT.out.right + · exact Set.Finite.inter_of_left hfinS T /-- The least finite support is itself a support. -/ lemma supp_is_support [Infinite 𝔸] {x : X} : PermSet.HasSupport 𝔸 x (supp 𝔸 x) := by obtain ⟨S, ⟨hsuppS, hfinS⟩⟩ := nom.fin_supp x - have suppf : (supp 𝔸 x = ⋂₀ { T : Set 𝔸 | T ⊆ S ∧ PermSet.HasSupport 𝔸 x T ∧ T.Finite }) := by - unfold supp; ext a - constructor - · intro h T hT - apply h - exact hT.out.right - · intro h T hT - suffices : a ∈ S ∩ T - · apply Set.mem_of_mem_inter_right; assumption - · apply h - constructor - · exact Set.inter_subset_left - · constructor - · exact PermSet.support_inter 𝔸 hsuppS hfinS hT.out.left hT.out.right - · apply Set.Finite.inter_of_left; assumption - rw [suppf] + rw [supp_equiv_finite 𝔸 hsuppS hfinS] apply PermSet.support_sInter · apply Set.Finite.subset - · apply Set.Finite.powerset - exact hfinS + · exact Set.Finite.powerset hfinS · intro T hT exact hT.out.left · use S |