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