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