# HG changeset patch
# User hoelzl
# Date 1362494593 -3600
# Node ID 763c6872bd10c5dc40b58e7e2e516a1f792a27e2
# Parent  8c10293e7ea71c71f117e8ec6a7023db4e12a55d
generalized isGlb_unique

diff -r 8c10293e7ea7 -r 763c6872bd10 src/HOL/Library/Glbs.thy
--- 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
diff -r 8c10293e7ea7 -r 763c6872bd10 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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)"