diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2025-10-22 23:34:14 +0200 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2025-10-22 23:34:14 +0200 |
| commit | 281326b9b7eb6561526f02ff37eab9c39aa83b58 (patch) | |
| tree | e97e1bd1c1ca95d7775a988af3a65a90e50fa94e /Nominal/Instances.lean | |
| parent | b1a5137ed3f2d7810a1670d2e3888e8a87d89b02 (diff) | |
always require infinite, countable, equality-decidable atoms
Diffstat (limited to 'Nominal/Instances.lean')
| -rw-r--r-- | Nominal/Instances.lean | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Nominal/Instances.lean b/Nominal/Instances.lean index 057a0de..dcf079f 100644 --- a/Nominal/Instances.lean +++ b/Nominal/Instances.lean @@ -8,7 +8,7 @@ import Nominal.Support This file contains common instances of (FPerm ๐ธ)-sets and nominal sets. -/ -variable (๐ธ : Type) +variable (๐ธ : Type) [Infinite ๐ธ] [Countable ๐ธ] [DecidableEq ๐ธ] /-! ## Atoms @@ -25,7 +25,7 @@ instance : NominalSet ๐ธ ๐ธ where intro a; use {a} exact โจNominalSet.supp_atom' ๐ธ, Set.finite_singleton aโฉ -lemma NominalSet.supp_atom [Infinite ๐ธ] [DecidableEq ๐ธ] {a : ๐ธ} : supp ๐ธ a = {a} := by +lemma NominalSet.supp_atom {a : ๐ธ} : supp ๐ธ a = {a} := by ext b; constructor ยท apply support_subset_supp ๐ธ ยท exact NominalSet.supp_atom' ๐ธ @@ -90,7 +90,7 @@ section Products instance {X Y : Type} [PermSet ๐ธ X] [PermSet ๐ธ Y] : PermSet ๐ธ (X ร Y) where -variable {X Y : Type} [NominalSet ๐ธ X] [NominalSet ๐ธ Y] [Infinite ๐ธ] +variable {X Y : Type} [NominalSet ๐ธ X] [NominalSet ๐ธ Y] private lemma NominalSet.supp_product' {x : X} {y : Y} : PermSet.HasSupport ๐ธ (x, y) (supp ๐ธ x โช supp ๐ธ y) := by intro ฯ hฯ @@ -135,7 +135,7 @@ section Coproducts instance {X Y : Type} [PermSet ๐ธ X] [PermSet ๐ธ Y] : PermSet ๐ธ (X โ Y) where -variable {X Y : Type} [NominalSet ๐ธ X] [NominalSet ๐ธ Y] [Infinite ๐ธ] +variable {X Y : Type} [NominalSet ๐ธ X] [NominalSet ๐ธ Y] private lemma NominalSet.supp_coproductโ' {x : X} : PermSet.HasSupport ๐ธ (.inl x : X โ Y) (supp ๐ธ x) := by intro ฯ hฯ |