diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2025-12-02 11:52:15 +0100 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2025-12-02 11:52:55 +0100 |
| commit | a8915795c109980285e11ed53d453987c0917069 (patch) | |
| tree | 63a17d262814082f6f93e203395d3cd6a4c62316 /Nominal/Instances/Basic.lean | |
| parent | 732b74059139428115aadad9b29653351f000c8a (diff) | |
minor cleanup
Diffstat (limited to 'Nominal/Instances/Basic.lean')
| -rw-r--r-- | Nominal/Instances/Basic.lean | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean index dea5bcf..7f461ac 100644 --- a/Nominal/Instances/Basic.lean +++ b/Nominal/Instances/Basic.lean @@ -254,6 +254,13 @@ instance : PermSet 𝔸 (Quotient setoid.toSetoid) where lemma mk_equivariant : Function.Equivariant 𝔸 (Quotient.mk setoid.toSetoid) := by simp [Function.Equivariant] +lemma lift_equivariant + {Y : Type} [PermSet 𝔸 Y] (f : X → Y) (h : ∀ (a b : X), a ≈ b → f a = f b) : + Function.Equivariant 𝔸 f → Function.Equivariant 𝔸 (Quotient.lift f h) := by + intro hequi x π + obtain ⟨x', hx'⟩ := x.exists_rep + simp [← hx', hequi x' π] + variable {X : Type} [NominalSet 𝔸 X] {setoid : EquivariantSetoid 𝔸 X} instance : NominalSet 𝔸 (Quotient setoid.toSetoid) := |