diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2026-01-12 17:07:26 +0100 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2026-01-12 17:07:26 +0100 |
| commit | c02833bceaa69c632285dde4742a91b332d41c6a (patch) | |
| tree | 3d02223d729601457167936f4913ecd76f566bcb /Nominal/NameRestriction/Finsupp.lean | |
| parent | 04d26f09a95b2f04a2ea055245826630dbd9c724 (diff) | |
cleanup
Diffstat (limited to 'Nominal/NameRestriction/Finsupp.lean')
| -rw-r--r-- | Nominal/NameRestriction/Finsupp.lean | 13 |
1 files changed, 13 insertions, 0 deletions
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 |