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>