From c02833bceaa69c632285dde4742a91b332d41c6a Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Mon, 12 Jan 2026 17:07:26 +0100 Subject: cleanup --- Nominal/NameRestriction/Finsupp.lean | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'Nominal/NameRestriction/Finsupp.lean') diff --git a/Nominal/NameRestriction/Finsupp.lean b/Nominal/NameRestriction/Finsupp.lean index 3059bba..4311bee 100644 --- a/Nominal/NameRestriction/Finsupp.lean +++ b/Nominal/NameRestriction/Finsupp.lean @@ -64,6 +64,19 @@ instance {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] : PermSet 𝔸 (X → Y) abbrev FinsuppFunction (X Y : Type) [PermSet 𝔸 X] [PermSet 𝔸 Y] : Type := Finsupp 𝔸 (X → Y) +lemma FinsuppFunction.supp_image {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] (f : PermSet.FinsuppFunction 𝔸 X Y) : + ∀ x, PermSet.HasSupport 𝔸 (f.val x) (NominalSet.supp 𝔸 f ∪ NominalSet.supp 𝔸 x) := by + intro x π hπ + have hπ₁ : π ∈ PermSet.fix 𝔸 (NominalSet.supp 𝔸 f) := by + apply PermSet.fix_antitone_mem 𝔸 hπ; exact Set.subset_union_left + have hπ₂ : π ∈ PermSet.fix 𝔸 (NominalSet.supp 𝔸 x) := by + apply PermSet.fix_antitone_mem 𝔸 hπ; exact Set.subset_union_right + suffices (π • f).val (π • x) = f.val x by + simp at this + exact this + rw [show π • f = f from NominalSet.supp_is_support 𝔸 hπ₁] + rw [show π • x = x from NominalSet.supp_is_support 𝔸 hπ₂] + variable (X Y : Type) [NominalSet 𝔸 X] [NominalSet 𝔸 Y] namespace Finsupp -- cgit v1.3.1