--- 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"
--- 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"