--- a/NEWS Fri Mar 14 18:13:56 2025 +0100
+++ b/NEWS Sat Mar 15 09:17:46 2025 +0100
@@ -52,6 +52,10 @@
- Added lemmas.
quotient_disj_strong
+* Theory "HOL.Transfer":
+ - Added lemmas.
+ single_valuedp_eq_right_unique
+
* Theory "HOL-Library.Multiset":
- Renamed lemmas. Minor INCOMPATIBILITY.
filter_image_mset ~> filter_mset_image_mset
--- a/src/HOL/Transfer.thy Fri Mar 14 18:13:56 2025 +0100
+++ b/src/HOL/Transfer.thy Sat Mar 15 09:17:46 2025 +0100
@@ -126,6 +126,9 @@
(\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and>
(\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
+lemma single_valuedp_eq_right_unique: "single_valuedp = right_unique"
+ by (rule ext) (simp add: single_valuedp_def right_unique_def)
+
lemma left_unique_iff: "left_unique R \<longleftrightarrow> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R x z)"
unfolding Uniq_def left_unique_def by force