--- 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> {}"
--- 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
--- 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>
--- 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)