# HG changeset patch
# User hoelzl
# Date 1362494599 -3600
# Node ID 011c97ba3b3df381093282a7d9f8a06e269e2db5
# Parent  f8a00792fbc1c874e81a7266ef07b6214f0c04ab
move lemma Inf to usage point

diff -r f8a00792fbc1 -r 011c97ba3b3d src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 05 15:43:18 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 05 15:43:19 2013 +0100
@@ -48,6 +48,11 @@
     and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x" "\<And>x. norm (f x) \<le> norm x * K"
   shows "bounded_linear f"
   unfolding bounded_linear_def additive_def bounded_linear_axioms_def using assms by auto
+
+lemma Inf: (* rename *)
+  fixes S :: "real set"
+  shows "S \<noteq> {} ==> (\<exists>b. b <=* S) ==> isGlb UNIV S (Inf S)"
+by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def) 
  
 lemma real_le_inf_subset:
   assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. b <=* s"
diff -r f8a00792fbc1 -r 011c97ba3b3d src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:18 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:19 2013 +0100
@@ -4967,11 +4967,6 @@
 
 text {* Hence some handy theorems on distance, diameter etc. of/from a set. *}
 
-
-lemma Inf:
-  fixes S :: "real set"
-  shows "S \<noteq> {} ==> (\<exists>b. b <=* S) ==> isGlb UNIV S (Inf S)"
-by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def) 
 lemma distance_attains_sup:
   assumes "compact s" "s \<noteq> {}"
   shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a y \<le> dist a x"