1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 13:20:17 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 13:21:34 2013 +0100
     1.3 @@ -17,6 +17,13 @@
     1.4    Norm_Arith
     1.5  begin
     1.6  
     1.7 +(* TODO: Move this to RComplete.thy -- would need to include Glb into RComplete *)
     1.8 +lemma real_isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::real)"
     1.9 +  apply (frule isGlb_isLb)
    1.10 +  apply (frule_tac x = y in isGlb_isLb)
    1.11 +  apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
    1.12 +  done
    1.13 +
    1.14  lemma countable_PiE: 
    1.15    "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"
    1.16    by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
    1.17 @@ -2321,13 +2328,6 @@
    1.18    shows "finite S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))"
    1.19    by (rule Inf_insert, rule finite_imp_bounded, simp)
    1.20  
    1.21 -(* TODO: Move this to RComplete.thy -- would need to include Glb into RComplete *)
    1.22 -lemma real_isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::real)"
    1.23 -  apply (frule isGlb_isLb)
    1.24 -  apply (frule_tac x = y in isGlb_isLb)
    1.25 -  apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
    1.26 -  done
    1.27 -
    1.28  subsection {* Compactness *}
    1.29  
    1.30  subsubsection{* Open-cover compactness *}