--- a/src/HOL/Library/Glbs.thy Tue Mar 05 15:43:12 2013 +0100
+++ b/src/HOL/Library/Glbs.thy Tue Mar 05 15:43:13 2013 +0100
@@ -70,4 +70,10 @@
lemma isGlb_ubs: "isGlb R S x \<Longrightarrow> lbs R S *<= x"
unfolding lbs_def isGlb_def by (rule greatestPD2)
+lemma isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::'a::linorder)"
+ apply (frule isGlb_isLb)
+ apply (frule_tac x = y in isGlb_isLb)
+ apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
+ done
+
end
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Mar 05 15:43:12 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Mar 05 15:43:13 2013 +0100
@@ -28,12 +28,7 @@
lemma lim_subseq: "subseq r \<Longrightarrow> s ----> l \<Longrightarrow> (s o r) ----> l"
by (rule LIMSEQ_subseq_LIMSEQ)
-(* TODO: Move this to RComplete.thy -- would need to include Glb into RComplete *)
-lemma real_isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::real)"
- apply (frule isGlb_isLb)
- apply (frule_tac x = y in isGlb_isLb)
- apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
- done
+lemmas real_isGlb_unique = isGlb_unique[where 'a=real]
lemma countable_PiE:
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"