# HG changeset patch
# User hoelzl
# Date 1358425294 -3600
# Node ID 1aa1a7991fd924f07dd7eaa6f866ba205bf1888f
# Parent  3690724028b182daf3667b69c61446c2633ec17e
move auxiliary lemma to top

diff -r 3690724028b1 -r 1aa1a7991fd9 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 13:20:17 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 13:21:34 2013 +0100
@@ -17,6 +17,13 @@
   Norm_Arith
 begin
 
+(* 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
+
 lemma countable_PiE: 
   "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"
   by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
@@ -2321,13 +2328,6 @@
   shows "finite S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))"
   by (rule Inf_insert, rule finite_imp_bounded, simp)
 
-(* 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
-
 subsection {* Compactness *}
 
 subsubsection{* Open-cover compactness *}