From a8915795c109980285e11ed53d453987c0917069 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Tue, 2 Dec 2025 11:52:15 +0100 Subject: minor cleanup --- Nominal/Instances/Basic.lean | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'Nominal/Instances/Basic.lean') 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) := -- cgit v1.3.1