author hoelzl Thu, 17 Jan 2013 13:21:34 +0100 changeset 50942 1aa1a7991fd9 parent 50941 3690724028b1 child 50943 88a00a1c7c2c
move auxiliary lemma to top
```--- 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 *}```