diff options
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 |