# HG changeset patch
# User immler
# Date 1546864409 -3600
# Node ID 2be1baf40351a7b1f58455166e4271f12fdcb5cc
# Parent  63ee37c519a334c0951b81a6f9e618c6410d17ce
moved setdist to more appropriate places

diff -r 63ee37c519a3 -r 2be1baf40351 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Jan 07 13:16:33 2019 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Jan 07 13:33:29 2019 +0100
@@ -5283,6 +5283,13 @@
   apply fastforce
   done
 
+lemma setdist_closest_point:
+    "\<lbrakk>closed S; S \<noteq> {}\<rbrakk> \<Longrightarrow> setdist {a} S = dist a (closest_point S a)"
+  apply (rule setdist_unique)
+  using closest_point_le
+  apply (auto simp: closest_point_in_set)
+  done
+
 lemma closest_point_lipschitz:
   assumes "convex S"
     and "closed S" "S \<noteq> {}"
diff -r 63ee37c519a3 -r 2be1baf40351 src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Mon Jan 07 13:16:33 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Mon Jan 07 13:33:29 2019 +0100
@@ -3176,7 +3176,7 @@
   unfolding continuous_on_iff dist_norm by simp
 
 lemma continuous_on_closed_Collect_le:
-  fixes f g :: "'a::t2_space \<Rightarrow> real"
+  fixes f g :: "'a::topological_space \<Rightarrow> real"
   assumes f: "continuous_on s f" and g: "continuous_on s g" and s: "closed s"
   shows "closed {x \<in> s. f x \<le> g x}"
 proof -
@@ -3188,4 +3188,156 @@
   finally show ?thesis .
 qed
 
+lemma continuous_le_on_closure:
+  fixes a::real
+  assumes f: "continuous_on (closure s) f"
+      and x: "x \<in> closure(s)"
+      and xlo: "\<And>x. x \<in> s ==> f(x) \<le> a"
+    shows "f(x) \<le> a"
+  using image_closure_subset [OF f, where T=" {x. x \<le> a}" ] assms
+    continuous_on_closed_Collect_le[of "UNIV" "\<lambda>x. x" "\<lambda>x. a"]
+  by auto
+
+lemma continuous_ge_on_closure:
+  fixes a::real
+  assumes f: "continuous_on (closure s) f"
+      and x: "x \<in> closure(s)"
+      and xlo: "\<And>x. x \<in> s ==> f(x) \<ge> a"
+    shows "f(x) \<ge> a"
+  using image_closure_subset [OF f, where T=" {x. a \<le> x}"] assms
+    continuous_on_closed_Collect_le[of "UNIV" "\<lambda>x. a" "\<lambda>x. x"]
+  by auto
+
+
+subsection\<open>The infimum of the distance between two sets\<close>
+
+definition%important setdist :: "'a::metric_space set \<Rightarrow> 'a set \<Rightarrow> real" where
+  "setdist s t \<equiv>
+       (if s = {} \<or> t = {} then 0
+        else Inf {dist x y| x y. x \<in> s \<and> y \<in> t})"
+
+lemma setdist_empty1 [simp]: "setdist {} t = 0"
+  by (simp add: setdist_def)
+
+lemma setdist_empty2 [simp]: "setdist t {} = 0"
+  by (simp add: setdist_def)
+
+lemma setdist_pos_le [simp]: "0 \<le> setdist s t"
+  by (auto simp: setdist_def ex_in_conv [symmetric] intro: cInf_greatest)
+
+lemma le_setdistI:
+  assumes "s \<noteq> {}" "t \<noteq> {}" "\<And>x y. \<lbrakk>x \<in> s; y \<in> t\<rbrakk> \<Longrightarrow> d \<le> dist x y"
+    shows "d \<le> setdist s t"
+  using assms
+  by (auto simp: setdist_def Set.ex_in_conv [symmetric] intro: cInf_greatest)
+
+lemma setdist_le_dist: "\<lbrakk>x \<in> s; y \<in> t\<rbrakk> \<Longrightarrow> setdist s t \<le> dist x y"
+  unfolding setdist_def
+  by (auto intro!: bdd_belowI [where m=0] cInf_lower)
+
+lemma le_setdist_iff:
+        "d \<le> setdist s t \<longleftrightarrow>
+        (\<forall>x \<in> s. \<forall>y \<in> t. d \<le> dist x y) \<and> (s = {} \<or> t = {} \<longrightarrow> d \<le> 0)"
+  apply (cases "s = {} \<or> t = {}")
+  apply (force simp add: setdist_def)
+  apply (intro iffI conjI)
+  using setdist_le_dist apply fastforce
+  apply (auto simp: intro: le_setdistI)
+  done
+
+lemma setdist_ltE:
+  assumes "setdist s t < b" "s \<noteq> {}" "t \<noteq> {}"
+    obtains x y where "x \<in> s" "y \<in> t" "dist x y < b"
+using assms
+by (auto simp: not_le [symmetric] le_setdist_iff)
+
+lemma setdist_refl: "setdist s s = 0"
+  apply (cases "s = {}")
+  apply (force simp add: setdist_def)
+  apply (rule antisym [OF _ setdist_pos_le])
+  apply (metis all_not_in_conv dist_self setdist_le_dist)
+  done
+
+lemma setdist_sym: "setdist s t = setdist t s"
+  by (force simp: setdist_def dist_commute intro!: arg_cong [where f=Inf])
+
+lemma setdist_triangle: "setdist s t \<le> setdist s {a} + setdist {a} t"
+proof (cases "s = {} \<or> t = {}")
+  case True then show ?thesis
+    using setdist_pos_le by fastforce
+next
+  case False
+  have "\<And>x. x \<in> s \<Longrightarrow> setdist s t - dist x a \<le> setdist {a} t"
+    apply (rule le_setdistI, blast)
+    using False apply (fastforce intro: le_setdistI)
+    apply (simp add: algebra_simps)
+    apply (metis dist_commute dist_triangle3 order_trans [OF setdist_le_dist])
+    done
+  then have "setdist s t - setdist {a} t \<le> setdist s {a}"
+    using False by (fastforce intro: le_setdistI)
+  then show ?thesis
+    by (simp add: algebra_simps)
+qed
+
+lemma setdist_singletons [simp]: "setdist {x} {y} = dist x y"
+  by (simp add: setdist_def)
+
+lemma setdist_Lipschitz: "\<bar>setdist {x} s - setdist {y} s\<bar> \<le> dist x y"
+  apply (subst setdist_singletons [symmetric])
+  by (metis abs_diff_le_iff diff_le_eq setdist_triangle setdist_sym)
+
+lemma continuous_at_setdist [continuous_intros]: "continuous (at x) (\<lambda>y. (setdist {y} s))"
+  by (force simp: continuous_at_eps_delta dist_real_def intro: le_less_trans [OF setdist_Lipschitz])
+
+lemma continuous_on_setdist [continuous_intros]: "continuous_on t (\<lambda>y. (setdist {y} s))"
+  by (metis continuous_at_setdist continuous_at_imp_continuous_on)
+
+lemma uniformly_continuous_on_setdist: "uniformly_continuous_on t (\<lambda>y. (setdist {y} s))"
+  by (force simp: uniformly_continuous_on_def dist_real_def intro: le_less_trans [OF setdist_Lipschitz])
+
+lemma setdist_subset_right: "\<lbrakk>t \<noteq> {}; t \<subseteq> u\<rbrakk> \<Longrightarrow> setdist s u \<le> setdist s t"
+  apply (cases "s = {} \<or> u = {}", force)
+  apply (auto simp: setdist_def intro!: bdd_belowI [where m=0] cInf_superset_mono)
+  done
+
+lemma setdist_subset_left: "\<lbrakk>s \<noteq> {}; s \<subseteq> t\<rbrakk> \<Longrightarrow> setdist t u \<le> setdist s u"
+  by (metis setdist_subset_right setdist_sym)
+
+lemma setdist_closure_1 [simp]: "setdist (closure s) t = setdist s t"
+proof (cases "s = {} \<or> t = {}")
+  case True then show ?thesis by force
+next
+  case False
+  { fix y
+    assume "y \<in> t"
+    have "continuous_on (closure s) (\<lambda>a. dist a y)"
+      by (auto simp: continuous_intros dist_norm)
+    then have *: "\<And>x. x \<in> closure s \<Longrightarrow> setdist s t \<le> dist x y"
+      apply (rule continuous_ge_on_closure)
+      apply assumption
+      apply (blast intro: setdist_le_dist \<open>y \<in> t\<close> )
+      done
+  } note * = this
+  show ?thesis
+    apply (rule antisym)
+     using False closure_subset apply (blast intro: setdist_subset_left)
+    using False *
+    apply (force simp add: closure_eq_empty intro!: le_setdistI)
+    done
+qed
+
+lemma setdist_closure_2 [simp]: "setdist t (closure s) = setdist t s"
+by (metis setdist_closure_1 setdist_sym)
+
+lemma setdist_eq_0I: "\<lbrakk>x \<in> S; x \<in> T\<rbrakk> \<Longrightarrow> setdist S T = 0"
+  by (metis antisym dist_self setdist_le_dist setdist_pos_le)
+
+lemma setdist_unique:
+  "\<lbrakk>a \<in> S; b \<in> T; \<And>x y. x \<in> S \<and> y \<in> T ==> dist a b \<le> dist x y\<rbrakk>
+   \<Longrightarrow> setdist S T = dist a b"
+  by (force simp add: setdist_le_dist le_setdist_iff intro: antisym)
+
+lemma setdist_le_sing: "x \<in> S ==> setdist S T \<le> setdist {x} T"
+  using setdist_subset_left by auto
+
 end
\ No newline at end of file
diff -r 63ee37c519a3 -r 2be1baf40351 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Mon Jan 07 13:16:33 2019 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Mon Jan 07 13:33:29 2019 +0100
@@ -4681,243 +4681,6 @@
 apply simp
 done
 
-subsection\<open>The infimum of the distance between two sets\<close>
-
-definition%important setdist :: "'a::metric_space set \<Rightarrow> 'a set \<Rightarrow> real" where
-  "setdist s t \<equiv>
-       (if s = {} \<or> t = {} then 0
-        else Inf {dist x y| x y. x \<in> s \<and> y \<in> t})"
-
-lemma setdist_empty1 [simp]: "setdist {} t = 0"
-  by (simp add: setdist_def)
-
-lemma setdist_empty2 [simp]: "setdist t {} = 0"
-  by (simp add: setdist_def)
-
-lemma setdist_pos_le [simp]: "0 \<le> setdist s t"
-  by (auto simp: setdist_def ex_in_conv [symmetric] intro: cInf_greatest)
-
-lemma le_setdistI:
-  assumes "s \<noteq> {}" "t \<noteq> {}" "\<And>x y. \<lbrakk>x \<in> s; y \<in> t\<rbrakk> \<Longrightarrow> d \<le> dist x y"
-    shows "d \<le> setdist s t"
-  using assms
-  by (auto simp: setdist_def Set.ex_in_conv [symmetric] intro: cInf_greatest)
-
-lemma setdist_le_dist: "\<lbrakk>x \<in> s; y \<in> t\<rbrakk> \<Longrightarrow> setdist s t \<le> dist x y"
-  unfolding setdist_def
-  by (auto intro!: bdd_belowI [where m=0] cInf_lower)
-
-lemma le_setdist_iff:
-        "d \<le> setdist s t \<longleftrightarrow>
-        (\<forall>x \<in> s. \<forall>y \<in> t. d \<le> dist x y) \<and> (s = {} \<or> t = {} \<longrightarrow> d \<le> 0)"
-  apply (cases "s = {} \<or> t = {}")
-  apply (force simp add: setdist_def)
-  apply (intro iffI conjI)
-  using setdist_le_dist apply fastforce
-  apply (auto simp: intro: le_setdistI)
-  done
-
-lemma setdist_ltE:
-  assumes "setdist s t < b" "s \<noteq> {}" "t \<noteq> {}"
-    obtains x y where "x \<in> s" "y \<in> t" "dist x y < b"
-using assms
-by (auto simp: not_le [symmetric] le_setdist_iff)
-
-lemma setdist_refl: "setdist s s = 0"
-  apply (cases "s = {}")
-  apply (force simp add: setdist_def)
-  apply (rule antisym [OF _ setdist_pos_le])
-  apply (metis all_not_in_conv dist_self setdist_le_dist)
-  done
-
-lemma setdist_sym: "setdist s t = setdist t s"
-  by (force simp: setdist_def dist_commute intro!: arg_cong [where f=Inf])
-
-lemma setdist_triangle: "setdist s t \<le> setdist s {a} + setdist {a} t"
-proof (cases "s = {} \<or> t = {}")
-  case True then show ?thesis
-    using setdist_pos_le by fastforce
-next
-  case False
-  have "\<And>x. x \<in> s \<Longrightarrow> setdist s t - dist x a \<le> setdist {a} t"
-    apply (rule le_setdistI, blast)
-    using False apply (fastforce intro: le_setdistI)
-    apply (simp add: algebra_simps)
-    apply (metis dist_commute dist_triangle3 order_trans [OF setdist_le_dist])
-    done
-  then have "setdist s t - setdist {a} t \<le> setdist s {a}"
-    using False by (fastforce intro: le_setdistI)
-  then show ?thesis
-    by (simp add: algebra_simps)
-qed
-
-lemma setdist_singletons [simp]: "setdist {x} {y} = dist x y"
-  by (simp add: setdist_def)
-
-lemma setdist_Lipschitz: "\<bar>setdist {x} s - setdist {y} s\<bar> \<le> dist x y"
-  apply (subst setdist_singletons [symmetric])
-  by (metis abs_diff_le_iff diff_le_eq setdist_triangle setdist_sym)
-
-lemma continuous_at_setdist [continuous_intros]: "continuous (at x) (\<lambda>y. (setdist {y} s))"
-  by (force simp: continuous_at_eps_delta dist_real_def intro: le_less_trans [OF setdist_Lipschitz])
-
-lemma continuous_on_setdist [continuous_intros]: "continuous_on t (\<lambda>y. (setdist {y} s))"
-  by (metis continuous_at_setdist continuous_at_imp_continuous_on)
-
-lemma uniformly_continuous_on_setdist: "uniformly_continuous_on t (\<lambda>y. (setdist {y} s))"
-  by (force simp: uniformly_continuous_on_def dist_real_def intro: le_less_trans [OF setdist_Lipschitz])
-
-lemma setdist_subset_right: "\<lbrakk>t \<noteq> {}; t \<subseteq> u\<rbrakk> \<Longrightarrow> setdist s u \<le> setdist s t"
-  apply (cases "s = {} \<or> u = {}", force)
-  apply (auto simp: setdist_def intro!: bdd_belowI [where m=0] cInf_superset_mono)
-  done
-
-lemma setdist_subset_left: "\<lbrakk>s \<noteq> {}; s \<subseteq> t\<rbrakk> \<Longrightarrow> setdist t u \<le> setdist s u"
-  by (metis setdist_subset_right setdist_sym)
-
-lemma setdist_closure_1 [simp]: "setdist (closure s) t = setdist s t"
-proof (cases "s = {} \<or> t = {}")
-  case True then show ?thesis by force
-next
-  case False
-  { fix y
-    assume "y \<in> t"
-    have "continuous_on (closure s) (\<lambda>a. dist a y)"
-      by (auto simp: continuous_intros dist_norm)
-    then have *: "\<And>x. x \<in> closure s \<Longrightarrow> setdist s t \<le> dist x y"
-      apply (rule continuous_ge_on_closure)
-      apply assumption
-      apply (blast intro: setdist_le_dist \<open>y \<in> t\<close> )
-      done
-  } note * = this
-  show ?thesis
-    apply (rule antisym)
-     using False closure_subset apply (blast intro: setdist_subset_left)
-    using False *
-    apply (force simp add: closure_eq_empty intro!: le_setdistI)
-    done
-qed
-
-lemma setdist_closure_2 [simp]: "setdist t (closure s) = setdist t s"
-by (metis setdist_closure_1 setdist_sym)
-
-lemma setdist_compact_closed:
-  fixes S :: "'a::euclidean_space set"
-  assumes S: "compact S" and T: "closed T"
-      and "S \<noteq> {}" "T \<noteq> {}"
-    shows "\<exists>x \<in> S. \<exists>y \<in> T. dist x y = setdist S T"
-proof -
-  have "(\<Union>x\<in> S. \<Union>y \<in> T. {x - y}) \<noteq> {}"
-    using assms by blast
-  then have "\<exists>x \<in> S. \<exists>y \<in> T. dist x y \<le> setdist S T"
-    apply (rule distance_attains_inf [where a=0, OF compact_closed_differences [OF S T]])
-    apply (simp add: dist_norm le_setdist_iff)
-    apply blast
-    done
-  then show ?thesis
-    by (blast intro!: antisym [OF _ setdist_le_dist] )
-qed
-
-lemma setdist_closed_compact:
-  fixes S :: "'a::euclidean_space set"
-  assumes S: "closed S" and T: "compact T"
-      and "S \<noteq> {}" "T \<noteq> {}"
-    shows "\<exists>x \<in> S. \<exists>y \<in> T. dist x y = setdist S T"
-  using setdist_compact_closed [OF T S \<open>T \<noteq> {}\<close> \<open>S \<noteq> {}\<close>]
-  by (metis dist_commute setdist_sym)
-
-lemma setdist_eq_0I: "\<lbrakk>x \<in> S; x \<in> T\<rbrakk> \<Longrightarrow> setdist S T = 0"
-  by (metis antisym dist_self setdist_le_dist setdist_pos_le)
-
-lemma setdist_eq_0_compact_closed:
-  fixes S :: "'a::euclidean_space set"
-  assumes S: "compact S" and T: "closed T"
-    shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> S \<inter> T \<noteq> {}"
-  apply (cases "S = {} \<or> T = {}", force)
-  using setdist_compact_closed [OF S T]
-  apply (force intro: setdist_eq_0I )
-  done
-
-corollary setdist_gt_0_compact_closed:
-  fixes S :: "'a::euclidean_space set"
-  assumes S: "compact S" and T: "closed T"
-    shows "setdist S T > 0 \<longleftrightarrow> (S \<noteq> {} \<and> T \<noteq> {} \<and> S \<inter> T = {})"
-  using setdist_pos_le [of S T] setdist_eq_0_compact_closed [OF assms]
-  by linarith
-
-lemma setdist_eq_0_closed_compact:
-  fixes S :: "'a::euclidean_space set"
-  assumes S: "closed S" and T: "compact T"
-    shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> S \<inter> T \<noteq> {}"
-  using setdist_eq_0_compact_closed [OF T S]
-  by (metis Int_commute setdist_sym)
-
-lemma setdist_eq_0_bounded:
-  fixes S :: "'a::euclidean_space set"
-  assumes "bounded S \<or> bounded T"
-    shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> closure S \<inter> closure T \<noteq> {}"
-  apply (cases "S = {} \<or> T = {}", force)
-  using setdist_eq_0_compact_closed [of "closure S" "closure T"]
-        setdist_eq_0_closed_compact [of "closure S" "closure T"] assms
-  apply (force simp add:  bounded_closure compact_eq_bounded_closed)
-  done
-
-lemma setdist_unique:
-  "\<lbrakk>a \<in> S; b \<in> T; \<And>x y. x \<in> S \<and> y \<in> T ==> dist a b \<le> dist x y\<rbrakk>
-   \<Longrightarrow> setdist S T = dist a b"
-  by (force simp add: setdist_le_dist le_setdist_iff intro: antisym)
-
-lemma setdist_closest_point:
-    "\<lbrakk>closed S; S \<noteq> {}\<rbrakk> \<Longrightarrow> setdist {a} S = dist a (closest_point S a)"
-  apply (rule setdist_unique)
-  using closest_point_le
-  apply (auto simp: closest_point_in_set)
-  done
-
-lemma setdist_eq_0_sing_1:
-    fixes S :: "'a::euclidean_space set"
-    shows "setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> closure S"
-  by (auto simp: setdist_eq_0_bounded)
-
-lemma setdist_eq_0_sing_2:
-    fixes S :: "'a::euclidean_space set"
-    shows "setdist S {x} = 0 \<longleftrightarrow> S = {} \<or> x \<in> closure S"
-  by (auto simp: setdist_eq_0_bounded)
-
-lemma setdist_neq_0_sing_1:
-    fixes S :: "'a::euclidean_space set"
-    shows "\<lbrakk>setdist {x} S = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> S \<noteq> {} \<and> x \<notin> closure S"
-  by (auto simp: setdist_eq_0_sing_1)
-
-lemma setdist_neq_0_sing_2:
-    fixes S :: "'a::euclidean_space set"
-    shows "\<lbrakk>setdist S {x} = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> S \<noteq> {} \<and> x \<notin> closure S"
-  by (auto simp: setdist_eq_0_sing_2)
-
-lemma setdist_sing_in_set:
-    fixes S :: "'a::euclidean_space set"
-    shows "x \<in> S \<Longrightarrow> setdist {x} S = 0"
-  using closure_subset by (auto simp: setdist_eq_0_sing_1)
-
-lemma setdist_le_sing: "x \<in> S ==> setdist S T \<le> setdist {x} T"
-  using setdist_subset_left by auto
-
-lemma setdist_eq_0_closed:
-  fixes S :: "'a::euclidean_space set"
-  shows  "closed S \<Longrightarrow> (setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> S)"
-by (simp add: setdist_eq_0_sing_1)
-
-lemma setdist_eq_0_closedin:
-  fixes S :: "'a::euclidean_space set"
-  shows "\<lbrakk>closedin (subtopology euclidean U) S; x \<in> U\<rbrakk>
-         \<Longrightarrow> (setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> S)"
-  by (auto simp: closedin_limpt setdist_eq_0_sing_1 closure_def)
-
-lemma setdist_gt_0_closedin:
-  fixes S :: "'a::euclidean_space set"
-  shows "\<lbrakk>closedin (subtopology euclidean U) S; x \<in> U; S \<noteq> {}; x \<notin> S\<rbrakk>
-         \<Longrightarrow> setdist {x} S > 0"
-  using less_eq_real_def setdist_eq_0_closedin by fastforce
 
 subsection%unimportant\<open>Basic lemmas about hyperplanes and halfspaces\<close>
 
diff -r 63ee37c519a3 -r 2be1baf40351 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Jan 07 13:16:33 2019 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Jan 07 13:33:29 2019 +0100
@@ -1104,25 +1104,6 @@
   shows "closed {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i}"
   by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
 
-lemma continuous_le_on_closure:
-  fixes a::real
-  assumes f: "continuous_on (closure s) f"
-      and x: "x \<in> closure(s)"
-      and xlo: "\<And>x. x \<in> s ==> f(x) \<le> a"
-    shows "f(x) \<le> a"
-    using image_closure_subset [OF f]
-  using image_closure_subset [OF f] closed_halfspace_le [of "1::real" a] assms
-  by force
-
-lemma continuous_ge_on_closure:
-  fixes a::real
-  assumes f: "continuous_on (closure s) f"
-      and x: "x \<in> closure(s)"
-      and xlo: "\<And>x. x \<in> s ==> f(x) \<ge> a"
-    shows "f(x) \<ge> a"
-  using image_closure_subset [OF f] closed_halfspace_ge [of a "1::real"] assms
-  by force
-
 
 subsection%unimportant\<open>Some more convenient intermediate-value theorem formulations\<close>
 
@@ -2259,6 +2240,108 @@
 qed
 
 
+subsection \<open>Set Distance\<close>
+
+lemma setdist_compact_closed:
+  fixes S :: "'a::{heine_borel,real_normed_vector} set"
+  assumes S: "compact S" and T: "closed T"
+      and "S \<noteq> {}" "T \<noteq> {}"
+    shows "\<exists>x \<in> S. \<exists>y \<in> T. dist x y = setdist S T"
+proof -
+  have "(\<Union>x\<in> S. \<Union>y \<in> T. {x - y}) \<noteq> {}"
+    using assms by blast
+  then have "\<exists>x \<in> S. \<exists>y \<in> T. dist x y \<le> setdist S T"
+    apply (rule distance_attains_inf [where a=0, OF compact_closed_differences [OF S T]])
+    apply (simp add: dist_norm le_setdist_iff)
+    apply blast
+    done
+  then show ?thesis
+    by (blast intro!: antisym [OF _ setdist_le_dist] )
+qed
+
+lemma setdist_closed_compact:
+  fixes S :: "'a::{heine_borel,real_normed_vector} set"
+  assumes S: "closed S" and T: "compact T"
+      and "S \<noteq> {}" "T \<noteq> {}"
+    shows "\<exists>x \<in> S. \<exists>y \<in> T. dist x y = setdist S T"
+  using setdist_compact_closed [OF T S \<open>T \<noteq> {}\<close> \<open>S \<noteq> {}\<close>]
+  by (metis dist_commute setdist_sym)
+
+lemma setdist_eq_0_compact_closed:
+  fixes S :: "'a::{heine_borel,real_normed_vector} set"
+  assumes S: "compact S" and T: "closed T"
+    shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> S \<inter> T \<noteq> {}"
+  apply (cases "S = {} \<or> T = {}", force)
+  using setdist_compact_closed [OF S T]
+  apply (force intro: setdist_eq_0I )
+  done
+
+corollary setdist_gt_0_compact_closed:
+  fixes S :: "'a::{heine_borel,real_normed_vector} set"
+  assumes S: "compact S" and T: "closed T"
+    shows "setdist S T > 0 \<longleftrightarrow> (S \<noteq> {} \<and> T \<noteq> {} \<and> S \<inter> T = {})"
+  using setdist_pos_le [of S T] setdist_eq_0_compact_closed [OF assms]
+  by linarith
+
+lemma setdist_eq_0_closed_compact:
+  fixes S :: "'a::{heine_borel,real_normed_vector} set"
+  assumes S: "closed S" and T: "compact T"
+    shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> S \<inter> T \<noteq> {}"
+  using setdist_eq_0_compact_closed [OF T S]
+  by (metis Int_commute setdist_sym)
+
+lemma setdist_eq_0_bounded:
+  fixes S :: "'a::{heine_borel,real_normed_vector} set"
+  assumes "bounded S \<or> bounded T"
+    shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> closure S \<inter> closure T \<noteq> {}"
+  apply (cases "S = {} \<or> T = {}", force)
+  using setdist_eq_0_compact_closed [of "closure S" "closure T"]
+        setdist_eq_0_closed_compact [of "closure S" "closure T"] assms
+  apply (force simp add:  bounded_closure compact_eq_bounded_closed)
+  done
+
+lemma setdist_eq_0_sing_1:
+    fixes S :: "'a::{heine_borel,real_normed_vector} set"
+    shows "setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> closure S"
+  by (auto simp: setdist_eq_0_bounded)
+
+lemma setdist_eq_0_sing_2:
+    fixes S :: "'a::{heine_borel,real_normed_vector} set"
+    shows "setdist S {x} = 0 \<longleftrightarrow> S = {} \<or> x \<in> closure S"
+  by (auto simp: setdist_eq_0_bounded)
+
+lemma setdist_neq_0_sing_1:
+    fixes S :: "'a::{heine_borel,real_normed_vector} set"
+    shows "\<lbrakk>setdist {x} S = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> S \<noteq> {} \<and> x \<notin> closure S"
+  by (auto simp: setdist_eq_0_sing_1)
+
+lemma setdist_neq_0_sing_2:
+    fixes S :: "'a::{heine_borel,real_normed_vector} set"
+    shows "\<lbrakk>setdist S {x} = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> S \<noteq> {} \<and> x \<notin> closure S"
+  by (auto simp: setdist_eq_0_sing_2)
+
+lemma setdist_sing_in_set:
+    fixes S :: "'a::{heine_borel,real_normed_vector} set"
+    shows "x \<in> S \<Longrightarrow> setdist {x} S = 0"
+  using closure_subset by (auto simp: setdist_eq_0_sing_1)
+
+lemma setdist_eq_0_closed:
+  fixes S :: "'a::{heine_borel,real_normed_vector} set"
+  shows  "closed S \<Longrightarrow> (setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> S)"
+by (simp add: setdist_eq_0_sing_1)
+
+lemma setdist_eq_0_closedin:
+  fixes S :: "'a::{heine_borel,real_normed_vector} set"
+  shows "\<lbrakk>closedin (subtopology euclidean U) S; x \<in> U\<rbrakk>
+         \<Longrightarrow> (setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> S)"
+  by (auto simp: closedin_limpt setdist_eq_0_sing_1 closure_def)
+
+lemma setdist_gt_0_closedin:
+  fixes S :: "'a::{heine_borel,real_normed_vector} set"
+  shows "\<lbrakk>closedin (subtopology euclidean U) S; x \<in> U; S \<noteq> {}; x \<notin> S\<rbrakk>
+         \<Longrightarrow> setdist {x} S > 0"
+  using less_eq_real_def setdist_eq_0_closedin by fastforce
+
 no_notation
   eucl_less (infix "<e" 50)