# HG changeset patch
# User desharna
# Date 1742066845 -3600
# Node ID f7c5a010115a71fb6db09bc6728efe6d0fe9af75
# Parent  919eb0e6793060ff001f8e8c2b8bbd319c6c7b82
added lemma left_unique_iff_Uniq

diff -r 919eb0e67930 -r f7c5a010115a NEWS
--- a/NEWS	Sat Mar 15 20:17:03 2025 +0100
+++ b/NEWS	Sat Mar 15 20:27:25 2025 +0100
@@ -28,6 +28,7 @@
       antisymp_equality[simp] ~> antisymp_on_equality[simp]
       transp_equality[simp] ~> transp_on_equality[simp]
   - Added lemmas.
+      left_unique_iff_Uniq
       reflp_on_refl_on_eq[pred_set_conv]
       symp_on_equality[simp]
 
diff -r 919eb0e67930 -r f7c5a010115a src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sat Mar 15 20:17:03 2025 +0100
+++ b/src/HOL/Relation.thy	Sat Mar 15 20:27:25 2025 +0100
@@ -835,6 +835,9 @@
 lemma left_uniqueD: "left_unique A \<Longrightarrow> A x z \<Longrightarrow> A y z \<Longrightarrow> x = y"
   unfolding left_unique_def by blast
 
+lemma left_unique_iff_Uniq: "left_unique r \<longleftrightarrow> (\<forall>y. \<exists>\<^sub>\<le>\<^sub>1x. r x y)"
+  unfolding Uniq_def left_unique_def by blast
+
 
 subsubsection \<open>Right uniqueness\<close>