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