diff options
Diffstat (limited to 'Nominal/Support.lean')
| -rw-r--r-- | Nominal/Support.lean | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Nominal/Support.lean b/Nominal/Support.lean index 7888a68..fde20c7 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -79,7 +79,7 @@ lemma support_inter {x : X} {S T : Set ๐ธ} : HasSupport ๐ธ x S โ S.Finite simp) let m' := (S \ T).restrict m rw [Set.injOn_iff_injective, show (S \ T).restrict m = m' by rfl] at h_m_injective - obtain h_m_inv := Function.partialInv_of_injective h_m_injective + obtain h_m_inv := h_m_injective.isPartialInv have h_m_image : m '' (S \ T) โ (ฯ'.supp โช S โช T)แถ := Set.image_subset_iff.mpr h_m_preimage |