author hoelzl Tue, 05 Mar 2013 15:43:19 +0100 changeset 51348 011c97ba3b3d parent 51347 f8a00792fbc1 child 51349 166170c5f8a2
move lemma Inf to usage point
```--- 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"```