From 281326b9b7eb6561526f02ff37eab9c39aa83b58 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Wed, 22 Oct 2025 23:34:14 +0200
Subject: always require infinite, countable, equality-decidable atoms

---
 Nominal/Support.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'Nominal/Support.lean')

diff --git a/Nominal/Support.lean b/Nominal/Support.lean
index efed617..78e8b3e 100644
--- a/Nominal/Support.lean
+++ b/Nominal/Support.lean
@@ -8,7 +8,7 @@ import Nominal.Helpers.Finset
 This file provides basic definitions for support of (FPerm 𝔸)-sets and nominal sets.
 -/
 
-variable (𝔸 : Type)
+variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
 
 /-!
 ## Support Definitions
@@ -54,7 +54,7 @@ lemma support_superset {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S ⊆
   exact hπ a (hsub ha)
 
 /-- For two finite supports, the intersection is also a support. -/
-lemma support_inter [Infinite 𝔸] {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite → HasSupport 𝔸 x T → T.Finite → HasSupport 𝔸 x (S ∩ T) := by
+lemma support_inter {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite → HasSupport 𝔸 x T → T.Finite → HasSupport 𝔸 x (S ∩ T) := by
   intro h_S_support h_S_finite h_T_support h_T_finite π h_π_fix
   let π' := π.val
   let h_π_fin := π.prop
@@ -151,7 +151,7 @@ lemma support_inter [Infinite 𝔸] {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x
     _     = x                               := by rw [h_T_support h_σ_fixT]
 
 /-- For a finite number of finite supports, the intersection is also a support. -/
-lemma support_sInter [Infinite 𝔸] {x : X} {C : Set (Set 𝔸)}: C.Finite → C.Nonempty → (∀ S ∈ C, HasSupport 𝔸 x S ∧ S.Finite) → HasSupport 𝔸 x (⋂₀ C) := by
+lemma support_sInter {x : X} {C : Set (Set 𝔸)}: C.Finite → C.Nonempty → (∀ S ∈ C, HasSupport 𝔸 x S ∧ S.Finite) → HasSupport 𝔸 x (⋂₀ C) := by
   suffices (C : Finset (Set 𝔸)) : C.Nonempty → (∀ S ∈ C, HasSupport 𝔸 x S ∧ S.Finite) → HasSupport 𝔸 x (⋂₀ C.toSet) ∧ (⋂₀ C.toSet).Finite
   · intro hfin
     rw [show C = hfin.toFinset.toSet by simp]
@@ -207,7 +207,7 @@ lemma supp_finite {x : X} : (supp 𝔸 x).Finite := by
     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
+private lemma supp_equiv_finite {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
@@ -223,7 +223,7 @@ private lemma supp_equiv_finite [Infinite 𝔸] {x : X} {S : Set 𝔸} : PermSet
       · 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
+lemma supp_is_support {x : X} : PermSet.HasSupport 𝔸 x (supp 𝔸 x) := by
   obtain ⟨S, ⟨hsuppS, hfinS⟩⟩ := nom.fin_supp x
   rw [supp_equiv_finite 𝔸 hsuppS hfinS]
   apply PermSet.support_sInter
-- 
cgit v1.3.1