--- 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]
--- 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>