diff -r 0649ff183dcf -r 01c88cf514fc src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Tue May 02 11:09:18 2023 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue May 02 12:51:05 2023 +0100
@@ -481,6 +481,12 @@
   assume "X = {}" with lt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
 qed (intro cSup_eq_non_empty assms)
 
+lemma cSup_unique:
+  fixes b :: "'a :: {conditionally_complete_lattice, no_bot}"
+  assumes "\<And>c. (\<forall>x \<in> s. x \<le> c) \<longleftrightarrow> b \<le> c"
+  shows "Sup s = b"
+  by (metis assms cSup_eq order.refl)
+
 lemma cInf_eq:
   fixes a :: "'a :: {conditionally_complete_lattice, no_top}"
   assumes upper: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
@@ -490,6 +496,12 @@
   assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
 qed (intro cInf_eq_non_empty assms)
 
+lemma cInf_unique:
+  fixes b :: "'a :: {conditionally_complete_lattice, no_top}"
+  assumes "\<And>c. (\<forall>x \<in> s. x \<ge> c) \<longleftrightarrow> b \<ge> c"
+  shows "Inf s = b"
+  by (meson assms cInf_eq order.refl)
+
 class conditionally_complete_linorder = conditionally_complete_lattice + linorder
 begin