diff options
| author | Hannes Schulze <contact@haschu.me> | 2026-04-14 16:04:44 +0200 |
|---|---|---|
| committer | Hannes Schulze <contact@haschu.me> | 2026-04-15 13:22:40 +0200 |
| commit | a5ff8efe5b5e314e0aa759318e5fb194e066f612 (patch) | |
| tree | 4d13dd84ac4ced2360a51799f0e5c846bd733872 /Nominal/Support.lean | |
| parent | 43942e78f4b3ed4cfca3b508f06161d0983c545e (diff) | |
update lean
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 |