diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2025-10-27 21:58:56 +0100 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2025-10-27 21:58:56 +0100 |
| commit | b3f26f306945ec9e391140f1645012ba11decb40 (patch) | |
| tree | bae99d681301af5da7f4a4019d6c391ab68971b5 /Nominal/Equivariance.lean | |
| parent | 091fd832586627fbf31375fb5487d5e6fa6f7053 (diff) | |
quotient types as nominal sets
Diffstat (limited to 'Nominal/Equivariance.lean')
| -rw-r--r-- | Nominal/Equivariance.lean | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean index 189ca66..0fe9f91 100644 --- a/Nominal/Equivariance.lean +++ b/Nominal/Equivariance.lean @@ -31,6 +31,10 @@ def EquivariantSet (S : Set X) : Prop := def EquivariantRelation (R : Rel X Y) : Prop := ∀ (x : X) (y : Y) (π : FPerm 𝔸), R x y → R (π • x) (π • y) +/-- Extended setoid definition that also requires the relation to be equivariant. -/ +class EquivariantSetoid (X : Type) [PermSet 𝔸 X] extends Setoid X where + equivariant : EquivariantRelation 𝔸 r + /-- For equivariant sets, we even have "if and only if". -/ lemma equivariant_set_iff {S : Set X} : EquivariantSet 𝔸 S ↔ ∀ (x : X) (π : FPerm 𝔸), x ∈ S ↔ π • x ∈ S := by constructor |