# HG changeset patch
# User desharna
# Date 1742026666 -3600
# Node ID c61367ada9bbeac928b18bd1a1b8272e07c4e222
# Parent  365917fc6e313a31d13c234580b78947d5f2eb4c
added lemma single_valuedp_eq_right_unique

diff -r 365917fc6e31 -r c61367ada9bb NEWS
--- 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
diff -r 365917fc6e31 -r c61367ada9bb src/HOL/Transfer.thy
--- 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