# HG changeset patch
# User immler
# Date 1546793689 -3600
# Node ID 42cc3609fedfb1bf572b4c68af8fa0f11ab7bc47
# Parent  10644973cddef9b89b9b3c941891e71b7453e093
moved some material from Connected.thy to more appropriate places

diff -r 10644973cdde -r 42cc3609fedf src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Sun Jan 06 16:27:52 2019 +0100
+++ b/src/HOL/Analysis/Connected.thy	Sun Jan 06 17:54:49 2019 +0100
@@ -10,342 +10,60 @@
     Topology_Euclidean_Space
 begin
 
-subsection%unimportant \<open>More properties of closed balls, spheres, etc\<close>
-
-lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"
-  apply (simp add: interior_def, safe)
-  apply (force simp: open_contains_cball)
-  apply (rule_tac x="ball x e" in exI)
-  apply (simp add: subset_trans [OF ball_subset_cball])
-  done
-
-lemma islimpt_ball:
-  fixes x y :: "'a::{real_normed_vector,perfect_space}"
-  shows "y islimpt ball x e \<longleftrightarrow> 0 < e \<and> y \<in> cball x e"
-  (is "?lhs \<longleftrightarrow> ?rhs")
-proof
-  show ?rhs if ?lhs
-  proof
-    {
-      assume "e \<le> 0"
-      then have *: "ball x e = {}"
-        using ball_eq_empty[of x e] by auto
-      have False using \<open>?lhs\<close>
-        unfolding * using islimpt_EMPTY[of y] by auto
-    }
-    then show "e > 0" by (metis not_less)
-    show "y \<in> cball x e"
-      using closed_cball[of x e] islimpt_subset[of y "ball x e" "cball x e"]
-        ball_subset_cball[of x e] \<open>?lhs\<close>
-      unfolding closed_limpt by auto
+subsection%unimportant\<open>Lemmas Combining Imports\<close>
+
+lemma isCont_indicator:
+  fixes x :: "'a::t2_space"
+  shows "isCont (indicator A :: 'a \<Rightarrow> real) x = (x \<notin> frontier A)"
+proof auto
+  fix x
+  assume cts_at: "isCont (indicator A :: 'a \<Rightarrow> real) x" and fr: "x \<in> frontier A"
+  with continuous_at_open have 1: "\<forall>V::real set. open V \<and> indicator A x \<in> V \<longrightarrow>
+    (\<exists>U::'a set. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> V))" by auto
+  show False
+  proof (cases "x \<in> A")
+    assume x: "x \<in> A"
+    hence "indicator A x \<in> ({0<..<2} :: real set)" by simp
+    hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({0<..<2} :: real set))"
+      using 1 open_greaterThanLessThan by blast
+    then guess U .. note U = this
+    hence "\<forall>y\<in>U. indicator A y > (0::real)"
+      unfolding greaterThanLessThan_def by auto
+    hence "U \<subseteq> A" using indicator_eq_0_iff by force
+    hence "x \<in> interior A" using U interiorI by auto
+    thus ?thesis using fr unfolding frontier_def by simp
+  next
+    assume x: "x \<notin> A"
+    hence "indicator A x \<in> ({-1<..<1} :: real set)" by simp
+    hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({-1<..<1} :: real set))"
+      using 1 open_greaterThanLessThan by blast
+    then guess U .. note U = this
+    hence "\<forall>y\<in>U. indicator A y < (1::real)"
+      unfolding greaterThanLessThan_def by auto
+    hence "U \<subseteq> -A" by auto
+    hence "x \<in> interior (-A)" using U interiorI by auto
+    thus ?thesis using fr interior_complement unfolding frontier_def by auto
   qed
-  show ?lhs if ?rhs
-  proof -
-    from that have "e > 0" by auto
-    {
-      fix d :: real
-      assume "d > 0"
-      have "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
-      proof (cases "d \<le> dist x y")
-        case True
-        then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
-        proof (cases "x = y")
-          case True
-          then have False
-            using \<open>d \<le> dist x y\<close> \<open>d>0\<close> by auto
-          then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
-            by auto
-        next
-          case False
-          have "dist x (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) =
-            norm (x - y + (d / (2 * norm (y - x))) *\<^sub>R (y - x))"
-            unfolding mem_cball mem_ball dist_norm diff_diff_eq2 diff_add_eq[symmetric]
-            by auto
-          also have "\<dots> = \<bar>- 1 + d / (2 * norm (x - y))\<bar> * norm (x - y)"
-            using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", symmetric, of "y - x"]
-            unfolding scaleR_minus_left scaleR_one
-            by (auto simp: norm_minus_commute)
-          also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
-            unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
-            unfolding distrib_right using \<open>x\<noteq>y\<close>  by auto
-          also have "\<dots> \<le> e - d/2" using \<open>d \<le> dist x y\<close> and \<open>d>0\<close> and \<open>?rhs\<close>
-            by (auto simp: dist_norm)
-          finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \<in> ball x e" using \<open>d>0\<close>
-            by auto
-          moreover
-          have "(d / (2*dist y x)) *\<^sub>R (y - x) \<noteq> 0"
-            using \<open>x\<noteq>y\<close>[unfolded dist_nz] \<open>d>0\<close> unfolding scaleR_eq_0_iff
-            by (auto simp: dist_commute)
-          moreover
-          have "dist (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) y < d"
-            unfolding dist_norm
-            apply simp
-            unfolding norm_minus_cancel
-            using \<open>d > 0\<close> \<open>x\<noteq>y\<close>[unfolded dist_nz] dist_commute[of x y]
-            unfolding dist_norm
-            apply auto
-            done
-          ultimately show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
-            apply (rule_tac x = "y - (d / (2*dist y x)) *\<^sub>R (y - x)" in bexI)
-            apply auto
-            done
-        qed
-      next
-        case False
-        then have "d > dist x y" by auto
-        show "\<exists>x' \<in> ball x e. x' \<noteq> y \<and> dist x' y < d"
-        proof (cases "x = y")
-          case True
-          obtain z where **: "z \<noteq> y" "dist z y < min e d"
-            using perfect_choose_dist[of "min e d" y]
-            using \<open>d > 0\<close> \<open>e>0\<close> by auto
-          show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
-            unfolding \<open>x = y\<close>
-            using \<open>z \<noteq> y\<close> **
-            apply (rule_tac x=z in bexI)
-            apply (auto simp: dist_commute)
-            done
-        next
-          case False
-          then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
-            using \<open>d>0\<close> \<open>d > dist x y\<close> \<open>?rhs\<close>
-            apply (rule_tac x=x in bexI, auto)
-            done
-        qed
-      qed
-    }
-    then show ?thesis
-      unfolding mem_cball islimpt_approachable mem_ball by auto
+next
+  assume nfr: "x \<notin> frontier A"
+  hence "x \<in> interior A \<or> x \<in> interior (-A)"
+    by (auto simp: frontier_def closure_interior)
+  thus "isCont ((indicator A)::'a \<Rightarrow> real) x"
+  proof
+    assume int: "x \<in> interior A"
+    then obtain U where U: "open U" "x \<in> U" "U \<subseteq> A" unfolding interior_def by auto
+    hence "\<forall>y\<in>U. indicator A y = (1::real)" unfolding indicator_def by auto
+    hence "continuous_on U (indicator A)" by (simp add: continuous_on_const indicator_eq_1_iff)
+    thus ?thesis using U continuous_on_eq_continuous_at by auto
+  next
+    assume ext: "x \<in> interior (-A)"
+    then obtain U where U: "open U" "x \<in> U" "U \<subseteq> -A" unfolding interior_def by auto
+    then have "continuous_on U (indicator A)"
+      using continuous_on_topological by (auto simp: subset_iff)
+    thus ?thesis using U continuous_on_eq_continuous_at by auto
   qed
 qed
 
-lemma closure_ball_lemma:
-  fixes x y :: "'a::real_normed_vector"
-  assumes "x \<noteq> y"
-  shows "y islimpt ball x (dist x y)"
-proof (rule islimptI)
-  fix T
-  assume "y \<in> T" "open T"
-  then obtain r where "0 < r" "\<forall>z. dist z y < r \<longrightarrow> z \<in> T"
-    unfolding open_dist by fast
-  (* choose point between x and y, within distance r of y. *)
-  define k where "k = min 1 (r / (2 * dist x y))"
-  define z where "z = y + scaleR k (x - y)"
-  have z_def2: "z = x + scaleR (1 - k) (y - x)"
-    unfolding z_def by (simp add: algebra_simps)
-  have "dist z y < r"
-    unfolding z_def k_def using \<open>0 < r\<close>
-    by (simp add: dist_norm min_def)
-  then have "z \<in> T"
-    using \<open>\<forall>z. dist z y < r \<longrightarrow> z \<in> T\<close> by simp
-  have "dist x z < dist x y"
-    unfolding z_def2 dist_norm
-    apply (simp add: norm_minus_commute)
-    apply (simp only: dist_norm [symmetric])
-    apply (subgoal_tac "\<bar>1 - k\<bar> * dist x y < 1 * dist x y", simp)
-    apply (rule mult_strict_right_mono)
-    apply (simp add: k_def \<open>0 < r\<close> \<open>x \<noteq> y\<close>)
-    apply (simp add: \<open>x \<noteq> y\<close>)
-    done
-  then have "z \<in> ball x (dist x y)"
-    by simp
-  have "z \<noteq> y"
-    unfolding z_def k_def using \<open>x \<noteq> y\<close> \<open>0 < r\<close>
-    by (simp add: min_def)
-  show "\<exists>z\<in>ball x (dist x y). z \<in> T \<and> z \<noteq> y"
-    using \<open>z \<in> ball x (dist x y)\<close> \<open>z \<in> T\<close> \<open>z \<noteq> y\<close>
-    by fast
-qed
-
-lemma at_within_ball_bot_iff:
-  fixes x y :: "'a::{real_normed_vector,perfect_space}"
-  shows "at x within ball y r = bot \<longleftrightarrow> (r=0 \<or> x \<notin> cball y r)"
-  unfolding trivial_limit_within 
-apply (auto simp add:trivial_limit_within islimpt_ball )
-by (metis le_less_trans less_eq_real_def zero_le_dist)
-
-lemma closure_ball [simp]:
-  fixes x :: "'a::real_normed_vector"
-  shows "0 < e \<Longrightarrow> closure (ball x e) = cball x e"
-  apply (rule equalityI)
-  apply (rule closure_minimal)
-  apply (rule ball_subset_cball)
-  apply (rule closed_cball)
-  apply (rule subsetI, rename_tac y)
-  apply (simp add: le_less [where 'a=real])
-  apply (erule disjE)
-  apply (rule subsetD [OF closure_subset], simp)
-  apply (simp add: closure_def, clarify)
-  apply (rule closure_ball_lemma)
-  apply simp
-  done
-
-(* In a trivial vector space, this fails for e = 0. *)
-lemma interior_cball [simp]:
-  fixes x :: "'a::{real_normed_vector, perfect_space}"
-  shows "interior (cball x e) = ball x e"
-proof (cases "e \<ge> 0")
-  case False note cs = this
-  from cs have null: "ball x e = {}"
-    using ball_empty[of e x] by auto
-  moreover
-  {
-    fix y
-    assume "y \<in> cball x e"
-    then have False
-      by (metis ball_eq_empty null cs dist_eq_0_iff dist_le_zero_iff empty_subsetI mem_cball subset_antisym subset_ball)
-  }
-  then have "cball x e = {}" by auto
-  then have "interior (cball x e) = {}"
-    using interior_empty by auto
-  ultimately show ?thesis by blast
-next
-  case True note cs = this
-  have "ball x e \<subseteq> cball x e"
-    using ball_subset_cball by auto
-  moreover
-  {
-    fix S y
-    assume as: "S \<subseteq> cball x e" "open S" "y\<in>S"
-    then obtain d where "d>0" and d: "\<forall>x'. dist x' y < d \<longrightarrow> x' \<in> S"
-      unfolding open_dist by blast
-    then obtain xa where xa_y: "xa \<noteq> y" and xa: "dist xa y < d"
-      using perfect_choose_dist [of d] by auto
-    have "xa \<in> S"
-      using d[THEN spec[where x = xa]]
-      using xa by (auto simp: dist_commute)
-    then have xa_cball: "xa \<in> cball x e"
-      using as(1) by auto
-    then have "y \<in> ball x e"
-    proof (cases "x = y")
-      case True
-      then have "e > 0" using cs order.order_iff_strict xa_cball xa_y by fastforce
-      then show "y \<in> ball x e"
-        using \<open>x = y \<close> by simp
-    next
-      case False
-      have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) y < d"
-        unfolding dist_norm
-        using \<open>d>0\<close> norm_ge_zero[of "y - x"] \<open>x \<noteq> y\<close> by auto
-      then have *: "y + (d / 2 / dist y x) *\<^sub>R (y - x) \<in> cball x e"
-        using d as(1)[unfolded subset_eq] by blast
-      have "y - x \<noteq> 0" using \<open>x \<noteq> y\<close> by auto
-      hence **:"d / (2 * norm (y - x)) > 0"
-        unfolding zero_less_norm_iff[symmetric] using \<open>d>0\<close> by auto
-      have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) x =
-        norm (y + (d / (2 * norm (y - x))) *\<^sub>R y - (d / (2 * norm (y - x))) *\<^sub>R x - x)"
-        by (auto simp: dist_norm algebra_simps)
-      also have "\<dots> = norm ((1 + d / (2 * norm (y - x))) *\<^sub>R (y - x))"
-        by (auto simp: algebra_simps)
-      also have "\<dots> = \<bar>1 + d / (2 * norm (y - x))\<bar> * norm (y - x)"
-        using ** by auto
-      also have "\<dots> = (dist y x) + d/2"
-        using ** by (auto simp: distrib_right dist_norm)
-      finally have "e \<ge> dist x y +d/2"
-        using *[unfolded mem_cball] by (auto simp: dist_commute)
-      then show "y \<in> ball x e"
-        unfolding mem_ball using \<open>d>0\<close> by auto
-    qed
-  }
-  then have "\<forall>S \<subseteq> cball x e. open S \<longrightarrow> S \<subseteq> ball x e"
-    by auto
-  ultimately show ?thesis
-    using interior_unique[of "ball x e" "cball x e"]
-    using open_ball[of x e]
-    by auto
-qed
-
-lemma interior_ball [simp]: "interior (ball x e) = ball x e"
-  by (simp add: interior_open)
-
-lemma frontier_ball [simp]:
-  fixes a :: "'a::real_normed_vector"
-  shows "0 < e \<Longrightarrow> frontier (ball a e) = sphere a e"
-  by (force simp: frontier_def)
-
-lemma frontier_cball [simp]:
-  fixes a :: "'a::{real_normed_vector, perfect_space}"
-  shows "frontier (cball a e) = sphere a e"
-  by (force simp: frontier_def)
-
-lemma cball_eq_empty [simp]: "cball x e = {} \<longleftrightarrow> e < 0"
-  apply (simp add: set_eq_iff not_le)
-  apply (metis zero_le_dist dist_self order_less_le_trans)
-  done
-
-lemma cball_empty [simp]: "e < 0 \<Longrightarrow> cball x e = {}"
-  by simp
-
-lemma cball_eq_sing:
-  fixes x :: "'a::{metric_space,perfect_space}"
-  shows "cball x e = {x} \<longleftrightarrow> e = 0"
-proof (rule linorder_cases)
-  assume e: "0 < e"
-  obtain a where "a \<noteq> x" "dist a x < e"
-    using perfect_choose_dist [OF e] by auto
-  then have "a \<noteq> x" "dist x a \<le> e"
-    by (auto simp: dist_commute)
-  with e show ?thesis by (auto simp: set_eq_iff)
-qed auto
-
-lemma cball_sing:
-  fixes x :: "'a::metric_space"
-  shows "e = 0 \<Longrightarrow> cball x e = {x}"
-  by (auto simp: set_eq_iff)
-
-lemma ball_divide_subset: "d \<ge> 1 \<Longrightarrow> ball x (e/d) \<subseteq> ball x e"
-  apply (cases "e \<le> 0")
-  apply (simp add: ball_empty divide_simps)
-  apply (rule subset_ball)
-  apply (simp add: divide_simps)
-  done
-
-lemma ball_divide_subset_numeral: "ball x (e / numeral w) \<subseteq> ball x e"
-  using ball_divide_subset one_le_numeral by blast
-
-lemma cball_divide_subset: "d \<ge> 1 \<Longrightarrow> cball x (e/d) \<subseteq> cball x e"
-  apply (cases "e < 0")
-  apply (simp add: divide_simps)
-  apply (rule subset_cball)
-  apply (metis div_by_1 frac_le not_le order_refl zero_less_one)
-  done
-
-lemma cball_divide_subset_numeral: "cball x (e / numeral w) \<subseteq> cball x e"
-  using cball_divide_subset one_le_numeral by blast
-
-lemma compact_cball[simp]:
-  fixes x :: "'a::heine_borel"
-  shows "compact (cball x e)"
-  using compact_eq_bounded_closed bounded_cball closed_cball
-  by blast
-
-lemma compact_frontier_bounded[intro]:
-  fixes S :: "'a::heine_borel set"
-  shows "bounded S \<Longrightarrow> compact (frontier S)"
-  unfolding frontier_def
-  using compact_eq_bounded_closed
-  by blast
-
-lemma compact_frontier[intro]:
-  fixes S :: "'a::heine_borel set"
-  shows "compact S \<Longrightarrow> compact (frontier S)"
-  using compact_eq_bounded_closed compact_frontier_bounded
-  by blast
-
-corollary compact_sphere [simp]:
-  fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
-  shows "compact (sphere a r)"
-using compact_frontier [of "cball a r"] by simp
-
-corollary bounded_sphere [simp]:
-  fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
-  shows "bounded (sphere a r)"
-by (simp add: compact_imp_bounded)
-
-corollary closed_sphere  [simp]:
-  fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
-  shows "closed (sphere a r)"
-by (simp add: compact_imp_closed)
 
 subsection%unimportant \<open>Connectedness\<close>
 
@@ -776,1325 +494,6 @@
   using closedin_connected_component componentsE by blast
 
 
-subsection \<open>Intersecting chains of compact sets and the Baire property\<close>
-
-proposition bounded_closed_chain:
-  fixes \<F> :: "'a::heine_borel set set"
-  assumes "B \<in> \<F>" "bounded B" and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> closed S" and "{} \<notin> \<F>"
-      and chain: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
-    shows "\<Inter>\<F> \<noteq> {}"
-proof -
-  have "B \<inter> \<Inter>\<F> \<noteq> {}"
-  proof (rule compact_imp_fip)
-    show "compact B" "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
-      by (simp_all add: assms compact_eq_bounded_closed)
-    show "\<lbrakk>finite \<G>; \<G> \<subseteq> \<F>\<rbrakk> \<Longrightarrow> B \<inter> \<Inter>\<G> \<noteq> {}" for \<G>
-    proof (induction \<G> rule: finite_induct)
-      case empty
-      with assms show ?case by force
-    next
-      case (insert U \<G>)
-      then have "U \<in> \<F>" and ne: "B \<inter> \<Inter>\<G> \<noteq> {}" by auto
-      then consider "B \<subseteq> U" | "U \<subseteq> B"
-          using \<open>B \<in> \<F>\<close> chain by blast
-        then show ?case
-        proof cases
-          case 1
-          then show ?thesis
-            using Int_left_commute ne by auto
-        next
-          case 2
-          have "U \<noteq> {}"
-            using \<open>U \<in> \<F>\<close> \<open>{} \<notin> \<F>\<close> by blast
-          moreover
-          have False if "\<And>x. x \<in> U \<Longrightarrow> \<exists>Y\<in>\<G>. x \<notin> Y"
-          proof -
-            have "\<And>x. x \<in> U \<Longrightarrow> \<exists>Y\<in>\<G>. Y \<subseteq> U"
-              by (metis chain contra_subsetD insert.prems insert_subset that)
-            then obtain Y where "Y \<in> \<G>" "Y \<subseteq> U"
-              by (metis all_not_in_conv \<open>U \<noteq> {}\<close>)
-            moreover obtain x where "x \<in> \<Inter>\<G>"
-              by (metis Int_emptyI ne)
-            ultimately show ?thesis
-              by (metis Inf_lower subset_eq that)
-          qed
-          with 2 show ?thesis
-            by blast
-        qed
-      qed
-  qed
-  then show ?thesis by blast
-qed
-
-corollary compact_chain:
-  fixes \<F> :: "'a::heine_borel set set"
-  assumes "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" "{} \<notin> \<F>"
-          "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
-    shows "\<Inter> \<F> \<noteq> {}"
-proof (cases "\<F> = {}")
-  case True
-  then show ?thesis by auto
-next
-  case False
-  show ?thesis
-    by (metis False all_not_in_conv assms compact_imp_bounded compact_imp_closed bounded_closed_chain)
-qed
-
-lemma compact_nest:
-  fixes F :: "'a::linorder \<Rightarrow> 'b::heine_borel set"
-  assumes F: "\<And>n. compact(F n)" "\<And>n. F n \<noteq> {}" and mono: "\<And>m n. m \<le> n \<Longrightarrow> F n \<subseteq> F m"
-  shows "\<Inter>range F \<noteq> {}"
-proof -
-  have *: "\<And>S T. S \<in> range F \<and> T \<in> range F \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
-    by (metis mono image_iff le_cases)
-  show ?thesis
-    apply (rule compact_chain [OF _ _ *])
-    using F apply (blast intro: dest: *)+
-    done
-qed
-
-text\<open>The Baire property of dense sets\<close>
-theorem Baire:
-  fixes S::"'a::{real_normed_vector,heine_borel} set"
-  assumes "closed S" "countable \<G>"
-      and ope: "\<And>T. T \<in> \<G> \<Longrightarrow> openin (subtopology euclidean S) T \<and> S \<subseteq> closure T"
- shows "S \<subseteq> closure(\<Inter>\<G>)"
-proof (cases "\<G> = {}")
-  case True
-  then show ?thesis
-    using closure_subset by auto
-next
-  let ?g = "from_nat_into \<G>"
-  case False
-  then have gin: "?g n \<in> \<G>" for n
-    by (simp add: from_nat_into)
-  show ?thesis
-  proof (clarsimp simp: closure_approachable)
-    fix x and e::real
-    assume "x \<in> S" "0 < e"
-    obtain TF where opeF: "\<And>n. openin (subtopology euclidean S) (TF n)"
-               and ne: "\<And>n. TF n \<noteq> {}"
-               and subg: "\<And>n. S \<inter> closure(TF n) \<subseteq> ?g n"
-               and subball: "\<And>n. closure(TF n) \<subseteq> ball x e"
-               and decr: "\<And>n. TF(Suc n) \<subseteq> TF n"
-    proof -
-      have *: "\<exists>Y. (openin (subtopology euclidean S) Y \<and> Y \<noteq> {} \<and>
-                   S \<inter> closure Y \<subseteq> ?g n \<and> closure Y \<subseteq> ball x e) \<and> Y \<subseteq> U"
-        if opeU: "openin (subtopology euclidean S) U" and "U \<noteq> {}" and cloU: "closure U \<subseteq> ball x e" for U n
-      proof -
-        obtain T where T: "open T" "U = T \<inter> S"
-          using \<open>openin (subtopology euclidean S) U\<close> by (auto simp: openin_subtopology)
-        with \<open>U \<noteq> {}\<close> have "T \<inter> closure (?g n) \<noteq> {}"
-          using gin ope by fastforce
-        then have "T \<inter> ?g n \<noteq> {}"
-          using \<open>open T\<close> open_Int_closure_eq_empty by blast
-        then obtain y where "y \<in> U" "y \<in> ?g n"
-          using T ope [of "?g n", OF gin] by (blast dest:  openin_imp_subset)
-        moreover have "openin (subtopology euclidean S) (U \<inter> ?g n)"
-          using gin ope opeU by blast
-        ultimately obtain d where U: "U \<inter> ?g n \<subseteq> S" and "d > 0" and d: "ball y d \<inter> S \<subseteq> U \<inter> ?g n"
-          by (force simp: openin_contains_ball)
-        show ?thesis
-        proof (intro exI conjI)
-          show "openin (subtopology euclidean S) (S \<inter> ball y (d/2))"
-            by (simp add: openin_open_Int)
-          show "S \<inter> ball y (d/2) \<noteq> {}"
-            using \<open>0 < d\<close> \<open>y \<in> U\<close> opeU openin_imp_subset by fastforce
-          have "S \<inter> closure (S \<inter> ball y (d/2)) \<subseteq> S \<inter> closure (ball y (d/2))"
-            using closure_mono by blast
-          also have "... \<subseteq> ?g n"
-            using \<open>d > 0\<close> d by force
-          finally show "S \<inter> closure (S \<inter> ball y (d/2)) \<subseteq> ?g n" .
-          have "closure (S \<inter> ball y (d/2)) \<subseteq> S \<inter> ball y d"
-          proof -
-            have "closure (ball y (d/2)) \<subseteq> ball y d"
-              using \<open>d > 0\<close> by auto
-            then have "closure (S \<inter> ball y (d/2)) \<subseteq> ball y d"
-              by (meson closure_mono inf.cobounded2 subset_trans)
-            then show ?thesis
-              by (simp add: \<open>closed S\<close> closure_minimal)
-          qed
-          also have "...  \<subseteq> ball x e"
-            using cloU closure_subset d by blast
-          finally show "closure (S \<inter> ball y (d/2)) \<subseteq> ball x e" .
-          show "S \<inter> ball y (d/2) \<subseteq> U"
-            using ball_divide_subset_numeral d by blast
-        qed
-      qed
-      let ?\<Phi> = "\<lambda>n X. openin (subtopology euclidean S) X \<and> X \<noteq> {} \<and>
-                      S \<inter> closure X \<subseteq> ?g n \<and> closure X \<subseteq> ball x e"
-      have "closure (S \<inter> ball x (e / 2)) \<subseteq> closure(ball x (e/2))"
-        by (simp add: closure_mono)
-      also have "...  \<subseteq> ball x e"
-        using \<open>e > 0\<close> by auto
-      finally have "closure (S \<inter> ball x (e / 2)) \<subseteq> ball x e" .
-      moreover have"openin (subtopology euclidean S) (S \<inter> ball x (e / 2))" "S \<inter> ball x (e / 2) \<noteq> {}"
-        using \<open>0 < e\<close> \<open>x \<in> S\<close> by auto
-      ultimately obtain Y where Y: "?\<Phi> 0 Y \<and> Y \<subseteq> S \<inter> ball x (e / 2)"
-            using * [of "S \<inter> ball x (e/2)" 0] by metis
-      show thesis
-      proof (rule exE [OF dependent_nat_choice [of ?\<Phi> "\<lambda>n X Y. Y \<subseteq> X"]])
-        show "\<exists>x. ?\<Phi> 0 x"
-          using Y by auto
-        show "\<exists>Y. ?\<Phi> (Suc n) Y \<and> Y \<subseteq> X" if "?\<Phi> n X" for X n
-          using that by (blast intro: *)
-      qed (use that in metis)
-    qed
-    have "(\<Inter>n. S \<inter> closure (TF n)) \<noteq> {}"
-    proof (rule compact_nest)
-      show "\<And>n. compact (S \<inter> closure (TF n))"
-        by (metis closed_closure subball bounded_subset_ballI compact_eq_bounded_closed closed_Int_compact [OF \<open>closed S\<close>])
-      show "\<And>n. S \<inter> closure (TF n) \<noteq> {}"
-        by (metis Int_absorb1 opeF \<open>closed S\<close> closure_eq_empty closure_minimal ne openin_imp_subset)
-      show "\<And>m n. m \<le> n \<Longrightarrow> S \<inter> closure (TF n) \<subseteq> S \<inter> closure (TF m)"
-        by (meson closure_mono decr dual_order.refl inf_mono lift_Suc_antimono_le)
-    qed
-    moreover have "(\<Inter>n. S \<inter> closure (TF n)) \<subseteq> {y \<in> \<Inter>\<G>. dist y x < e}"
-    proof (clarsimp, intro conjI)
-      fix y
-      assume "y \<in> S" and y: "\<forall>n. y \<in> closure (TF n)"
-      then show "\<forall>T\<in>\<G>. y \<in> T"
-        by (metis Int_iff from_nat_into_surj [OF \<open>countable \<G>\<close>] set_mp subg)
-      show "dist y x < e"
-        by (metis y dist_commute mem_ball subball subsetCE)
-    qed
-    ultimately show "\<exists>y \<in> \<Inter>\<G>. dist y x < e"
-      by auto
-  qed
-qed
-
-subsection%unimportant \<open>Some theorems on sups and infs using the notion "bounded"\<close>
-
-lemma bounded_real: "bounded (S::real set) \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. \<bar>x\<bar> \<le> a)"
-  by (simp add: bounded_iff)
-
-lemma bounded_imp_bdd_above: "bounded S \<Longrightarrow> bdd_above (S :: real set)"
-  by (auto simp: bounded_def bdd_above_def dist_real_def)
-     (metis abs_le_D1 abs_minus_commute diff_le_eq)
-
-lemma bounded_imp_bdd_below: "bounded S \<Longrightarrow> bdd_below (S :: real set)"
-  by (auto simp: bounded_def bdd_below_def dist_real_def)
-     (metis abs_le_D1 add.commute diff_le_eq)
-
-lemma bounded_inner_imp_bdd_above:
-  assumes "bounded s"
-    shows "bdd_above ((\<lambda>x. x \<bullet> a) ` s)"
-by (simp add: assms bounded_imp_bdd_above bounded_linear_image bounded_linear_inner_left)
-
-lemma bounded_inner_imp_bdd_below:
-  assumes "bounded s"
-    shows "bdd_below ((\<lambda>x. x \<bullet> a) ` s)"
-by (simp add: assms bounded_imp_bdd_below bounded_linear_image bounded_linear_inner_left)
-
-lemma bounded_has_Sup:
-  fixes S :: "real set"
-  assumes "bounded S"
-    and "S \<noteq> {}"
-  shows "\<forall>x\<in>S. x \<le> Sup S"
-    and "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b"
-proof
-  show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b"
-    using assms by (metis cSup_least)
-qed (metis cSup_upper assms(1) bounded_imp_bdd_above)
-
-lemma Sup_insert:
-  fixes S :: "real set"
-  shows "bounded S \<Longrightarrow> Sup (insert x S) = (if S = {} then x else max x (Sup S))"
-  by (auto simp: bounded_imp_bdd_above sup_max cSup_insert_If)
-
-lemma Sup_insert_finite:
-  fixes S :: "'a::conditionally_complete_linorder set"
-  shows "finite S \<Longrightarrow> Sup (insert x S) = (if S = {} then x else max x (Sup S))"
-by (simp add: cSup_insert sup_max)
-
-lemma bounded_has_Inf:
-  fixes S :: "real set"
-  assumes "bounded S"
-    and "S \<noteq> {}"
-  shows "\<forall>x\<in>S. x \<ge> Inf S"
-    and "\<forall>b. (\<forall>x\<in>S. x \<ge> b) \<longrightarrow> Inf S \<ge> b"
-proof
-  show "\<forall>b. (\<forall>x\<in>S. x \<ge> b) \<longrightarrow> Inf S \<ge> b"
-    using assms by (metis cInf_greatest)
-qed (metis cInf_lower assms(1) bounded_imp_bdd_below)
-
-lemma Inf_insert:
-  fixes S :: "real set"
-  shows "bounded S \<Longrightarrow> Inf (insert x S) = (if S = {} then x else min x (Inf S))"
-  by (auto simp: bounded_imp_bdd_below inf_min cInf_insert_If)
-
-lemma Inf_insert_finite:
-  fixes S :: "'a::conditionally_complete_linorder set"
-  shows "finite S \<Longrightarrow> Inf (insert x S) = (if S = {} then x else min x (Inf S))"
-by (simp add: cInf_eq_Min)
-
-lemma finite_imp_less_Inf:
-  fixes a :: "'a::conditionally_complete_linorder"
-  shows "\<lbrakk>finite X; x \<in> X; \<And>x. x\<in>X \<Longrightarrow> a < x\<rbrakk> \<Longrightarrow> a < Inf X"
-  by (induction X rule: finite_induct) (simp_all add: cInf_eq_Min Inf_insert_finite)
-
-lemma finite_less_Inf_iff:
-  fixes a :: "'a :: conditionally_complete_linorder"
-  shows "\<lbrakk>finite X; X \<noteq> {}\<rbrakk> \<Longrightarrow> a < Inf X \<longleftrightarrow> (\<forall>x \<in> X. a < x)"
-  by (auto simp: cInf_eq_Min)
-
-lemma finite_imp_Sup_less:
-  fixes a :: "'a::conditionally_complete_linorder"
-  shows "\<lbrakk>finite X; x \<in> X; \<And>x. x\<in>X \<Longrightarrow> a > x\<rbrakk> \<Longrightarrow> a > Sup X"
-  by (induction X rule: finite_induct) (simp_all add: cSup_eq_Max Sup_insert_finite)
-
-lemma finite_Sup_less_iff:
-  fixes a :: "'a :: conditionally_complete_linorder"
-  shows "\<lbrakk>finite X; X \<noteq> {}\<rbrakk> \<Longrightarrow> a > Sup X \<longleftrightarrow> (\<forall>x \<in> X. a > x)"
-  by (auto simp: cSup_eq_Max)
-
-proposition is_interval_compact:
-   "is_interval S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = cbox a b)"   (is "?lhs = ?rhs")
-proof (cases "S = {}")
-  case True
-  with empty_as_interval show ?thesis by auto
-next
-  case False
-  show ?thesis
-  proof
-    assume L: ?lhs
-    then have "is_interval S" "compact S" by auto
-    define a where "a \<equiv> \<Sum>i\<in>Basis. (INF x\<in>S. x \<bullet> i) *\<^sub>R i"
-    define b where "b \<equiv> \<Sum>i\<in>Basis. (SUP x\<in>S. x \<bullet> i) *\<^sub>R i"
-    have 1: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> (INF x\<in>S. x \<bullet> i) \<le> x \<bullet> i"
-      by (simp add: cInf_lower bounded_inner_imp_bdd_below compact_imp_bounded L)
-    have 2: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)"
-      by (simp add: cSup_upper bounded_inner_imp_bdd_above compact_imp_bounded L)
-    have 3: "x \<in> S" if inf: "\<And>i. i \<in> Basis \<Longrightarrow> (INF x\<in>S. x \<bullet> i) \<le> x \<bullet> i"
-                   and sup: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)" for x
-    proof (rule mem_box_componentwiseI [OF \<open>is_interval S\<close>])
-      fix i::'a
-      assume i: "i \<in> Basis"
-      have cont: "continuous_on S (\<lambda>x. x \<bullet> i)"
-        by (intro continuous_intros)
-      obtain a where "a \<in> S" and a: "\<And>y. y\<in>S \<Longrightarrow> a \<bullet> i \<le> y \<bullet> i"
-        using continuous_attains_inf [OF \<open>compact S\<close> False cont] by blast
-      obtain b where "b \<in> S" and b: "\<And>y. y\<in>S \<Longrightarrow> y \<bullet> i \<le> b \<bullet> i"
-        using continuous_attains_sup [OF \<open>compact S\<close> False cont] by blast
-      have "a \<bullet> i \<le> (INF x\<in>S. x \<bullet> i)"
-        by (simp add: False a cINF_greatest)
-      also have "\<dots> \<le> x \<bullet> i"
-        by (simp add: i inf)
-      finally have ai: "a \<bullet> i \<le> x \<bullet> i" .
-      have "x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)"
-        by (simp add: i sup)
-      also have "(SUP x\<in>S. x \<bullet> i) \<le> b \<bullet> i"
-        by (simp add: False b cSUP_least)
-      finally have bi: "x \<bullet> i \<le> b \<bullet> i" .
-      show "x \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` S"
-        apply (rule_tac x="\<Sum>j\<in>Basis. (if j = i then x \<bullet> i else a \<bullet> j) *\<^sub>R j" in image_eqI)
-        apply (simp add: i)
-        apply (rule mem_is_intervalI [OF \<open>is_interval S\<close> \<open>a \<in> S\<close> \<open>b \<in> S\<close>])
-        using i ai bi apply force
-        done
-    qed
-    have "S = cbox a b"
-      by (auto simp: a_def b_def mem_box intro: 1 2 3)
-    then show ?rhs
-      by blast
-  next
-    assume R: ?rhs
-    then show ?lhs
-      using compact_cbox is_interval_cbox by blast
-  qed
-qed
-
-text \<open>Hence some handy theorems on distance, diameter etc. of/from a set.\<close>
-
-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"
-proof (rule continuous_attains_sup [OF assms])
-  {
-    fix x
-    assume "x\<in>s"
-    have "(dist a \<longlongrightarrow> dist a x) (at x within s)"
-      by (intro tendsto_dist tendsto_const tendsto_ident_at)
-  }
-  then show "continuous_on s (dist a)"
-    unfolding continuous_on ..
-qed
-
-text \<open>For \emph{minimal} distance, we only need closure, not compactness.\<close>
-
-lemma distance_attains_inf:
-  fixes a :: "'a::heine_borel"
-  assumes "closed s" and "s \<noteq> {}"
-  obtains x where "x\<in>s" "\<And>y. y \<in> s \<Longrightarrow> dist a x \<le> dist a y"
-proof -
-  from assms obtain b where "b \<in> s" by auto
-  let ?B = "s \<inter> cball a (dist b a)"
-  have "?B \<noteq> {}" using \<open>b \<in> s\<close>
-    by (auto simp: dist_commute)
-  moreover have "continuous_on ?B (dist a)"
-    by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)
-  moreover have "compact ?B"
-    by (intro closed_Int_compact \<open>closed s\<close> compact_cball)
-  ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"
-    by (metis continuous_attains_inf)
-  with that show ?thesis by fastforce
-qed
-
-
-subsection%unimportant\<open>Relations among convergence and absolute convergence for power series\<close>
-
-lemma summable_imp_bounded:
-  fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
-  shows "summable f \<Longrightarrow> bounded (range f)"
-by (frule summable_LIMSEQ_zero) (simp add: convergent_imp_bounded)
-
-lemma summable_imp_sums_bounded:
-   "summable f \<Longrightarrow> bounded (range (\<lambda>n. sum f {..<n}))"
-by (auto simp: summable_def sums_def dest: convergent_imp_bounded)
-
-lemma power_series_conv_imp_absconv_weak:
-  fixes a:: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}" and w :: 'a
-  assumes sum: "summable (\<lambda>n. a n * z ^ n)" and no: "norm w < norm z"
-    shows "summable (\<lambda>n. of_real(norm(a n)) * w ^ n)"
-proof -
-  obtain M where M: "\<And>x. norm (a x * z ^ x) \<le> M"
-    using summable_imp_bounded [OF sum] by (force simp: bounded_iff)
-  then have *: "summable (\<lambda>n. norm (a n) * norm w ^ n)"
-    by (rule_tac M=M in Abel_lemma) (auto simp: norm_mult norm_power intro: no)
-  show ?thesis
-    apply (rule series_comparison_complex [of "(\<lambda>n. of_real(norm(a n) * norm w ^ n))"])
-    apply (simp only: summable_complex_of_real *)
-    apply (auto simp: norm_mult norm_power)
-    done
-qed
-
-subsection%unimportant \<open>Bounded closed nest property (proof does not use Heine-Borel)\<close>
-
-lemma bounded_closed_nest:
-  fixes S :: "nat \<Rightarrow> ('a::heine_borel) set"
-  assumes "\<And>n. closed (S n)"
-      and "\<And>n. S n \<noteq> {}"
-      and "\<And>m n. m \<le> n \<Longrightarrow> S n \<subseteq> S m"
-      and "bounded (S 0)"
-  obtains a where "\<And>n. a \<in> S n"
-proof -
-  from assms(2) obtain x where x: "\<forall>n. x n \<in> S n"
-    using choice[of "\<lambda>n x. x \<in> S n"] by auto
-  from assms(4,1) have "seq_compact (S 0)"
-    by (simp add: bounded_closed_imp_seq_compact)
-  then obtain l r where lr: "l \<in> S 0" "strict_mono r" "(x \<circ> r) \<longlonglongrightarrow> l"
-    using x and assms(3) unfolding seq_compact_def by blast
-  have "\<forall>n. l \<in> S n"
-  proof
-    fix n :: nat
-    have "closed (S n)"
-      using assms(1) by simp
-    moreover have "\<forall>i. (x \<circ> r) i \<in> S i"
-      using x and assms(3) and lr(2) [THEN seq_suble] by auto
-    then have "\<forall>i. (x \<circ> r) (i + n) \<in> S n"
-      using assms(3) by (fast intro!: le_add2)
-    moreover have "(\<lambda>i. (x \<circ> r) (i + n)) \<longlonglongrightarrow> l"
-      using lr(3) by (rule LIMSEQ_ignore_initial_segment)
-    ultimately show "l \<in> S n"
-      by (rule closed_sequentially)
-  qed
-  then show ?thesis 
-    using that by blast
-qed
-
-text \<open>Decreasing case does not even need compactness, just completeness.\<close>
-
-lemma decreasing_closed_nest:
-  fixes S :: "nat \<Rightarrow> ('a::complete_space) set"
-  assumes "\<And>n. closed (S n)"
-          "\<And>n. S n \<noteq> {}"
-          "\<And>m n. m \<le> n \<Longrightarrow> S n \<subseteq> S m"
-          "\<And>e. e>0 \<Longrightarrow> \<exists>n. \<forall>x\<in>S n. \<forall>y\<in>S n. dist x y < e"
-  obtains a where "\<And>n. a \<in> S n"
-proof -
-  have "\<forall>n. \<exists>x. x \<in> S n"
-    using assms(2) by auto
-  then have "\<exists>t. \<forall>n. t n \<in> S n"
-    using choice[of "\<lambda>n x. x \<in> S n"] by auto
-  then obtain t where t: "\<forall>n. t n \<in> S n" by auto
-  {
-    fix e :: real
-    assume "e > 0"
-    then obtain N where N: "\<forall>x\<in>S N. \<forall>y\<in>S N. dist x y < e"
-      using assms(4) by blast
-    {
-      fix m n :: nat
-      assume "N \<le> m \<and> N \<le> n"
-      then have "t m \<in> S N" "t n \<in> S N"
-        using assms(3) t unfolding  subset_eq t by blast+
-      then have "dist (t m) (t n) < e"
-        using N by auto
-    }
-    then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (t m) (t n) < e"
-      by auto
-  }
-  then have "Cauchy t"
-    unfolding cauchy_def by auto
-  then obtain l where l:"(t \<longlongrightarrow> l) sequentially"
-    using complete_UNIV unfolding complete_def by auto
-  { fix n :: nat
-    { fix e :: real
-      assume "e > 0"
-      then obtain N :: nat where N: "\<forall>n\<ge>N. dist (t n) l < e"
-        using l[unfolded lim_sequentially] by auto
-      have "t (max n N) \<in> S n"
-        by (meson assms(3) contra_subsetD max.cobounded1 t)
-      then have "\<exists>y\<in>S n. dist y l < e"
-        using N max.cobounded2 by blast
-    }
-    then have "l \<in> S n"
-      using closed_approachable[of "S n" l] assms(1) by auto
-  }
-  then show ?thesis
-    using that by blast
-qed
-
-text \<open>Strengthen it to the intersection actually being a singleton.\<close>
-
-lemma decreasing_closed_nest_sing:
-  fixes S :: "nat \<Rightarrow> 'a::complete_space set"
-  assumes "\<And>n. closed(S n)"
-          "\<And>n. S n \<noteq> {}"
-          "\<And>m n. m \<le> n \<Longrightarrow> S n \<subseteq> S m"
-          "\<And>e. e>0 \<Longrightarrow> \<exists>n. \<forall>x \<in> (S n). \<forall> y\<in>(S n). dist x y < e"
-  shows "\<exists>a. \<Inter>(range S) = {a}"
-proof -
-  obtain a where a: "\<forall>n. a \<in> S n"
-    using decreasing_closed_nest[of S] using assms by auto
-  { fix b
-    assume b: "b \<in> \<Inter>(range S)"
-    { fix e :: real
-      assume "e > 0"
-      then have "dist a b < e"
-        using assms(4) and b and a by blast
-    }
-    then have "dist a b = 0"
-      by (metis dist_eq_0_iff dist_nz less_le)
-  }
-  with a have "\<Inter>(range S) = {a}"
-    unfolding image_def by auto
-  then show ?thesis ..
-qed
-
-
-subsection \<open>Infimum Distance\<close>
-
-definition%important "infdist x A = (if A = {} then 0 else INF a\<in>A. dist x a)"
-
-lemma bdd_below_image_dist[intro, simp]: "bdd_below (dist x ` A)"
-  by (auto intro!: zero_le_dist)
-
-lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = (INF a\<in>A. dist x a)"
-  by (simp add: infdist_def)
-
-lemma infdist_nonneg: "0 \<le> infdist x A"
-  by (auto simp: infdist_def intro: cINF_greatest)
-
-lemma infdist_le: "a \<in> A \<Longrightarrow> infdist x A \<le> dist x a"
-  by (auto intro: cINF_lower simp add: infdist_def)
-
-lemma infdist_le2: "a \<in> A \<Longrightarrow> dist x a \<le> d \<Longrightarrow> infdist x A \<le> d"
-  by (auto intro!: cINF_lower2 simp add: infdist_def)
-
-lemma infdist_zero[simp]: "a \<in> A \<Longrightarrow> infdist a A = 0"
-  by (auto intro!: antisym infdist_nonneg infdist_le2)
-
-lemma infdist_triangle: "infdist x A \<le> infdist y A + dist x y"
-proof (cases "A = {}")
-  case True
-  then show ?thesis by (simp add: infdist_def)
-next
-  case False
-  then obtain a where "a \<in> A" by auto
-  have "infdist x A \<le> Inf {dist x y + dist y a |a. a \<in> A}"
-  proof (rule cInf_greatest)
-    from \<open>A \<noteq> {}\<close> show "{dist x y + dist y a |a. a \<in> A} \<noteq> {}"
-      by simp
-    fix d
-    assume "d \<in> {dist x y + dist y a |a. a \<in> A}"
-    then obtain a where d: "d = dist x y + dist y a" "a \<in> A"
-      by auto
-    show "infdist x A \<le> d"
-      unfolding infdist_notempty[OF \<open>A \<noteq> {}\<close>]
-    proof (rule cINF_lower2)
-      show "a \<in> A" by fact
-      show "dist x a \<le> d"
-        unfolding d by (rule dist_triangle)
-    qed simp
-  qed
-  also have "\<dots> = dist x y + infdist y A"
-  proof (rule cInf_eq, safe)
-    fix a
-    assume "a \<in> A"
-    then show "dist x y + infdist y A \<le> dist x y + dist y a"
-      by (auto intro: infdist_le)
-  next
-    fix i
-    assume inf: "\<And>d. d \<in> {dist x y + dist y a |a. a \<in> A} \<Longrightarrow> i \<le> d"
-    then have "i - dist x y \<le> infdist y A"
-      unfolding infdist_notempty[OF \<open>A \<noteq> {}\<close>] using \<open>a \<in> A\<close>
-      by (intro cINF_greatest) (auto simp: field_simps)
-    then show "i \<le> dist x y + infdist y A"
-      by simp
-  qed
-  finally show ?thesis by simp
-qed
-
-lemma in_closure_iff_infdist_zero:
-  assumes "A \<noteq> {}"
-  shows "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
-proof
-  assume "x \<in> closure A"
-  show "infdist x A = 0"
-  proof (rule ccontr)
-    assume "infdist x A \<noteq> 0"
-    with infdist_nonneg[of x A] have "infdist x A > 0"
-      by auto
-    then have "ball x (infdist x A) \<inter> closure A = {}"
-      apply auto
-      apply (metis \<open>x \<in> closure A\<close> closure_approachable dist_commute infdist_le not_less)
-      done
-    then have "x \<notin> closure A"
-      by (metis \<open>0 < infdist x A\<close> centre_in_ball disjoint_iff_not_equal)
-    then show False using \<open>x \<in> closure A\<close> by simp
-  qed
-next
-  assume x: "infdist x A = 0"
-  then obtain a where "a \<in> A"
-    by atomize_elim (metis all_not_in_conv assms)
-  show "x \<in> closure A"
-    unfolding closure_approachable
-    apply safe
-  proof (rule ccontr)
-    fix e :: real
-    assume "e > 0"
-    assume "\<not> (\<exists>y\<in>A. dist y x < e)"
-    then have "infdist x A \<ge> e" using \<open>a \<in> A\<close>
-      unfolding infdist_def
-      by (force simp: dist_commute intro: cINF_greatest)
-    with x \<open>e > 0\<close> show False by auto
-  qed
-qed
-
-lemma in_closed_iff_infdist_zero:
-  assumes "closed A" "A \<noteq> {}"
-  shows "x \<in> A \<longleftrightarrow> infdist x A = 0"
-proof -
-  have "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
-    by (rule in_closure_iff_infdist_zero) fact
-  with assms show ?thesis by simp
-qed
-
-lemma infdist_pos_not_in_closed:
-  assumes "closed S" "S \<noteq> {}" "x \<notin> S"
-  shows "infdist x S > 0"
-using in_closed_iff_infdist_zero[OF assms(1) assms(2), of x] assms(3) infdist_nonneg le_less by fastforce
-
-lemma
-  infdist_attains_inf:
-  fixes X::"'a::heine_borel set"
-  assumes "closed X"
-  assumes "X \<noteq> {}"
-  obtains x where "x \<in> X" "infdist y X = dist y x"
-proof -
-  have "bdd_below (dist y ` X)"
-    by auto
-  from distance_attains_inf[OF assms, of y]
-  obtain x where INF: "x \<in> X" "\<And>z. z \<in> X \<Longrightarrow> dist y x \<le> dist y z" by auto
-  have "infdist y X = dist y x"
-    by (auto simp: infdist_def assms
-      intro!: antisym cINF_lower[OF _ \<open>x \<in> X\<close>] cINF_greatest[OF assms(2) INF(2)])
-  with \<open>x \<in> X\<close> show ?thesis ..
-qed
-
-
-text \<open>Every metric space is a T4 space:\<close>
-
-instance metric_space \<subseteq> t4_space
-proof
-  fix S T::"'a set" assume H: "closed S" "closed T" "S \<inter> T = {}"
-  consider "S = {}" | "T = {}" | "S \<noteq> {} \<and> T \<noteq> {}" by auto
-  then show "\<exists>U V. open U \<and> open V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> U \<inter> V = {}"
-  proof (cases)
-    case 1
-    show ?thesis
-      apply (rule exI[of _ "{}"], rule exI[of _ UNIV]) using 1 by auto
-  next
-    case 2
-    show ?thesis
-      apply (rule exI[of _ UNIV], rule exI[of _ "{}"]) using 2 by auto
-  next
-    case 3
-    define U where "U = (\<Union>x\<in>S. ball x ((infdist x T)/2))"
-    have A: "open U" unfolding U_def by auto
-    have "infdist x T > 0" if "x \<in> S" for x
-      using H that 3 by (auto intro!: infdist_pos_not_in_closed)
-    then have B: "S \<subseteq> U" unfolding U_def by auto
-    define V where "V = (\<Union>x\<in>T. ball x ((infdist x S)/2))"
-    have C: "open V" unfolding V_def by auto
-    have "infdist x S > 0" if "x \<in> T" for x
-      using H that 3 by (auto intro!: infdist_pos_not_in_closed)
-    then have D: "T \<subseteq> V" unfolding V_def by auto
-
-    have "(ball x ((infdist x T)/2)) \<inter> (ball y ((infdist y S)/2)) = {}" if "x \<in> S" "y \<in> T" for x y
-    proof (auto)
-      fix z assume H: "dist x z * 2 < infdist x T" "dist y z * 2 < infdist y S"
-      have "2 * dist x y \<le> 2 * dist x z + 2 * dist y z"
-        using dist_triangle[of x y z] by (auto simp add: dist_commute)
-      also have "... < infdist x T + infdist y S"
-        using H by auto
-      finally have "dist x y < infdist x T \<or> dist x y < infdist y S"
-        by auto
-      then show False
-        using infdist_le[OF \<open>x \<in> S\<close>, of y] infdist_le[OF \<open>y \<in> T\<close>, of x] by (auto simp add: dist_commute)
-    qed
-    then have E: "U \<inter> V = {}"
-      unfolding U_def V_def by auto
-    show ?thesis
-      apply (rule exI[of _ U], rule exI[of _ V]) using A B C D E by auto
-  qed
-qed
-
-lemma tendsto_infdist [tendsto_intros]:
-  assumes f: "(f \<longlongrightarrow> l) F"
-  shows "((\<lambda>x. infdist (f x) A) \<longlongrightarrow> infdist l A) F"
-proof (rule tendstoI)
-  fix e ::real
-  assume "e > 0"
-  from tendstoD[OF f this]
-  show "eventually (\<lambda>x. dist (infdist (f x) A) (infdist l A) < e) F"
-  proof (eventually_elim)
-    fix x
-    from infdist_triangle[of l A "f x"] infdist_triangle[of "f x" A l]
-    have "dist (infdist (f x) A) (infdist l A) \<le> dist (f x) l"
-      by (simp add: dist_commute dist_real_def)
-    also assume "dist (f x) l < e"
-    finally show "dist (infdist (f x) A) (infdist l A) < e" .
-  qed
-qed
-
-lemma continuous_infdist[continuous_intros]:
-  assumes "continuous F f"
-  shows "continuous F (\<lambda>x. infdist (f x) A)"
-  using assms unfolding continuous_def by (rule tendsto_infdist)
-
-lemma compact_infdist_le:
-  fixes A::"'a::heine_borel set"
-  assumes "A \<noteq> {}"
-  assumes "compact A"
-  assumes "e > 0"
-  shows "compact {x. infdist x A \<le> e}"
-proof -
-  from continuous_closed_vimage[of "{0..e}" "\<lambda>x. infdist x A"]
-    continuous_infdist[OF continuous_ident, of _ UNIV A]
-  have "closed {x. infdist x A \<le> e}" by (auto simp: vimage_def infdist_nonneg)
-  moreover
-  from assms obtain x0 b where b: "\<And>x. x \<in> A \<Longrightarrow> dist x0 x \<le> b" "closed A"
-    by (auto simp: compact_eq_bounded_closed bounded_def)
-  {
-    fix y
-    assume le: "infdist y A \<le> e"
-    from infdist_attains_inf[OF \<open>closed A\<close> \<open>A \<noteq> {}\<close>, of y]
-    obtain z where z: "z \<in> A" "infdist y A = dist y z" by blast
-    have "dist x0 y \<le> dist y z + dist x0 z"
-      by (metis dist_commute dist_triangle)
-    also have "dist y z \<le> e" using le z by simp
-    also have "dist x0 z \<le> b" using b z by simp
-    finally have "dist x0 y \<le> b + e" by arith
-  } then
-  have "bounded {x. infdist x A \<le> e}"
-    by (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + e"])
-  ultimately show "compact {x. infdist x A \<le> e}"
-    by (simp add: compact_eq_bounded_closed)
-qed
-
-subsection%unimportant \<open>Equality of continuous functions on closure and related results\<close>
-
-lemma continuous_closedin_preimage_constant:
-  fixes f :: "_ \<Rightarrow> 'b::t1_space"
-  shows "continuous_on S f \<Longrightarrow> closedin (subtopology euclidean S) {x \<in> S. f x = a}"
-  using continuous_closedin_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)
-
-lemma continuous_closed_preimage_constant:
-  fixes f :: "_ \<Rightarrow> 'b::t1_space"
-  shows "continuous_on S f \<Longrightarrow> closed S \<Longrightarrow> closed {x \<in> S. f x = a}"
-  using continuous_closed_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)
-
-lemma continuous_constant_on_closure:
-  fixes f :: "_ \<Rightarrow> 'b::t1_space"
-  assumes "continuous_on (closure S) f"
-      and "\<And>x. x \<in> S \<Longrightarrow> f x = a"
-      and "x \<in> closure S"
-  shows "f x = a"
-    using continuous_closed_preimage_constant[of "closure S" f a]
-      assms closure_minimal[of S "{x \<in> closure S. f x = a}"] closure_subset
-    unfolding subset_eq
-    by auto
-
-lemma image_closure_subset:
-  assumes contf: "continuous_on (closure S) f"
-    and "closed T"
-    and "(f ` S) \<subseteq> T"
-  shows "f ` (closure S) \<subseteq> T"
-proof -
-  have "S \<subseteq> {x \<in> closure S. f x \<in> T}"
-    using assms(3) closure_subset by auto
-  moreover have "closed (closure S \<inter> f -` T)"
-    using continuous_closed_preimage[OF contf] \<open>closed T\<close> by auto
-  ultimately have "closure S = (closure S \<inter> f -` T)"
-    using closure_minimal[of S "(closure S \<inter> f -` T)"] by auto
-  then show ?thesis by auto
-qed
-
-lemma continuous_on_closure_norm_le:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
-  assumes "continuous_on (closure s) f"
-    and "\<forall>y \<in> s. norm(f y) \<le> b"
-    and "x \<in> (closure s)"
-  shows "norm (f x) \<le> b"
-proof -
-  have *: "f ` s \<subseteq> cball 0 b"
-    using assms(2)[unfolded mem_cball_0[symmetric]] by auto
-  show ?thesis
-    by (meson "*" assms(1) assms(3) closed_cball image_closure_subset image_subset_iff mem_cball_0)
-qed
-
-lemma isCont_indicator:
-  fixes x :: "'a::t2_space"
-  shows "isCont (indicator A :: 'a \<Rightarrow> real) x = (x \<notin> frontier A)"
-proof auto
-  fix x
-  assume cts_at: "isCont (indicator A :: 'a \<Rightarrow> real) x" and fr: "x \<in> frontier A"
-  with continuous_at_open have 1: "\<forall>V::real set. open V \<and> indicator A x \<in> V \<longrightarrow>
-    (\<exists>U::'a set. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> V))" by auto
-  show False
-  proof (cases "x \<in> A")
-    assume x: "x \<in> A"
-    hence "indicator A x \<in> ({0<..<2} :: real set)" by simp
-    hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({0<..<2} :: real set))"
-      using 1 open_greaterThanLessThan by blast
-    then guess U .. note U = this
-    hence "\<forall>y\<in>U. indicator A y > (0::real)"
-      unfolding greaterThanLessThan_def by auto
-    hence "U \<subseteq> A" using indicator_eq_0_iff by force
-    hence "x \<in> interior A" using U interiorI by auto
-    thus ?thesis using fr unfolding frontier_def by simp
-  next
-    assume x: "x \<notin> A"
-    hence "indicator A x \<in> ({-1<..<1} :: real set)" by simp
-    hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({-1<..<1} :: real set))"
-      using 1 open_greaterThanLessThan by blast
-    then guess U .. note U = this
-    hence "\<forall>y\<in>U. indicator A y < (1::real)"
-      unfolding greaterThanLessThan_def by auto
-    hence "U \<subseteq> -A" by auto
-    hence "x \<in> interior (-A)" using U interiorI by auto
-    thus ?thesis using fr interior_complement unfolding frontier_def by auto
-  qed
-next
-  assume nfr: "x \<notin> frontier A"
-  hence "x \<in> interior A \<or> x \<in> interior (-A)"
-    by (auto simp: frontier_def closure_interior)
-  thus "isCont ((indicator A)::'a \<Rightarrow> real) x"
-  proof
-    assume int: "x \<in> interior A"
-    then obtain U where U: "open U" "x \<in> U" "U \<subseteq> A" unfolding interior_def by auto
-    hence "\<forall>y\<in>U. indicator A y = (1::real)" unfolding indicator_def by auto
-    hence "continuous_on U (indicator A)" by (simp add: continuous_on_const indicator_eq_1_iff)
-    thus ?thesis using U continuous_on_eq_continuous_at by auto
-  next
-    assume ext: "x \<in> interior (-A)"
-    then obtain U where U: "open U" "x \<in> U" "U \<subseteq> -A" unfolding interior_def by auto
-    then have "continuous_on U (indicator A)"
-      using continuous_on_topological by (auto simp: subset_iff)
-    thus ?thesis using U continuous_on_eq_continuous_at by auto
-  qed
-qed
-
-subsection%unimportant \<open>A function constant on a set\<close>
-
-definition constant_on  (infixl "(constant'_on)" 50)
-  where "f constant_on A \<equiv> \<exists>y. \<forall>x\<in>A. f x = y"
-
-lemma constant_on_subset: "\<lbrakk>f constant_on A; B \<subseteq> A\<rbrakk> \<Longrightarrow> f constant_on B"
-  unfolding constant_on_def by blast
-
-lemma injective_not_constant:
-  fixes S :: "'a::{perfect_space} set"
-  shows "\<lbrakk>open S; inj_on f S; f constant_on S\<rbrakk> \<Longrightarrow> S = {}"
-unfolding constant_on_def
-by (metis equals0I inj_on_contraD islimpt_UNIV islimpt_def)
-
-lemma constant_on_closureI:
-  fixes f :: "_ \<Rightarrow> 'b::t1_space"
-  assumes cof: "f constant_on S" and contf: "continuous_on (closure S) f"
-    shows "f constant_on (closure S)"
-using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def
-by metis
-
-subsection%unimportant\<open>Relating linear images to open/closed/interior/closure\<close>
-
-proposition open_surjective_linear_image:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
-  assumes "open A" "linear f" "surj f"
-    shows "open(f ` A)"
-unfolding open_dist
-proof clarify
-  fix x
-  assume "x \<in> A"
-  have "bounded (inv f ` Basis)"
-    by (simp add: finite_imp_bounded)
-  with bounded_pos obtain B where "B > 0" and B: "\<And>x. x \<in> inv f ` Basis \<Longrightarrow> norm x \<le> B"
-    by metis
-  obtain e where "e > 0" and e: "\<And>z. dist z x < e \<Longrightarrow> z \<in> A"
-    by (metis open_dist \<open>x \<in> A\<close> \<open>open A\<close>)
-  define \<delta> where "\<delta> \<equiv> e / B / DIM('b)"
-  show "\<exists>e>0. \<forall>y. dist y (f x) < e \<longrightarrow> y \<in> f ` A"
-  proof (intro exI conjI)
-    show "\<delta> > 0"
-      using \<open>e > 0\<close> \<open>B > 0\<close>  by (simp add: \<delta>_def divide_simps)
-    have "y \<in> f ` A" if "dist y (f x) * (B * real DIM('b)) < e" for y
-    proof -
-      define u where "u \<equiv> y - f x"
-      show ?thesis
-      proof (rule image_eqI)
-        show "y = f (x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i))"
-          apply (simp add: linear_add linear_sum linear.scaleR \<open>linear f\<close> surj_f_inv_f \<open>surj f\<close>)
-          apply (simp add: euclidean_representation u_def)
-          done
-        have "dist (x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i)) x \<le> (\<Sum>i\<in>Basis. norm ((u \<bullet> i) *\<^sub>R inv f i))"
-          by (simp add: dist_norm sum_norm_le)
-        also have "... = (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar> * norm (inv f i))"
-          by simp
-        also have "... \<le> (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar>) * B"
-          by (simp add: B sum_distrib_right sum_mono mult_left_mono)
-        also have "... \<le> DIM('b) * dist y (f x) * B"
-          apply (rule mult_right_mono [OF sum_bounded_above])
-          using \<open>0 < B\<close> by (auto simp: Basis_le_norm dist_norm u_def)
-        also have "... < e"
-          by (metis mult.commute mult.left_commute that)
-        finally show "x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i) \<in> A"
-          by (rule e)
-      qed
-    qed
-    then show "\<forall>y. dist y (f x) < \<delta> \<longrightarrow> y \<in> f ` A"
-      using \<open>e > 0\<close> \<open>B > 0\<close>
-      by (auto simp: \<delta>_def divide_simps mult_less_0_iff)
-  qed
-qed
-
-corollary open_bijective_linear_image_eq:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes "linear f" "bij f"
-    shows "open(f ` A) \<longleftrightarrow> open A"
-proof
-  assume "open(f ` A)"
-  then have "open(f -` (f ` A))"
-    using assms by (force simp: linear_continuous_at linear_conv_bounded_linear continuous_open_vimage)
-  then show "open A"
-    by (simp add: assms bij_is_inj inj_vimage_image_eq)
-next
-  assume "open A"
-  then show "open(f ` A)"
-    by (simp add: assms bij_is_surj open_surjective_linear_image)
-qed
-
-corollary interior_bijective_linear_image:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes "linear f" "bij f"
-  shows "interior (f ` S) = f ` interior S"  (is "?lhs = ?rhs")
-proof safe
-  fix x
-  assume x: "x \<in> ?lhs"
-  then obtain T where "open T" and "x \<in> T" and "T \<subseteq> f ` S"
-    by (metis interiorE)
-  then show "x \<in> ?rhs"
-    by (metis (no_types, hide_lams) assms subsetD interior_maximal open_bijective_linear_image_eq subset_image_iff)
-next
-  fix x
-  assume x: "x \<in> interior S"
-  then show "f x \<in> interior (f ` S)"
-    by (meson assms imageI image_mono interiorI interior_subset open_bijective_linear_image_eq open_interior)
-qed
-
-lemma interior_injective_linear_image:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
-  assumes "linear f" "inj f"
-   shows "interior(f ` S) = f ` (interior S)"
-  by (simp add: linear_injective_imp_surjective assms bijI interior_bijective_linear_image)
-
-lemma interior_surjective_linear_image:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
-  assumes "linear f" "surj f"
-   shows "interior(f ` S) = f ` (interior S)"
-  by (simp add: assms interior_injective_linear_image linear_surjective_imp_injective)
-
-lemma interior_negations:
-  fixes S :: "'a::euclidean_space set"
-  shows "interior(uminus ` S) = image uminus (interior S)"
-  by (simp add: bij_uminus interior_bijective_linear_image linear_uminus)
-
-text \<open>Preservation of compactness and connectedness under continuous function.\<close>
-
-lemma compact_eq_openin_cover:
-  "compact S \<longleftrightarrow>
-    (\<forall>C. (\<forall>c\<in>C. openin (subtopology euclidean S) c) \<and> S \<subseteq> \<Union>C \<longrightarrow>
-      (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
-proof safe
-  fix C
-  assume "compact S" and "\<forall>c\<in>C. openin (subtopology euclidean S) c" and "S \<subseteq> \<Union>C"
-  then have "\<forall>c\<in>{T. open T \<and> S \<inter> T \<in> C}. open c" and "S \<subseteq> \<Union>{T. open T \<and> S \<inter> T \<in> C}"
-    unfolding openin_open by force+
-  with \<open>compact S\<close> obtain D where "D \<subseteq> {T. open T \<and> S \<inter> T \<in> C}" and "finite D" and "S \<subseteq> \<Union>D"
-    by (meson compactE)
-  then have "image (\<lambda>T. S \<inter> T) D \<subseteq> C \<and> finite (image (\<lambda>T. S \<inter> T) D) \<and> S \<subseteq> \<Union>(image (\<lambda>T. S \<inter> T) D)"
-    by auto
-  then show "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" ..
-next
-  assume 1: "\<forall>C. (\<forall>c\<in>C. openin (subtopology euclidean S) c) \<and> S \<subseteq> \<Union>C \<longrightarrow>
-        (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D)"
-  show "compact S"
-  proof (rule compactI)
-    fix C
-    let ?C = "image (\<lambda>T. S \<inter> T) C"
-    assume "\<forall>t\<in>C. open t" and "S \<subseteq> \<Union>C"
-    then have "(\<forall>c\<in>?C. openin (subtopology euclidean S) c) \<and> S \<subseteq> \<Union>?C"
-      unfolding openin_open by auto
-    with 1 obtain D where "D \<subseteq> ?C" and "finite D" and "S \<subseteq> \<Union>D"
-      by metis
-    let ?D = "inv_into C (\<lambda>T. S \<inter> T) ` D"
-    have "?D \<subseteq> C \<and> finite ?D \<and> S \<subseteq> \<Union>?D"
-    proof (intro conjI)
-      from \<open>D \<subseteq> ?C\<close> show "?D \<subseteq> C"
-        by (fast intro: inv_into_into)
-      from \<open>finite D\<close> show "finite ?D"
-        by (rule finite_imageI)
-      from \<open>S \<subseteq> \<Union>D\<close> show "S \<subseteq> \<Union>?D"
-        apply (rule subset_trans, clarsimp)
-        apply (frule subsetD [OF \<open>D \<subseteq> ?C\<close>, THEN f_inv_into_f])
-        apply (erule rev_bexI, fast)
-        done
-    qed
-    then show "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" ..
-  qed
-qed
-
-subsection%unimportant\<open> Theorems relating continuity and uniform continuity to closures\<close>
-
-lemma continuous_on_closure:
-   "continuous_on (closure S) f \<longleftrightarrow>
-    (\<forall>x e. x \<in> closure S \<and> 0 < e
-           \<longrightarrow> (\<exists>d. 0 < d \<and> (\<forall>y. y \<in> S \<and> dist y x < d \<longrightarrow> dist (f y) (f x) < e)))"
-   (is "?lhs = ?rhs")
-proof
-  assume ?lhs then show ?rhs
-    unfolding continuous_on_iff  by (metis Un_iff closure_def)
-next
-  assume R [rule_format]: ?rhs
-  show ?lhs
-  proof
-    fix x and e::real
-    assume "0 < e" and x: "x \<in> closure S"
-    obtain \<delta>::real where "\<delta> > 0"
-                   and \<delta>: "\<And>y. \<lbrakk>y \<in> S; dist y x < \<delta>\<rbrakk> \<Longrightarrow> dist (f y) (f x) < e/2"
-      using R [of x "e/2"] \<open>0 < e\<close> x by auto
-    have "dist (f y) (f x) \<le> e" if y: "y \<in> closure S" and dyx: "dist y x < \<delta>/2" for y
-    proof -
-      obtain \<delta>'::real where "\<delta>' > 0"
-                      and \<delta>': "\<And>z. \<lbrakk>z \<in> S; dist z y < \<delta>'\<rbrakk> \<Longrightarrow> dist (f z) (f y) < e/2"
-        using R [of y "e/2"] \<open>0 < e\<close> y by auto
-      obtain z where "z \<in> S" and z: "dist z y < min \<delta>' \<delta> / 2"
-        using closure_approachable y
-        by (metis \<open>0 < \<delta>'\<close> \<open>0 < \<delta>\<close> divide_pos_pos min_less_iff_conj zero_less_numeral)
-      have "dist (f z) (f y) < e/2"
-        apply (rule \<delta>' [OF \<open>z \<in> S\<close>])
-        using z \<open>0 < \<delta>'\<close> by linarith
-      moreover have "dist (f z) (f x) < e/2"
-        apply (rule \<delta> [OF \<open>z \<in> S\<close>])
-        using z \<open>0 < \<delta>\<close>  dist_commute[of y z] dist_triangle_half_r [of y] dyx by auto
-      ultimately show ?thesis
-        by (metis dist_commute dist_triangle_half_l less_imp_le)
-    qed
-    then show "\<exists>d>0. \<forall>x'\<in>closure S. dist x' x < d \<longrightarrow> dist (f x') (f x) \<le> e"
-      by (rule_tac x="\<delta>/2" in exI) (simp add: \<open>\<delta> > 0\<close>)
-  qed
-qed
-
-lemma continuous_on_closure_sequentially:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b :: metric_space"
-  shows
-   "continuous_on (closure S) f \<longleftrightarrow>
-    (\<forall>x a. a \<in> closure S \<and> (\<forall>n. x n \<in> S) \<and> x \<longlonglongrightarrow> a \<longrightarrow> (f \<circ> x) \<longlonglongrightarrow> f a)"
-   (is "?lhs = ?rhs")
-proof -
-  have "continuous_on (closure S) f \<longleftrightarrow>
-           (\<forall>x \<in> closure S. continuous (at x within S) f)"
-    by (force simp: continuous_on_closure continuous_within_eps_delta)
-  also have "... = ?rhs"
-    by (force simp: continuous_within_sequentially)
-  finally show ?thesis .
-qed
-
-lemma uniformly_continuous_on_closure:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
-  assumes ucont: "uniformly_continuous_on S f"
-      and cont: "continuous_on (closure S) f"
-    shows "uniformly_continuous_on (closure S) f"
-unfolding uniformly_continuous_on_def
-proof (intro allI impI)
-  fix e::real
-  assume "0 < e"
-  then obtain d::real
-    where "d>0"
-      and d: "\<And>x x'. \<lbrakk>x\<in>S; x'\<in>S; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e/3"
-    using ucont [unfolded uniformly_continuous_on_def, rule_format, of "e/3"] by auto
-  show "\<exists>d>0. \<forall>x\<in>closure S. \<forall>x'\<in>closure S. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
-  proof (rule exI [where x="d/3"], clarsimp simp: \<open>d > 0\<close>)
-    fix x y
-    assume x: "x \<in> closure S" and y: "y \<in> closure S" and dyx: "dist y x * 3 < d"
-    obtain d1::real where "d1 > 0"
-           and d1: "\<And>w. \<lbrakk>w \<in> closure S; dist w x < d1\<rbrakk> \<Longrightarrow> dist (f w) (f x) < e/3"
-      using cont [unfolded continuous_on_iff, rule_format, of "x" "e/3"] \<open>0 < e\<close> x by auto
-     obtain x' where "x' \<in> S" and x': "dist x' x < min d1 (d / 3)"
-        using closure_approachable [of x S]
-        by (metis \<open>0 < d1\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj x zero_less_numeral)
-    obtain d2::real where "d2 > 0"
-           and d2: "\<forall>w \<in> closure S. dist w y < d2 \<longrightarrow> dist (f w) (f y) < e/3"
-      using cont [unfolded continuous_on_iff, rule_format, of "y" "e/3"] \<open>0 < e\<close> y by auto
-     obtain y' where "y' \<in> S" and y': "dist y' y < min d2 (d / 3)"
-        using closure_approachable [of y S]
-        by (metis \<open>0 < d2\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj y zero_less_numeral)
-     have "dist x' x < d/3" using x' by auto
-     moreover have "dist x y < d/3"
-       by (metis dist_commute dyx less_divide_eq_numeral1(1))
-     moreover have "dist y y' < d/3"
-       by (metis (no_types) dist_commute min_less_iff_conj y')
-     ultimately have "dist x' y' < d/3 + d/3 + d/3"
-       by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)
-     then have "dist x' y' < d" by simp
-     then have "dist (f x') (f y') < e/3"
-       by (rule d [OF \<open>y' \<in> S\<close> \<open>x' \<in> S\<close>])
-     moreover have "dist (f x') (f x) < e/3" using \<open>x' \<in> S\<close> closure_subset x' d1
-       by (simp add: closure_def)
-     moreover have "dist (f y') (f y) < e/3" using \<open>y' \<in> S\<close> closure_subset y' d2
-       by (simp add: closure_def)
-     ultimately have "dist (f y) (f x) < e/3 + e/3 + e/3"
-       by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)
-    then show "dist (f y) (f x) < e" by simp
-  qed
-qed
-
-lemma uniformly_continuous_on_extension_at_closure:
-  fixes f::"'a::metric_space \<Rightarrow> 'b::complete_space"
-  assumes uc: "uniformly_continuous_on X f"
-  assumes "x \<in> closure X"
-  obtains l where "(f \<longlongrightarrow> l) (at x within X)"
-proof -
-  from assms obtain xs where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"
-    by (auto simp: closure_sequential)
-
-  from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF xs]
-  obtain l where l: "(\<lambda>n. f (xs n)) \<longlonglongrightarrow> l"
-    by atomize_elim (simp only: convergent_eq_Cauchy)
-
-  have "(f \<longlongrightarrow> l) (at x within X)"
-  proof (safe intro!: Lim_within_LIMSEQ)
-    fix xs'
-    assume "\<forall>n. xs' n \<noteq> x \<and> xs' n \<in> X"
-      and xs': "xs' \<longlonglongrightarrow> x"
-    then have "xs' n \<noteq> x" "xs' n \<in> X" for n by auto
-
-    from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF \<open>xs' \<longlonglongrightarrow> x\<close> \<open>xs' _ \<in> X\<close>]
-    obtain l' where l': "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l'"
-      by atomize_elim (simp only: convergent_eq_Cauchy)
-
-    show "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l"
-    proof (rule tendstoI)
-      fix e::real assume "e > 0"
-      define e' where "e' \<equiv> e / 2"
-      have "e' > 0" using \<open>e > 0\<close> by (simp add: e'_def)
-
-      have "\<forall>\<^sub>F n in sequentially. dist (f (xs n)) l < e'"
-        by (simp add: \<open>0 < e'\<close> l tendstoD)
-      moreover
-      from uc[unfolded uniformly_continuous_on_def, rule_format, OF \<open>e' > 0\<close>]
-      obtain d where d: "d > 0" "\<And>x x'. x \<in> X \<Longrightarrow> x' \<in> X \<Longrightarrow> dist x x' < d \<Longrightarrow> dist (f x) (f x') < e'"
-        by auto
-      have "\<forall>\<^sub>F n in sequentially. dist (xs n) (xs' n) < d"
-        by (auto intro!: \<open>0 < d\<close> order_tendstoD tendsto_eq_intros xs xs')
-      ultimately
-      show "\<forall>\<^sub>F n in sequentially. dist (f (xs' n)) l < e"
-      proof eventually_elim
-        case (elim n)
-        have "dist (f (xs' n)) l \<le> dist (f (xs n)) (f (xs' n)) + dist (f (xs n)) l"
-          by (metis dist_triangle dist_commute)
-        also have "dist (f (xs n)) (f (xs' n)) < e'"
-          by (auto intro!: d xs \<open>xs' _ \<in> _\<close> elim)
-        also note \<open>dist (f (xs n)) l < e'\<close>
-        also have "e' + e' = e" by (simp add: e'_def)
-        finally show ?case by simp
-      qed
-    qed
-  qed
-  thus ?thesis ..
-qed
-
-lemma uniformly_continuous_on_extension_on_closure:
-  fixes f::"'a::metric_space \<Rightarrow> 'b::complete_space"
-  assumes uc: "uniformly_continuous_on X f"
-  obtains g where "uniformly_continuous_on (closure X) g" "\<And>x. x \<in> X \<Longrightarrow> f x = g x"
-    "\<And>Y h x. X \<subseteq> Y \<Longrightarrow> Y \<subseteq> closure X \<Longrightarrow> continuous_on Y h \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> f x = h x) \<Longrightarrow> x \<in> Y \<Longrightarrow> h x = g x"
-proof -
-  from uc have cont_f: "continuous_on X f"
-    by (simp add: uniformly_continuous_imp_continuous)
-  obtain y where y: "(f \<longlongrightarrow> y x) (at x within X)" if "x \<in> closure X" for x
-    apply atomize_elim
-    apply (rule choice)
-    using uniformly_continuous_on_extension_at_closure[OF assms]
-    by metis
-  let ?g = "\<lambda>x. if x \<in> X then f x else y x"
-
-  have "uniformly_continuous_on (closure X) ?g"
-    unfolding uniformly_continuous_on_def
-  proof safe
-    fix e::real assume "e > 0"
-    define e' where "e' \<equiv> e / 3"
-    have "e' > 0" using \<open>e > 0\<close> by (simp add: e'_def)
-    from uc[unfolded uniformly_continuous_on_def, rule_format, OF \<open>0 < e'\<close>]
-    obtain d where "d > 0" and d: "\<And>x x'. x \<in> X \<Longrightarrow> x' \<in> X \<Longrightarrow> dist x' x < d \<Longrightarrow> dist (f x') (f x) < e'"
-      by auto
-    define d' where "d' = d / 3"
-    have "d' > 0" using \<open>d > 0\<close> by (simp add: d'_def)
-    show "\<exists>d>0. \<forall>x\<in>closure X. \<forall>x'\<in>closure X. dist x' x < d \<longrightarrow> dist (?g x') (?g x) < e"
-    proof (safe intro!: exI[where x=d'] \<open>d' > 0\<close>)
-      fix x x' assume x: "x \<in> closure X" and x': "x' \<in> closure X" and dist: "dist x' x < d'"
-      then obtain xs xs' where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"
-        and xs': "xs' \<longlonglongrightarrow> x'" "\<And>n. xs' n \<in> X"
-        by (auto simp: closure_sequential)
-      have "\<forall>\<^sub>F n in sequentially. dist (xs' n) x' < d'"
-        and "\<forall>\<^sub>F n in sequentially. dist (xs n) x < d'"
-        by (auto intro!: \<open>0 < d'\<close> order_tendstoD tendsto_eq_intros xs xs')
-      moreover
-      have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x" if "x \<in> closure X" "x \<notin> X" "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X" for xs x
-        using that not_eventuallyD
-        by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at)
-      then have "(\<lambda>x. f (xs' x)) \<longlonglongrightarrow> ?g x'" "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> ?g x"
-        using x x'
-        by (auto intro!: continuous_on_tendsto_compose[OF cont_f] simp: xs' xs)
-      then have "\<forall>\<^sub>F n in sequentially. dist (f (xs' n)) (?g x') < e'"
-        "\<forall>\<^sub>F n in sequentially. dist (f (xs n)) (?g x) < e'"
-        by (auto intro!: \<open>0 < e'\<close> order_tendstoD tendsto_eq_intros)
-      ultimately
-      have "\<forall>\<^sub>F n in sequentially. dist (?g x') (?g x) < e"
-      proof eventually_elim
-        case (elim n)
-        have "dist (?g x') (?g x) \<le>
-          dist (f (xs' n)) (?g x') + dist (f (xs' n)) (f (xs n)) + dist (f (xs n)) (?g x)"
-          by (metis add.commute add_le_cancel_left dist_commute dist_triangle dist_triangle_le)
-        also
-        {
-          have "dist (xs' n) (xs n) \<le> dist (xs' n) x' + dist x' x + dist (xs n) x"
-            by (metis add.commute add_le_cancel_left  dist_triangle dist_triangle_le)
-          also note \<open>dist (xs' n) x' < d'\<close>
-          also note \<open>dist x' x < d'\<close>
-          also note \<open>dist (xs n) x < d'\<close>
-          finally have "dist (xs' n) (xs n) < d" by (simp add: d'_def)
-        }
-        with \<open>xs _ \<in> X\<close> \<open>xs' _ \<in> X\<close> have "dist (f (xs' n)) (f (xs n)) < e'"
-          by (rule d)
-        also note \<open>dist (f (xs' n)) (?g x') < e'\<close>
-        also note \<open>dist (f (xs n)) (?g x) < e'\<close>
-        finally show ?case by (simp add: e'_def)
-      qed
-      then show "dist (?g x') (?g x) < e" by simp
-    qed
-  qed
-  moreover have "f x = ?g x" if "x \<in> X" for x using that by simp
-  moreover
-  {
-    fix Y h x
-    assume Y: "x \<in> Y" "X \<subseteq> Y" "Y \<subseteq> closure X" and cont_h: "continuous_on Y h"
-      and extension: "(\<And>x. x \<in> X \<Longrightarrow> f x = h x)"
-    {
-      assume "x \<notin> X"
-      have "x \<in> closure X" using Y by auto
-      then obtain xs where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"
-        by (auto simp: closure_sequential)
-      from continuous_on_tendsto_compose[OF cont_h xs(1)] xs(2) Y
-      have hx: "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> h x"
-        by (auto simp: set_mp extension)
-      then have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x"
-        using \<open>x \<notin> X\<close> not_eventuallyD xs(2)
-        by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at xs)
-      with hx have "h x = y x" by (rule LIMSEQ_unique)
-    } then
-    have "h x = ?g x"
-      using extension by auto
-  }
-  ultimately show ?thesis ..
-qed
-
-lemma bounded_uniformly_continuous_image:
-  fixes f :: "'a :: heine_borel \<Rightarrow> 'b :: heine_borel"
-  assumes "uniformly_continuous_on S f" "bounded S"
-  shows "bounded(f ` S)"
-  by (metis (no_types, lifting) assms bounded_closure_image compact_closure compact_continuous_image compact_eq_bounded_closed image_cong uniformly_continuous_imp_continuous uniformly_continuous_on_extension_on_closure)
-
-subsection%unimportant \<open>Making a continuous function avoid some value in a neighbourhood\<close>
-
-lemma continuous_within_avoid:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
-  assumes "continuous (at x within s) f"
-    and "f x \<noteq> a"
-  shows "\<exists>e>0. \<forall>y \<in> s. dist x y < e --> f y \<noteq> a"
-proof -
-  obtain U where "open U" and "f x \<in> U" and "a \<notin> U"
-    using t1_space [OF \<open>f x \<noteq> a\<close>] by fast
-  have "(f \<longlongrightarrow> f x) (at x within s)"
-    using assms(1) by (simp add: continuous_within)
-  then have "eventually (\<lambda>y. f y \<in> U) (at x within s)"
-    using \<open>open U\<close> and \<open>f x \<in> U\<close>
-    unfolding tendsto_def by fast
-  then have "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
-    using \<open>a \<notin> U\<close> by (fast elim: eventually_mono)
-  then show ?thesis
-    using \<open>f x \<noteq> a\<close> by (auto simp: dist_commute eventually_at)
-qed
-
-lemma continuous_at_avoid:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
-  assumes "continuous (at x) f"
-    and "f x \<noteq> a"
-  shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"
-  using assms continuous_within_avoid[of x UNIV f a] by simp
-
-lemma continuous_on_avoid:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
-  assumes "continuous_on s f"
-    and "x \<in> s"
-    and "f x \<noteq> a"
-  shows "\<exists>e>0. \<forall>y \<in> s. dist x y < e \<longrightarrow> f y \<noteq> a"
-  using assms(1)[unfolded continuous_on_eq_continuous_within, THEN bspec[where x=x],
-    OF assms(2)] continuous_within_avoid[of x s f a]
-  using assms(3)
-  by auto
-
-lemma continuous_on_open_avoid:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
-  assumes "continuous_on s f"
-    and "open s"
-    and "x \<in> s"
-    and "f x \<noteq> a"
-  shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"
-  using assms(1)[unfolded continuous_on_eq_continuous_at[OF assms(2)], THEN bspec[where x=x], OF assms(3)]
-  using continuous_at_avoid[of x f a] assms(4)
-  by auto
-
 subsection%unimportant\<open>Quotient maps\<close>
 
 lemma quotient_map_imp_continuous_open:
diff -r 10644973cdde -r 42cc3609fedf src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Sun Jan 06 16:27:52 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Sun Jan 06 17:54:49 2019 +0100
@@ -43,6 +43,7 @@
   from power2_le_imp_le[OF th yz] show ?thesis .
 qed
 
+
 subsection \<open>Combination of Elementary and Abstract Topology\<close>
 
 lemma closedin_limpt:
@@ -132,8 +133,51 @@
          \<Longrightarrow> openin (subtopology euclidean u) (s - {a})"
 by (metis Int_Diff open_delete openin_open)
 
+lemma compact_eq_openin_cover:
+  "compact S \<longleftrightarrow>
+    (\<forall>C. (\<forall>c\<in>C. openin (subtopology euclidean S) c) \<and> S \<subseteq> \<Union>C \<longrightarrow>
+      (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
+proof safe
+  fix C
+  assume "compact S" and "\<forall>c\<in>C. openin (subtopology euclidean S) c" and "S \<subseteq> \<Union>C"
+  then have "\<forall>c\<in>{T. open T \<and> S \<inter> T \<in> C}. open c" and "S \<subseteq> \<Union>{T. open T \<and> S \<inter> T \<in> C}"
+    unfolding openin_open by force+
+  with \<open>compact S\<close> obtain D where "D \<subseteq> {T. open T \<and> S \<inter> T \<in> C}" and "finite D" and "S \<subseteq> \<Union>D"
+    by (meson compactE)
+  then have "image (\<lambda>T. S \<inter> T) D \<subseteq> C \<and> finite (image (\<lambda>T. S \<inter> T) D) \<and> S \<subseteq> \<Union>(image (\<lambda>T. S \<inter> T) D)"
+    by auto
+  then show "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" ..
+next
+  assume 1: "\<forall>C. (\<forall>c\<in>C. openin (subtopology euclidean S) c) \<and> S \<subseteq> \<Union>C \<longrightarrow>
+        (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D)"
+  show "compact S"
+  proof (rule compactI)
+    fix C
+    let ?C = "image (\<lambda>T. S \<inter> T) C"
+    assume "\<forall>t\<in>C. open t" and "S \<subseteq> \<Union>C"
+    then have "(\<forall>c\<in>?C. openin (subtopology euclidean S) c) \<and> S \<subseteq> \<Union>?C"
+      unfolding openin_open by auto
+    with 1 obtain D where "D \<subseteq> ?C" and "finite D" and "S \<subseteq> \<Union>D"
+      by metis
+    let ?D = "inv_into C (\<lambda>T. S \<inter> T) ` D"
+    have "?D \<subseteq> C \<and> finite ?D \<and> S \<subseteq> \<Union>?D"
+    proof (intro conjI)
+      from \<open>D \<subseteq> ?C\<close> show "?D \<subseteq> C"
+        by (fast intro: inv_into_into)
+      from \<open>finite D\<close> show "finite ?D"
+        by (rule finite_imageI)
+      from \<open>S \<subseteq> \<Union>D\<close> show "S \<subseteq> \<Union>?D"
+        apply (rule subset_trans, clarsimp)
+        apply (frule subsetD [OF \<open>D \<subseteq> ?C\<close>, THEN f_inv_into_f])
+        apply (erule rev_bexI, fast)
+        done
+    qed
+    then show "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" ..
+  qed
+qed
 
-subsection \<open>Continuity\<close>
+
+subsubsection \<open>Continuity\<close>
 
 lemma interior_image_subset:
   assumes "inj f" "\<And>x. continuous (at x) f"
@@ -153,6 +197,66 @@
   with \<open>x = f y\<close> show "x \<in> f ` interior S" ..
 qed
 
+subsubsection%unimportant \<open>Equality of continuous functions on closure and related results\<close>
+
+lemma continuous_closedin_preimage_constant:
+  fixes f :: "_ \<Rightarrow> 'b::t1_space"
+  shows "continuous_on S f \<Longrightarrow> closedin (subtopology euclidean S) {x \<in> S. f x = a}"
+  using continuous_closedin_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)
+
+lemma continuous_closed_preimage_constant:
+  fixes f :: "_ \<Rightarrow> 'b::t1_space"
+  shows "continuous_on S f \<Longrightarrow> closed S \<Longrightarrow> closed {x \<in> S. f x = a}"
+  using continuous_closed_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)
+
+lemma continuous_constant_on_closure:
+  fixes f :: "_ \<Rightarrow> 'b::t1_space"
+  assumes "continuous_on (closure S) f"
+      and "\<And>x. x \<in> S \<Longrightarrow> f x = a"
+      and "x \<in> closure S"
+  shows "f x = a"
+    using continuous_closed_preimage_constant[of "closure S" f a]
+      assms closure_minimal[of S "{x \<in> closure S. f x = a}"] closure_subset
+    unfolding subset_eq
+    by auto
+
+lemma image_closure_subset:
+  assumes contf: "continuous_on (closure S) f"
+    and "closed T"
+    and "(f ` S) \<subseteq> T"
+  shows "f ` (closure S) \<subseteq> T"
+proof -
+  have "S \<subseteq> {x \<in> closure S. f x \<in> T}"
+    using assms(3) closure_subset by auto
+  moreover have "closed (closure S \<inter> f -` T)"
+    using continuous_closed_preimage[OF contf] \<open>closed T\<close> by auto
+  ultimately have "closure S = (closure S \<inter> f -` T)"
+    using closure_minimal[of S "(closure S \<inter> f -` T)"] by auto
+  then show ?thesis by auto
+qed
+
+subsubsection%unimportant \<open>A function constant on a set\<close>
+
+definition constant_on  (infixl "(constant'_on)" 50)
+  where "f constant_on A \<equiv> \<exists>y. \<forall>x\<in>A. f x = y"
+
+lemma constant_on_subset: "\<lbrakk>f constant_on A; B \<subseteq> A\<rbrakk> \<Longrightarrow> f constant_on B"
+  unfolding constant_on_def by blast
+
+lemma injective_not_constant:
+  fixes S :: "'a::{perfect_space} set"
+  shows "\<lbrakk>open S; inj_on f S; f constant_on S\<rbrakk> \<Longrightarrow> S = {}"
+unfolding constant_on_def
+by (metis equals0I inj_on_contraD islimpt_UNIV islimpt_def)
+
+lemma constant_on_closureI:
+  fixes f :: "_ \<Rightarrow> 'b::t1_space"
+  assumes cof: "f constant_on S" and contf: "continuous_on (closure S) f"
+    shows "f constant_on (closure S)"
+using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def
+by metis
+
+
 subsection \<open>Open and closed balls\<close>
 
 definition%important ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
@@ -182,24 +286,12 @@
 lemma sphere_trivial [simp]: "sphere x 0 = {x}"
   by (simp add: sphere_def)
 
-lemma mem_ball_0 [simp]: "x \<in> ball 0 e \<longleftrightarrow> norm x < e"
-  for x :: "'a::real_normed_vector"
-  by (simp add: dist_norm)
-
-lemma mem_cball_0 [simp]: "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e"
-  for x :: "'a::real_normed_vector"
-  by (simp add: dist_norm)
-
 lemma disjoint_ballI: "dist x y \<ge> r+s \<Longrightarrow> ball x r \<inter> ball y s = {}"
   using dist_triangle_less_add not_le by fastforce
 
 lemma disjoint_cballI: "dist x y > r + s \<Longrightarrow> cball x r \<inter> cball y s = {}"
   by (metis add_mono disjoint_iff_not_equal dist_triangle2 dual_order.trans leD mem_cball)
 
-lemma mem_sphere_0 [simp]: "x \<in> sphere 0 e \<longleftrightarrow> norm x = e"
-  for x :: "'a::real_normed_vector"
-  by (simp add: dist_norm)
-
 lemma sphere_empty [simp]: "r < 0 \<Longrightarrow> sphere a r = {}"
   for a :: "'a::metric_space"
   by auto
@@ -259,24 +351,6 @@
 lemma cball_diff_eq_sphere: "cball a r - ball a r =  sphere a r"
   by (auto simp: cball_def ball_def dist_commute)
 
-lemma image_add_ball [simp]:
-  fixes a :: "'a::real_normed_vector"
-  shows "(+) b ` ball a r = ball (a+b) r"
-apply (intro equalityI subsetI)
-apply (force simp: dist_norm)
-apply (rule_tac x="x-b" in image_eqI)
-apply (auto simp: dist_norm algebra_simps)
-done
-
-lemma image_add_cball [simp]:
-  fixes a :: "'a::real_normed_vector"
-  shows "(+) b ` cball a r = cball (a+b) r"
-apply (intro equalityI subsetI)
-apply (force simp: dist_norm)
-apply (rule_tac x="x-b" in image_eqI)
-apply (auto simp: dist_norm algebra_simps)
-done
-
 lemma open_ball [intro, simp]: "open (ball x e)"
 proof -
   have "open (dist x -` {..<e})"
@@ -362,6 +436,42 @@
   shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)"
   by (auto simp: dist_real_def field_simps mem_ball)
 
+lemma interior_ball [simp]: "interior (ball x e) = ball x e"
+  by (simp add: interior_open)
+
+lemma cball_eq_empty [simp]: "cball x e = {} \<longleftrightarrow> e < 0"
+  apply (simp add: set_eq_iff not_le)
+  apply (metis zero_le_dist dist_self order_less_le_trans)
+  done
+
+lemma cball_empty [simp]: "e < 0 \<Longrightarrow> cball x e = {}"
+  by simp
+
+lemma cball_sing:
+  fixes x :: "'a::metric_space"
+  shows "e = 0 \<Longrightarrow> cball x e = {x}"
+  by (auto simp: set_eq_iff)
+
+lemma ball_divide_subset: "d \<ge> 1 \<Longrightarrow> ball x (e/d) \<subseteq> ball x e"
+  apply (cases "e \<le> 0")
+  apply (simp add: ball_empty divide_simps)
+  apply (rule subset_ball)
+  apply (simp add: divide_simps)
+  done
+
+lemma ball_divide_subset_numeral: "ball x (e / numeral w) \<subseteq> ball x e"
+  using ball_divide_subset one_le_numeral by blast
+
+lemma cball_divide_subset: "d \<ge> 1 \<Longrightarrow> cball x (e/d) \<subseteq> cball x e"
+  apply (cases "e < 0")
+  apply (simp add: divide_simps)
+  apply (rule subset_cball)
+  apply (metis div_by_1 frac_le not_le order_refl zero_less_one)
+  done
+
+lemma cball_divide_subset_numeral: "cball x (e / numeral w) \<subseteq> cball x e"
+  using cball_divide_subset one_le_numeral by blast
+
 
 subsection \<open>Limit Points\<close>
 
@@ -377,10 +487,6 @@
     THEN arg_cong [where f=Not]]
   by (simp add: Bex_def conj_commute conj_left_commute)
 
-lemma perfect_choose_dist: "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r"
-  for x :: "'a::{perfect_space,metric_space}"
-  using islimpt_UNIV [of x] by (simp add: islimpt_approachable)
-
 lemma limpt_of_limpts: "x islimpt {y. y islimpt S} \<Longrightarrow> x islimpt S"
   for x :: "'a::metric_space"
   apply (clarsimp simp add: islimpt_approachable)
@@ -410,6 +516,25 @@
   by (metis open_ball centre_in_ball finite_Int inf.absorb_iff2 inf_assoc open_contains_cball_eq)
 
 
+subsection \<open>Perfect Metric Spaces\<close>
+
+lemma perfect_choose_dist: "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r"
+  for x :: "'a::{perfect_space,metric_space}"
+  using islimpt_UNIV [of x] by (simp add: islimpt_approachable)
+
+lemma cball_eq_sing:
+  fixes x :: "'a::{metric_space,perfect_space}"
+  shows "cball x e = {x} \<longleftrightarrow> e = 0"
+proof (rule linorder_cases)
+  assume e: "0 < e"
+  obtain a where "a \<noteq> x" "dist a x < e"
+    using perfect_choose_dist [OF e] by auto
+  then have "a \<noteq> x" "dist x a \<le> e"
+    by (auto simp: dist_commute)
+  with e show ?thesis by (auto simp: set_eq_iff)
+qed auto
+
+
 subsection \<open>?\<close>
 
 lemma finite_ball_include:
@@ -484,6 +609,10 @@
   using open_contains_ball_eq [where S="interior S"]
   by (simp add: open_subset_interior)
 
+lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"
+  by (meson ball_subset_cball interior_subset mem_interior open_contains_cball open_interior
+      subset_trans)
+
 
 subsection \<open>Frontier\<close>
 
@@ -835,6 +964,50 @@
   by (rule closed_subset_contains_Inf)
      (auto intro: closed_real_atLeastAtMost intro!: bdd_belowI[of A a])
 
+lemma bounded_real: "bounded (S::real set) \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. \<bar>x\<bar> \<le> a)"
+  by (simp add: bounded_iff)
+
+lemma bounded_imp_bdd_above: "bounded S \<Longrightarrow> bdd_above (S :: real set)"
+  by (auto simp: bounded_def bdd_above_def dist_real_def)
+     (metis abs_le_D1 abs_minus_commute diff_le_eq)
+
+lemma bounded_imp_bdd_below: "bounded S \<Longrightarrow> bdd_below (S :: real set)"
+  by (auto simp: bounded_def bdd_below_def dist_real_def)
+     (metis abs_le_D1 add.commute diff_le_eq)
+
+lemma bounded_has_Sup:
+  fixes S :: "real set"
+  assumes "bounded S"
+    and "S \<noteq> {}"
+  shows "\<forall>x\<in>S. x \<le> Sup S"
+    and "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b"
+proof
+  show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b"
+    using assms by (metis cSup_least)
+qed (metis cSup_upper assms(1) bounded_imp_bdd_above)
+
+lemma Sup_insert:
+  fixes S :: "real set"
+  shows "bounded S \<Longrightarrow> Sup (insert x S) = (if S = {} then x else max x (Sup S))"
+  by (auto simp: bounded_imp_bdd_above sup_max cSup_insert_If)
+
+lemma bounded_has_Inf:
+  fixes S :: "real set"
+  assumes "bounded S"
+    and "S \<noteq> {}"
+  shows "\<forall>x\<in>S. x \<ge> Inf S"
+    and "\<forall>b. (\<forall>x\<in>S. x \<ge> b) \<longrightarrow> Inf S \<ge> b"
+proof
+  show "\<forall>b. (\<forall>x\<in>S. x \<ge> b) \<longrightarrow> Inf S \<ge> b"
+    using assms by (metis cInf_greatest)
+qed (metis cInf_lower assms(1) bounded_imp_bdd_below)
+
+lemma Inf_insert:
+  fixes S :: "real set"
+  shows "bounded S \<Longrightarrow> Inf (insert x S) = (if S = {} then x else min x (Inf S))"
+  by (auto simp: bounded_imp_bdd_below inf_min cInf_insert_If)
+
+
 subsection \<open>Compactness\<close>
 
 lemma compact_imp_bounded:
@@ -1134,6 +1307,7 @@
     using l r by fast
 qed
 
+
 subsubsection \<open>Completeness\<close>
 
 proposition (in metric_space) completeI:
@@ -1392,6 +1566,297 @@
   using frontier_subset_closed compact_eq_bounded_closed
   by blast
 
+
+subsubsection \<open>Properties of Balls and Spheres\<close>
+
+lemma compact_cball[simp]:
+  fixes x :: "'a::heine_borel"
+  shows "compact (cball x e)"
+  using compact_eq_bounded_closed bounded_cball closed_cball
+  by blast
+
+lemma compact_frontier_bounded[intro]:
+  fixes S :: "'a::heine_borel set"
+  shows "bounded S \<Longrightarrow> compact (frontier S)"
+  unfolding frontier_def
+  using compact_eq_bounded_closed
+  by blast
+
+lemma compact_frontier[intro]:
+  fixes S :: "'a::heine_borel set"
+  shows "compact S \<Longrightarrow> compact (frontier S)"
+  using compact_eq_bounded_closed compact_frontier_bounded
+  by blast
+
+
+subsubsection \<open>Distance from a Set\<close>
+
+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"
+proof (rule continuous_attains_sup [OF assms])
+  {
+    fix x
+    assume "x\<in>s"
+    have "(dist a \<longlongrightarrow> dist a x) (at x within s)"
+      by (intro tendsto_dist tendsto_const tendsto_ident_at)
+  }
+  then show "continuous_on s (dist a)"
+    unfolding continuous_on ..
+qed
+
+text \<open>For \emph{minimal} distance, we only need closure, not compactness.\<close>
+
+lemma distance_attains_inf:
+  fixes a :: "'a::heine_borel"
+  assumes "closed s" and "s \<noteq> {}"
+  obtains x where "x\<in>s" "\<And>y. y \<in> s \<Longrightarrow> dist a x \<le> dist a y"
+proof -
+  from assms obtain b where "b \<in> s" by auto
+  let ?B = "s \<inter> cball a (dist b a)"
+  have "?B \<noteq> {}" using \<open>b \<in> s\<close>
+    by (auto simp: dist_commute)
+  moreover have "continuous_on ?B (dist a)"
+    by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)
+  moreover have "compact ?B"
+    by (intro closed_Int_compact \<open>closed s\<close> compact_cball)
+  ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"
+    by (metis continuous_attains_inf)
+  with that show ?thesis by fastforce
+qed
+
+subsection \<open>Infimum Distance\<close>
+
+definition%important "infdist x A = (if A = {} then 0 else INF a\<in>A. dist x a)"
+
+lemma bdd_below_image_dist[intro, simp]: "bdd_below (dist x ` A)"
+  by (auto intro!: zero_le_dist)
+
+lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = (INF a\<in>A. dist x a)"
+  by (simp add: infdist_def)
+
+lemma infdist_nonneg: "0 \<le> infdist x A"
+  by (auto simp: infdist_def intro: cINF_greatest)
+
+lemma infdist_le: "a \<in> A \<Longrightarrow> infdist x A \<le> dist x a"
+  by (auto intro: cINF_lower simp add: infdist_def)
+
+lemma infdist_le2: "a \<in> A \<Longrightarrow> dist x a \<le> d \<Longrightarrow> infdist x A \<le> d"
+  by (auto intro!: cINF_lower2 simp add: infdist_def)
+
+lemma infdist_zero[simp]: "a \<in> A \<Longrightarrow> infdist a A = 0"
+  by (auto intro!: antisym infdist_nonneg infdist_le2)
+
+lemma infdist_triangle: "infdist x A \<le> infdist y A + dist x y"
+proof (cases "A = {}")
+  case True
+  then show ?thesis by (simp add: infdist_def)
+next
+  case False
+  then obtain a where "a \<in> A" by auto
+  have "infdist x A \<le> Inf {dist x y + dist y a |a. a \<in> A}"
+  proof (rule cInf_greatest)
+    from \<open>A \<noteq> {}\<close> show "{dist x y + dist y a |a. a \<in> A} \<noteq> {}"
+      by simp
+    fix d
+    assume "d \<in> {dist x y + dist y a |a. a \<in> A}"
+    then obtain a where d: "d = dist x y + dist y a" "a \<in> A"
+      by auto
+    show "infdist x A \<le> d"
+      unfolding infdist_notempty[OF \<open>A \<noteq> {}\<close>]
+    proof (rule cINF_lower2)
+      show "a \<in> A" by fact
+      show "dist x a \<le> d"
+        unfolding d by (rule dist_triangle)
+    qed simp
+  qed
+  also have "\<dots> = dist x y + infdist y A"
+  proof (rule cInf_eq, safe)
+    fix a
+    assume "a \<in> A"
+    then show "dist x y + infdist y A \<le> dist x y + dist y a"
+      by (auto intro: infdist_le)
+  next
+    fix i
+    assume inf: "\<And>d. d \<in> {dist x y + dist y a |a. a \<in> A} \<Longrightarrow> i \<le> d"
+    then have "i - dist x y \<le> infdist y A"
+      unfolding infdist_notempty[OF \<open>A \<noteq> {}\<close>] using \<open>a \<in> A\<close>
+      by (intro cINF_greatest) (auto simp: field_simps)
+    then show "i \<le> dist x y + infdist y A"
+      by simp
+  qed
+  finally show ?thesis by simp
+qed
+
+lemma in_closure_iff_infdist_zero:
+  assumes "A \<noteq> {}"
+  shows "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
+proof
+  assume "x \<in> closure A"
+  show "infdist x A = 0"
+  proof (rule ccontr)
+    assume "infdist x A \<noteq> 0"
+    with infdist_nonneg[of x A] have "infdist x A > 0"
+      by auto
+    then have "ball x (infdist x A) \<inter> closure A = {}"
+      apply auto
+      apply (metis \<open>x \<in> closure A\<close> closure_approachable dist_commute infdist_le not_less)
+      done
+    then have "x \<notin> closure A"
+      by (metis \<open>0 < infdist x A\<close> centre_in_ball disjoint_iff_not_equal)
+    then show False using \<open>x \<in> closure A\<close> by simp
+  qed
+next
+  assume x: "infdist x A = 0"
+  then obtain a where "a \<in> A"
+    by atomize_elim (metis all_not_in_conv assms)
+  show "x \<in> closure A"
+    unfolding closure_approachable
+    apply safe
+  proof (rule ccontr)
+    fix e :: real
+    assume "e > 0"
+    assume "\<not> (\<exists>y\<in>A. dist y x < e)"
+    then have "infdist x A \<ge> e" using \<open>a \<in> A\<close>
+      unfolding infdist_def
+      by (force simp: dist_commute intro: cINF_greatest)
+    with x \<open>e > 0\<close> show False by auto
+  qed
+qed
+
+lemma in_closed_iff_infdist_zero:
+  assumes "closed A" "A \<noteq> {}"
+  shows "x \<in> A \<longleftrightarrow> infdist x A = 0"
+proof -
+  have "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
+    by (rule in_closure_iff_infdist_zero) fact
+  with assms show ?thesis by simp
+qed
+
+lemma infdist_pos_not_in_closed:
+  assumes "closed S" "S \<noteq> {}" "x \<notin> S"
+  shows "infdist x S > 0"
+using in_closed_iff_infdist_zero[OF assms(1) assms(2), of x] assms(3) infdist_nonneg le_less by fastforce
+
+lemma
+  infdist_attains_inf:
+  fixes X::"'a::heine_borel set"
+  assumes "closed X"
+  assumes "X \<noteq> {}"
+  obtains x where "x \<in> X" "infdist y X = dist y x"
+proof -
+  have "bdd_below (dist y ` X)"
+    by auto
+  from distance_attains_inf[OF assms, of y]
+  obtain x where INF: "x \<in> X" "\<And>z. z \<in> X \<Longrightarrow> dist y x \<le> dist y z" by auto
+  have "infdist y X = dist y x"
+    by (auto simp: infdist_def assms
+      intro!: antisym cINF_lower[OF _ \<open>x \<in> X\<close>] cINF_greatest[OF assms(2) INF(2)])
+  with \<open>x \<in> X\<close> show ?thesis ..
+qed
+
+
+text \<open>Every metric space is a T4 space:\<close>
+
+instance metric_space \<subseteq> t4_space
+proof
+  fix S T::"'a set" assume H: "closed S" "closed T" "S \<inter> T = {}"
+  consider "S = {}" | "T = {}" | "S \<noteq> {} \<and> T \<noteq> {}" by auto
+  then show "\<exists>U V. open U \<and> open V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> U \<inter> V = {}"
+  proof (cases)
+    case 1
+    show ?thesis
+      apply (rule exI[of _ "{}"], rule exI[of _ UNIV]) using 1 by auto
+  next
+    case 2
+    show ?thesis
+      apply (rule exI[of _ UNIV], rule exI[of _ "{}"]) using 2 by auto
+  next
+    case 3
+    define U where "U = (\<Union>x\<in>S. ball x ((infdist x T)/2))"
+    have A: "open U" unfolding U_def by auto
+    have "infdist x T > 0" if "x \<in> S" for x
+      using H that 3 by (auto intro!: infdist_pos_not_in_closed)
+    then have B: "S \<subseteq> U" unfolding U_def by auto
+    define V where "V = (\<Union>x\<in>T. ball x ((infdist x S)/2))"
+    have C: "open V" unfolding V_def by auto
+    have "infdist x S > 0" if "x \<in> T" for x
+      using H that 3 by (auto intro!: infdist_pos_not_in_closed)
+    then have D: "T \<subseteq> V" unfolding V_def by auto
+
+    have "(ball x ((infdist x T)/2)) \<inter> (ball y ((infdist y S)/2)) = {}" if "x \<in> S" "y \<in> T" for x y
+    proof (auto)
+      fix z assume H: "dist x z * 2 < infdist x T" "dist y z * 2 < infdist y S"
+      have "2 * dist x y \<le> 2 * dist x z + 2 * dist y z"
+        using dist_triangle[of x y z] by (auto simp add: dist_commute)
+      also have "... < infdist x T + infdist y S"
+        using H by auto
+      finally have "dist x y < infdist x T \<or> dist x y < infdist y S"
+        by auto
+      then show False
+        using infdist_le[OF \<open>x \<in> S\<close>, of y] infdist_le[OF \<open>y \<in> T\<close>, of x] by (auto simp add: dist_commute)
+    qed
+    then have E: "U \<inter> V = {}"
+      unfolding U_def V_def by auto
+    show ?thesis
+      apply (rule exI[of _ U], rule exI[of _ V]) using A B C D E by auto
+  qed
+qed
+
+lemma tendsto_infdist [tendsto_intros]:
+  assumes f: "(f \<longlongrightarrow> l) F"
+  shows "((\<lambda>x. infdist (f x) A) \<longlongrightarrow> infdist l A) F"
+proof (rule tendstoI)
+  fix e ::real
+  assume "e > 0"
+  from tendstoD[OF f this]
+  show "eventually (\<lambda>x. dist (infdist (f x) A) (infdist l A) < e) F"
+  proof (eventually_elim)
+    fix x
+    from infdist_triangle[of l A "f x"] infdist_triangle[of "f x" A l]
+    have "dist (infdist (f x) A) (infdist l A) \<le> dist (f x) l"
+      by (simp add: dist_commute dist_real_def)
+    also assume "dist (f x) l < e"
+    finally show "dist (infdist (f x) A) (infdist l A) < e" .
+  qed
+qed
+
+lemma continuous_infdist[continuous_intros]:
+  assumes "continuous F f"
+  shows "continuous F (\<lambda>x. infdist (f x) A)"
+  using assms unfolding continuous_def by (rule tendsto_infdist)
+
+lemma compact_infdist_le:
+  fixes A::"'a::heine_borel set"
+  assumes "A \<noteq> {}"
+  assumes "compact A"
+  assumes "e > 0"
+  shows "compact {x. infdist x A \<le> e}"
+proof -
+  from continuous_closed_vimage[of "{0..e}" "\<lambda>x. infdist x A"]
+    continuous_infdist[OF continuous_ident, of _ UNIV A]
+  have "closed {x. infdist x A \<le> e}" by (auto simp: vimage_def infdist_nonneg)
+  moreover
+  from assms obtain x0 b where b: "\<And>x. x \<in> A \<Longrightarrow> dist x0 x \<le> b" "closed A"
+    by (auto simp: compact_eq_bounded_closed bounded_def)
+  {
+    fix y
+    assume le: "infdist y A \<le> e"
+    from infdist_attains_inf[OF \<open>closed A\<close> \<open>A \<noteq> {}\<close>, of y]
+    obtain z where z: "z \<in> A" "infdist y A = dist y z" by blast
+    have "dist x0 y \<le> dist y z + dist x0 z"
+      by (metis dist_commute dist_triangle)
+    also have "dist y z \<le> e" using le z by simp
+    also have "dist x0 z \<le> b" using b z by simp
+    finally have "dist x0 y \<le> b + e" by arith
+  } then
+  have "bounded {x. infdist x A \<le> e}"
+    by (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + e"])
+  ultimately show "compact {x. infdist x A \<le> e}"
+    by (simp add: compact_eq_bounded_closed)
+qed
+
+
 subsection \<open>Continuity\<close>
 
 text\<open>Derive the epsilon-delta forms, which we often use as "definitions"\<close>
@@ -1633,6 +2098,267 @@
   unfolding dist_norm tendsto_norm_zero_iff diff[symmetric]
   by (auto intro: tendsto_zero)
 
+subsection%unimportant\<open> Theorems relating continuity and uniform continuity to closures\<close>
+
+lemma continuous_on_closure:
+   "continuous_on (closure S) f \<longleftrightarrow>
+    (\<forall>x e. x \<in> closure S \<and> 0 < e
+           \<longrightarrow> (\<exists>d. 0 < d \<and> (\<forall>y. y \<in> S \<and> dist y x < d \<longrightarrow> dist (f y) (f x) < e)))"
+   (is "?lhs = ?rhs")
+proof
+  assume ?lhs then show ?rhs
+    unfolding continuous_on_iff  by (metis Un_iff closure_def)
+next
+  assume R [rule_format]: ?rhs
+  show ?lhs
+  proof
+    fix x and e::real
+    assume "0 < e" and x: "x \<in> closure S"
+    obtain \<delta>::real where "\<delta> > 0"
+                   and \<delta>: "\<And>y. \<lbrakk>y \<in> S; dist y x < \<delta>\<rbrakk> \<Longrightarrow> dist (f y) (f x) < e/2"
+      using R [of x "e/2"] \<open>0 < e\<close> x by auto
+    have "dist (f y) (f x) \<le> e" if y: "y \<in> closure S" and dyx: "dist y x < \<delta>/2" for y
+    proof -
+      obtain \<delta>'::real where "\<delta>' > 0"
+                      and \<delta>': "\<And>z. \<lbrakk>z \<in> S; dist z y < \<delta>'\<rbrakk> \<Longrightarrow> dist (f z) (f y) < e/2"
+        using R [of y "e/2"] \<open>0 < e\<close> y by auto
+      obtain z where "z \<in> S" and z: "dist z y < min \<delta>' \<delta> / 2"
+        using closure_approachable y
+        by (metis \<open>0 < \<delta>'\<close> \<open>0 < \<delta>\<close> divide_pos_pos min_less_iff_conj zero_less_numeral)
+      have "dist (f z) (f y) < e/2"
+        apply (rule \<delta>' [OF \<open>z \<in> S\<close>])
+        using z \<open>0 < \<delta>'\<close> by linarith
+      moreover have "dist (f z) (f x) < e/2"
+        apply (rule \<delta> [OF \<open>z \<in> S\<close>])
+        using z \<open>0 < \<delta>\<close>  dist_commute[of y z] dist_triangle_half_r [of y] dyx by auto
+      ultimately show ?thesis
+        by (metis dist_commute dist_triangle_half_l less_imp_le)
+    qed
+    then show "\<exists>d>0. \<forall>x'\<in>closure S. dist x' x < d \<longrightarrow> dist (f x') (f x) \<le> e"
+      by (rule_tac x="\<delta>/2" in exI) (simp add: \<open>\<delta> > 0\<close>)
+  qed
+qed
+
+lemma continuous_on_closure_sequentially:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b :: metric_space"
+  shows
+   "continuous_on (closure S) f \<longleftrightarrow>
+    (\<forall>x a. a \<in> closure S \<and> (\<forall>n. x n \<in> S) \<and> x \<longlonglongrightarrow> a \<longrightarrow> (f \<circ> x) \<longlonglongrightarrow> f a)"
+   (is "?lhs = ?rhs")
+proof -
+  have "continuous_on (closure S) f \<longleftrightarrow>
+           (\<forall>x \<in> closure S. continuous (at x within S) f)"
+    by (force simp: continuous_on_closure continuous_within_eps_delta)
+  also have "... = ?rhs"
+    by (force simp: continuous_within_sequentially)
+  finally show ?thesis .
+qed
+
+lemma uniformly_continuous_on_closure:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  assumes ucont: "uniformly_continuous_on S f"
+      and cont: "continuous_on (closure S) f"
+    shows "uniformly_continuous_on (closure S) f"
+unfolding uniformly_continuous_on_def
+proof (intro allI impI)
+  fix e::real
+  assume "0 < e"
+  then obtain d::real
+    where "d>0"
+      and d: "\<And>x x'. \<lbrakk>x\<in>S; x'\<in>S; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e/3"
+    using ucont [unfolded uniformly_continuous_on_def, rule_format, of "e/3"] by auto
+  show "\<exists>d>0. \<forall>x\<in>closure S. \<forall>x'\<in>closure S. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
+  proof (rule exI [where x="d/3"], clarsimp simp: \<open>d > 0\<close>)
+    fix x y
+    assume x: "x \<in> closure S" and y: "y \<in> closure S" and dyx: "dist y x * 3 < d"
+    obtain d1::real where "d1 > 0"
+           and d1: "\<And>w. \<lbrakk>w \<in> closure S; dist w x < d1\<rbrakk> \<Longrightarrow> dist (f w) (f x) < e/3"
+      using cont [unfolded continuous_on_iff, rule_format, of "x" "e/3"] \<open>0 < e\<close> x by auto
+     obtain x' where "x' \<in> S" and x': "dist x' x < min d1 (d / 3)"
+        using closure_approachable [of x S]
+        by (metis \<open>0 < d1\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj x zero_less_numeral)
+    obtain d2::real where "d2 > 0"
+           and d2: "\<forall>w \<in> closure S. dist w y < d2 \<longrightarrow> dist (f w) (f y) < e/3"
+      using cont [unfolded continuous_on_iff, rule_format, of "y" "e/3"] \<open>0 < e\<close> y by auto
+     obtain y' where "y' \<in> S" and y': "dist y' y < min d2 (d / 3)"
+        using closure_approachable [of y S]
+        by (metis \<open>0 < d2\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj y zero_less_numeral)
+     have "dist x' x < d/3" using x' by auto
+     moreover have "dist x y < d/3"
+       by (metis dist_commute dyx less_divide_eq_numeral1(1))
+     moreover have "dist y y' < d/3"
+       by (metis (no_types) dist_commute min_less_iff_conj y')
+     ultimately have "dist x' y' < d/3 + d/3 + d/3"
+       by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)
+     then have "dist x' y' < d" by simp
+     then have "dist (f x') (f y') < e/3"
+       by (rule d [OF \<open>y' \<in> S\<close> \<open>x' \<in> S\<close>])
+     moreover have "dist (f x') (f x) < e/3" using \<open>x' \<in> S\<close> closure_subset x' d1
+       by (simp add: closure_def)
+     moreover have "dist (f y') (f y) < e/3" using \<open>y' \<in> S\<close> closure_subset y' d2
+       by (simp add: closure_def)
+     ultimately have "dist (f y) (f x) < e/3 + e/3 + e/3"
+       by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)
+    then show "dist (f y) (f x) < e" by simp
+  qed
+qed
+
+lemma uniformly_continuous_on_extension_at_closure:
+  fixes f::"'a::metric_space \<Rightarrow> 'b::complete_space"
+  assumes uc: "uniformly_continuous_on X f"
+  assumes "x \<in> closure X"
+  obtains l where "(f \<longlongrightarrow> l) (at x within X)"
+proof -
+  from assms obtain xs where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"
+    by (auto simp: closure_sequential)
+
+  from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF xs]
+  obtain l where l: "(\<lambda>n. f (xs n)) \<longlonglongrightarrow> l"
+    by atomize_elim (simp only: convergent_eq_Cauchy)
+
+  have "(f \<longlongrightarrow> l) (at x within X)"
+  proof (safe intro!: Lim_within_LIMSEQ)
+    fix xs'
+    assume "\<forall>n. xs' n \<noteq> x \<and> xs' n \<in> X"
+      and xs': "xs' \<longlonglongrightarrow> x"
+    then have "xs' n \<noteq> x" "xs' n \<in> X" for n by auto
+
+    from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF \<open>xs' \<longlonglongrightarrow> x\<close> \<open>xs' _ \<in> X\<close>]
+    obtain l' where l': "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l'"
+      by atomize_elim (simp only: convergent_eq_Cauchy)
+
+    show "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l"
+    proof (rule tendstoI)
+      fix e::real assume "e > 0"
+      define e' where "e' \<equiv> e / 2"
+      have "e' > 0" using \<open>e > 0\<close> by (simp add: e'_def)
+
+      have "\<forall>\<^sub>F n in sequentially. dist (f (xs n)) l < e'"
+        by (simp add: \<open>0 < e'\<close> l tendstoD)
+      moreover
+      from uc[unfolded uniformly_continuous_on_def, rule_format, OF \<open>e' > 0\<close>]
+      obtain d where d: "d > 0" "\<And>x x'. x \<in> X \<Longrightarrow> x' \<in> X \<Longrightarrow> dist x x' < d \<Longrightarrow> dist (f x) (f x') < e'"
+        by auto
+      have "\<forall>\<^sub>F n in sequentially. dist (xs n) (xs' n) < d"
+        by (auto intro!: \<open>0 < d\<close> order_tendstoD tendsto_eq_intros xs xs')
+      ultimately
+      show "\<forall>\<^sub>F n in sequentially. dist (f (xs' n)) l < e"
+      proof eventually_elim
+        case (elim n)
+        have "dist (f (xs' n)) l \<le> dist (f (xs n)) (f (xs' n)) + dist (f (xs n)) l"
+          by (metis dist_triangle dist_commute)
+        also have "dist (f (xs n)) (f (xs' n)) < e'"
+          by (auto intro!: d xs \<open>xs' _ \<in> _\<close> elim)
+        also note \<open>dist (f (xs n)) l < e'\<close>
+        also have "e' + e' = e" by (simp add: e'_def)
+        finally show ?case by simp
+      qed
+    qed
+  qed
+  thus ?thesis ..
+qed
+
+lemma uniformly_continuous_on_extension_on_closure:
+  fixes f::"'a::metric_space \<Rightarrow> 'b::complete_space"
+  assumes uc: "uniformly_continuous_on X f"
+  obtains g where "uniformly_continuous_on (closure X) g" "\<And>x. x \<in> X \<Longrightarrow> f x = g x"
+    "\<And>Y h x. X \<subseteq> Y \<Longrightarrow> Y \<subseteq> closure X \<Longrightarrow> continuous_on Y h \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> f x = h x) \<Longrightarrow> x \<in> Y \<Longrightarrow> h x = g x"
+proof -
+  from uc have cont_f: "continuous_on X f"
+    by (simp add: uniformly_continuous_imp_continuous)
+  obtain y where y: "(f \<longlongrightarrow> y x) (at x within X)" if "x \<in> closure X" for x
+    apply atomize_elim
+    apply (rule choice)
+    using uniformly_continuous_on_extension_at_closure[OF assms]
+    by metis
+  let ?g = "\<lambda>x. if x \<in> X then f x else y x"
+
+  have "uniformly_continuous_on (closure X) ?g"
+    unfolding uniformly_continuous_on_def
+  proof safe
+    fix e::real assume "e > 0"
+    define e' where "e' \<equiv> e / 3"
+    have "e' > 0" using \<open>e > 0\<close> by (simp add: e'_def)
+    from uc[unfolded uniformly_continuous_on_def, rule_format, OF \<open>0 < e'\<close>]
+    obtain d where "d > 0" and d: "\<And>x x'. x \<in> X \<Longrightarrow> x' \<in> X \<Longrightarrow> dist x' x < d \<Longrightarrow> dist (f x') (f x) < e'"
+      by auto
+    define d' where "d' = d / 3"
+    have "d' > 0" using \<open>d > 0\<close> by (simp add: d'_def)
+    show "\<exists>d>0. \<forall>x\<in>closure X. \<forall>x'\<in>closure X. dist x' x < d \<longrightarrow> dist (?g x') (?g x) < e"
+    proof (safe intro!: exI[where x=d'] \<open>d' > 0\<close>)
+      fix x x' assume x: "x \<in> closure X" and x': "x' \<in> closure X" and dist: "dist x' x < d'"
+      then obtain xs xs' where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"
+        and xs': "xs' \<longlonglongrightarrow> x'" "\<And>n. xs' n \<in> X"
+        by (auto simp: closure_sequential)
+      have "\<forall>\<^sub>F n in sequentially. dist (xs' n) x' < d'"
+        and "\<forall>\<^sub>F n in sequentially. dist (xs n) x < d'"
+        by (auto intro!: \<open>0 < d'\<close> order_tendstoD tendsto_eq_intros xs xs')
+      moreover
+      have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x" if "x \<in> closure X" "x \<notin> X" "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X" for xs x
+        using that not_eventuallyD
+        by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at)
+      then have "(\<lambda>x. f (xs' x)) \<longlonglongrightarrow> ?g x'" "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> ?g x"
+        using x x'
+        by (auto intro!: continuous_on_tendsto_compose[OF cont_f] simp: xs' xs)
+      then have "\<forall>\<^sub>F n in sequentially. dist (f (xs' n)) (?g x') < e'"
+        "\<forall>\<^sub>F n in sequentially. dist (f (xs n)) (?g x) < e'"
+        by (auto intro!: \<open>0 < e'\<close> order_tendstoD tendsto_eq_intros)
+      ultimately
+      have "\<forall>\<^sub>F n in sequentially. dist (?g x') (?g x) < e"
+      proof eventually_elim
+        case (elim n)
+        have "dist (?g x') (?g x) \<le>
+          dist (f (xs' n)) (?g x') + dist (f (xs' n)) (f (xs n)) + dist (f (xs n)) (?g x)"
+          by (metis add.commute add_le_cancel_left dist_commute dist_triangle dist_triangle_le)
+        also
+        {
+          have "dist (xs' n) (xs n) \<le> dist (xs' n) x' + dist x' x + dist (xs n) x"
+            by (metis add.commute add_le_cancel_left  dist_triangle dist_triangle_le)
+          also note \<open>dist (xs' n) x' < d'\<close>
+          also note \<open>dist x' x < d'\<close>
+          also note \<open>dist (xs n) x < d'\<close>
+          finally have "dist (xs' n) (xs n) < d" by (simp add: d'_def)
+        }
+        with \<open>xs _ \<in> X\<close> \<open>xs' _ \<in> X\<close> have "dist (f (xs' n)) (f (xs n)) < e'"
+          by (rule d)
+        also note \<open>dist (f (xs' n)) (?g x') < e'\<close>
+        also note \<open>dist (f (xs n)) (?g x) < e'\<close>
+        finally show ?case by (simp add: e'_def)
+      qed
+      then show "dist (?g x') (?g x) < e" by simp
+    qed
+  qed
+  moreover have "f x = ?g x" if "x \<in> X" for x using that by simp
+  moreover
+  {
+    fix Y h x
+    assume Y: "x \<in> Y" "X \<subseteq> Y" "Y \<subseteq> closure X" and cont_h: "continuous_on Y h"
+      and extension: "(\<And>x. x \<in> X \<Longrightarrow> f x = h x)"
+    {
+      assume "x \<notin> X"
+      have "x \<in> closure X" using Y by auto
+      then obtain xs where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"
+        by (auto simp: closure_sequential)
+      from continuous_on_tendsto_compose[OF cont_h xs(1)] xs(2) Y
+      have hx: "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> h x"
+        by (auto simp: set_mp extension)
+      then have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x"
+        using \<open>x \<notin> X\<close> not_eventuallyD xs(2)
+        by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at xs)
+      with hx have "h x = y x" by (rule LIMSEQ_unique)
+    } then
+    have "h x = ?g x"
+      using extension by auto
+  }
+  ultimately show ?thesis ..
+qed
+
+lemma bounded_uniformly_continuous_image:
+  fixes f :: "'a :: heine_borel \<Rightarrow> 'b :: heine_borel"
+  assumes "uniformly_continuous_on S f" "bounded S"
+  shows "bounded(f ` S)"
+  by (metis (no_types, lifting) assms bounded_closure_image compact_closure compact_continuous_image compact_eq_bounded_closed image_cong uniformly_continuous_imp_continuous uniformly_continuous_on_extension_on_closure)
+
 
 subsection \<open>With Abstract Topology (TODO: move and remove dependency?)\<close>
 
@@ -1837,4 +2563,171 @@
   shows "continuous (at a within T) g"
   using assms by (simp add: Lim_transform_within_openin continuous_within)
 
+
+subsection \<open>Closed Nest\<close>
+
+text \<open>Bounded closed nest property (proof does not use Heine-Borel)\<close>
+
+lemma bounded_closed_nest:
+  fixes S :: "nat \<Rightarrow> ('a::heine_borel) set"
+  assumes "\<And>n. closed (S n)"
+      and "\<And>n. S n \<noteq> {}"
+      and "\<And>m n. m \<le> n \<Longrightarrow> S n \<subseteq> S m"
+      and "bounded (S 0)"
+  obtains a where "\<And>n. a \<in> S n"
+proof -
+  from assms(2) obtain x where x: "\<forall>n. x n \<in> S n"
+    using choice[of "\<lambda>n x. x \<in> S n"] by auto
+  from assms(4,1) have "seq_compact (S 0)"
+    by (simp add: bounded_closed_imp_seq_compact)
+  then obtain l r where lr: "l \<in> S 0" "strict_mono r" "(x \<circ> r) \<longlonglongrightarrow> l"
+    using x and assms(3) unfolding seq_compact_def by blast
+  have "\<forall>n. l \<in> S n"
+  proof
+    fix n :: nat
+    have "closed (S n)"
+      using assms(1) by simp
+    moreover have "\<forall>i. (x \<circ> r) i \<in> S i"
+      using x and assms(3) and lr(2) [THEN seq_suble] by auto
+    then have "\<forall>i. (x \<circ> r) (i + n) \<in> S n"
+      using assms(3) by (fast intro!: le_add2)
+    moreover have "(\<lambda>i. (x \<circ> r) (i + n)) \<longlonglongrightarrow> l"
+      using lr(3) by (rule LIMSEQ_ignore_initial_segment)
+    ultimately show "l \<in> S n"
+      by (rule closed_sequentially)
+  qed
+  then show ?thesis 
+    using that by blast
+qed
+
+text \<open>Decreasing case does not even need compactness, just completeness.\<close>
+
+lemma decreasing_closed_nest:
+  fixes S :: "nat \<Rightarrow> ('a::complete_space) set"
+  assumes "\<And>n. closed (S n)"
+          "\<And>n. S n \<noteq> {}"
+          "\<And>m n. m \<le> n \<Longrightarrow> S n \<subseteq> S m"
+          "\<And>e. e>0 \<Longrightarrow> \<exists>n. \<forall>x\<in>S n. \<forall>y\<in>S n. dist x y < e"
+  obtains a where "\<And>n. a \<in> S n"
+proof -
+  have "\<forall>n. \<exists>x. x \<in> S n"
+    using assms(2) by auto
+  then have "\<exists>t. \<forall>n. t n \<in> S n"
+    using choice[of "\<lambda>n x. x \<in> S n"] by auto
+  then obtain t where t: "\<forall>n. t n \<in> S n" by auto
+  {
+    fix e :: real
+    assume "e > 0"
+    then obtain N where N: "\<forall>x\<in>S N. \<forall>y\<in>S N. dist x y < e"
+      using assms(4) by blast
+    {
+      fix m n :: nat
+      assume "N \<le> m \<and> N \<le> n"
+      then have "t m \<in> S N" "t n \<in> S N"
+        using assms(3) t unfolding  subset_eq t by blast+
+      then have "dist (t m) (t n) < e"
+        using N by auto
+    }
+    then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (t m) (t n) < e"
+      by auto
+  }
+  then have "Cauchy t"
+    unfolding cauchy_def by auto
+  then obtain l where l:"(t \<longlongrightarrow> l) sequentially"
+    using complete_UNIV unfolding complete_def by auto
+  { fix n :: nat
+    { fix e :: real
+      assume "e > 0"
+      then obtain N :: nat where N: "\<forall>n\<ge>N. dist (t n) l < e"
+        using l[unfolded lim_sequentially] by auto
+      have "t (max n N) \<in> S n"
+        by (meson assms(3) contra_subsetD max.cobounded1 t)
+      then have "\<exists>y\<in>S n. dist y l < e"
+        using N max.cobounded2 by blast
+    }
+    then have "l \<in> S n"
+      using closed_approachable[of "S n" l] assms(1) by auto
+  }
+  then show ?thesis
+    using that by blast
+qed
+
+text \<open>Strengthen it to the intersection actually being a singleton.\<close>
+
+lemma decreasing_closed_nest_sing:
+  fixes S :: "nat \<Rightarrow> 'a::complete_space set"
+  assumes "\<And>n. closed(S n)"
+          "\<And>n. S n \<noteq> {}"
+          "\<And>m n. m \<le> n \<Longrightarrow> S n \<subseteq> S m"
+          "\<And>e. e>0 \<Longrightarrow> \<exists>n. \<forall>x \<in> (S n). \<forall> y\<in>(S n). dist x y < e"
+  shows "\<exists>a. \<Inter>(range S) = {a}"
+proof -
+  obtain a where a: "\<forall>n. a \<in> S n"
+    using decreasing_closed_nest[of S] using assms by auto
+  { fix b
+    assume b: "b \<in> \<Inter>(range S)"
+    { fix e :: real
+      assume "e > 0"
+      then have "dist a b < e"
+        using assms(4) and b and a by blast
+    }
+    then have "dist a b = 0"
+      by (metis dist_eq_0_iff dist_nz less_le)
+  }
+  with a have "\<Inter>(range S) = {a}"
+    unfolding image_def by auto
+  then show ?thesis ..
+qed
+
+subsection%unimportant \<open>Making a continuous function avoid some value in a neighbourhood\<close>
+
+lemma continuous_within_avoid:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
+  assumes "continuous (at x within s) f"
+    and "f x \<noteq> a"
+  shows "\<exists>e>0. \<forall>y \<in> s. dist x y < e --> f y \<noteq> a"
+proof -
+  obtain U where "open U" and "f x \<in> U" and "a \<notin> U"
+    using t1_space [OF \<open>f x \<noteq> a\<close>] by fast
+  have "(f \<longlongrightarrow> f x) (at x within s)"
+    using assms(1) by (simp add: continuous_within)
+  then have "eventually (\<lambda>y. f y \<in> U) (at x within s)"
+    using \<open>open U\<close> and \<open>f x \<in> U\<close>
+    unfolding tendsto_def by fast
+  then have "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
+    using \<open>a \<notin> U\<close> by (fast elim: eventually_mono)
+  then show ?thesis
+    using \<open>f x \<noteq> a\<close> by (auto simp: dist_commute eventually_at)
+qed
+
+lemma continuous_at_avoid:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
+  assumes "continuous (at x) f"
+    and "f x \<noteq> a"
+  shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"
+  using assms continuous_within_avoid[of x UNIV f a] by simp
+
+lemma continuous_on_avoid:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
+  assumes "continuous_on s f"
+    and "x \<in> s"
+    and "f x \<noteq> a"
+  shows "\<exists>e>0. \<forall>y \<in> s. dist x y < e \<longrightarrow> f y \<noteq> a"
+  using assms(1)[unfolded continuous_on_eq_continuous_within, THEN bspec[where x=x],
+    OF assms(2)] continuous_within_avoid[of x s f a]
+  using assms(3)
+  by auto
+
+lemma continuous_on_open_avoid:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
+  assumes "continuous_on s f"
+    and "open s"
+    and "x \<in> s"
+    and "f x \<noteq> a"
+  shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"
+  using assms(1)[unfolded continuous_on_eq_continuous_at[OF assms(2)], THEN bspec[where x=x], OF assms(3)]
+  using continuous_at_avoid[of x f a] assms(4)
+  by auto
+
+
 end
\ No newline at end of file
diff -r 10644973cdde -r 42cc3609fedf src/HOL/Analysis/Elementary_Normed_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Sun Jan 06 16:27:52 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Sun Jan 06 17:54:49 2019 +0100
@@ -136,6 +136,296 @@
   qed
 qed
 
+subsection \<open>Limit Points\<close>
+
+lemma islimpt_ball:
+  fixes x y :: "'a::{real_normed_vector,perfect_space}"
+  shows "y islimpt ball x e \<longleftrightarrow> 0 < e \<and> y \<in> cball x e"
+  (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  show ?rhs if ?lhs
+  proof
+    {
+      assume "e \<le> 0"
+      then have *: "ball x e = {}"
+        using ball_eq_empty[of x e] by auto
+      have False using \<open>?lhs\<close>
+        unfolding * using islimpt_EMPTY[of y] by auto
+    }
+    then show "e > 0" by (metis not_less)
+    show "y \<in> cball x e"
+      using closed_cball[of x e] islimpt_subset[of y "ball x e" "cball x e"]
+        ball_subset_cball[of x e] \<open>?lhs\<close>
+      unfolding closed_limpt by auto
+  qed
+  show ?lhs if ?rhs
+  proof -
+    from that have "e > 0" by auto
+    {
+      fix d :: real
+      assume "d > 0"
+      have "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
+      proof (cases "d \<le> dist x y")
+        case True
+        then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
+        proof (cases "x = y")
+          case True
+          then have False
+            using \<open>d \<le> dist x y\<close> \<open>d>0\<close> by auto
+          then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
+            by auto
+        next
+          case False
+          have "dist x (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) =
+            norm (x - y + (d / (2 * norm (y - x))) *\<^sub>R (y - x))"
+            unfolding mem_cball mem_ball dist_norm diff_diff_eq2 diff_add_eq[symmetric]
+            by auto
+          also have "\<dots> = \<bar>- 1 + d / (2 * norm (x - y))\<bar> * norm (x - y)"
+            using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", symmetric, of "y - x"]
+            unfolding scaleR_minus_left scaleR_one
+            by (auto simp: norm_minus_commute)
+          also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
+            unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
+            unfolding distrib_right using \<open>x\<noteq>y\<close>  by auto
+          also have "\<dots> \<le> e - d/2" using \<open>d \<le> dist x y\<close> and \<open>d>0\<close> and \<open>?rhs\<close>
+            by (auto simp: dist_norm)
+          finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \<in> ball x e" using \<open>d>0\<close>
+            by auto
+          moreover
+          have "(d / (2*dist y x)) *\<^sub>R (y - x) \<noteq> 0"
+            using \<open>x\<noteq>y\<close>[unfolded dist_nz] \<open>d>0\<close> unfolding scaleR_eq_0_iff
+            by (auto simp: dist_commute)
+          moreover
+          have "dist (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) y < d"
+            unfolding dist_norm
+            apply simp
+            unfolding norm_minus_cancel
+            using \<open>d > 0\<close> \<open>x\<noteq>y\<close>[unfolded dist_nz] dist_commute[of x y]
+            unfolding dist_norm
+            apply auto
+            done
+          ultimately show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
+            apply (rule_tac x = "y - (d / (2*dist y x)) *\<^sub>R (y - x)" in bexI)
+            apply auto
+            done
+        qed
+      next
+        case False
+        then have "d > dist x y" by auto
+        show "\<exists>x' \<in> ball x e. x' \<noteq> y \<and> dist x' y < d"
+        proof (cases "x = y")
+          case True
+          obtain z where **: "z \<noteq> y" "dist z y < min e d"
+            using perfect_choose_dist[of "min e d" y]
+            using \<open>d > 0\<close> \<open>e>0\<close> by auto
+          show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
+            unfolding \<open>x = y\<close>
+            using \<open>z \<noteq> y\<close> **
+            apply (rule_tac x=z in bexI)
+            apply (auto simp: dist_commute)
+            done
+        next
+          case False
+          then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
+            using \<open>d>0\<close> \<open>d > dist x y\<close> \<open>?rhs\<close>
+            apply (rule_tac x=x in bexI, auto)
+            done
+        qed
+      qed
+    }
+    then show ?thesis
+      unfolding mem_cball islimpt_approachable mem_ball by auto
+  qed
+qed
+
+lemma closure_ball_lemma:
+  fixes x y :: "'a::real_normed_vector"
+  assumes "x \<noteq> y"
+  shows "y islimpt ball x (dist x y)"
+proof (rule islimptI)
+  fix T
+  assume "y \<in> T" "open T"
+  then obtain r where "0 < r" "\<forall>z. dist z y < r \<longrightarrow> z \<in> T"
+    unfolding open_dist by fast
+  (* choose point between x and y, within distance r of y. *)
+  define k where "k = min 1 (r / (2 * dist x y))"
+  define z where "z = y + scaleR k (x - y)"
+  have z_def2: "z = x + scaleR (1 - k) (y - x)"
+    unfolding z_def by (simp add: algebra_simps)
+  have "dist z y < r"
+    unfolding z_def k_def using \<open>0 < r\<close>
+    by (simp add: dist_norm min_def)
+  then have "z \<in> T"
+    using \<open>\<forall>z. dist z y < r \<longrightarrow> z \<in> T\<close> by simp
+  have "dist x z < dist x y"
+    unfolding z_def2 dist_norm
+    apply (simp add: norm_minus_commute)
+    apply (simp only: dist_norm [symmetric])
+    apply (subgoal_tac "\<bar>1 - k\<bar> * dist x y < 1 * dist x y", simp)
+    apply (rule mult_strict_right_mono)
+    apply (simp add: k_def \<open>0 < r\<close> \<open>x \<noteq> y\<close>)
+    apply (simp add: \<open>x \<noteq> y\<close>)
+    done
+  then have "z \<in> ball x (dist x y)"
+    by simp
+  have "z \<noteq> y"
+    unfolding z_def k_def using \<open>x \<noteq> y\<close> \<open>0 < r\<close>
+    by (simp add: min_def)
+  show "\<exists>z\<in>ball x (dist x y). z \<in> T \<and> z \<noteq> y"
+    using \<open>z \<in> ball x (dist x y)\<close> \<open>z \<in> T\<close> \<open>z \<noteq> y\<close>
+    by fast
+qed
+
+
+subsection \<open>Balls and Spheres in Normed Spaces\<close>
+
+lemma mem_ball_0 [simp]: "x \<in> ball 0 e \<longleftrightarrow> norm x < e"
+  for x :: "'a::real_normed_vector"
+  by (simp add: dist_norm)
+
+lemma mem_cball_0 [simp]: "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e"
+  for x :: "'a::real_normed_vector"
+  by (simp add: dist_norm)
+
+lemma closure_ball [simp]:
+  fixes x :: "'a::real_normed_vector"
+  shows "0 < e \<Longrightarrow> closure (ball x e) = cball x e"
+  apply (rule equalityI)
+  apply (rule closure_minimal)
+  apply (rule ball_subset_cball)
+  apply (rule closed_cball)
+  apply (rule subsetI, rename_tac y)
+  apply (simp add: le_less [where 'a=real])
+  apply (erule disjE)
+  apply (rule subsetD [OF closure_subset], simp)
+  apply (simp add: closure_def, clarify)
+  apply (rule closure_ball_lemma)
+  apply simp
+  done
+
+lemma mem_sphere_0 [simp]: "x \<in> sphere 0 e \<longleftrightarrow> norm x = e"
+  for x :: "'a::real_normed_vector"
+  by (simp add: dist_norm)
+
+(* In a trivial vector space, this fails for e = 0. *)
+lemma interior_cball [simp]:
+  fixes x :: "'a::{real_normed_vector, perfect_space}"
+  shows "interior (cball x e) = ball x e"
+proof (cases "e \<ge> 0")
+  case False note cs = this
+  from cs have null: "ball x e = {}"
+    using ball_empty[of e x] by auto
+  moreover
+  have "cball x e = {}"
+  proof (rule equals0I)
+    fix y
+    assume "y \<in> cball x e"
+    then show False
+      by (metis ball_eq_empty null cs dist_eq_0_iff dist_le_zero_iff empty_subsetI mem_cball
+          subset_antisym subset_ball)
+  qed
+  then have "interior (cball x e) = {}"
+    using interior_empty by auto
+  ultimately show ?thesis by blast
+next
+  case True note cs = this
+  have "ball x e \<subseteq> cball x e"
+    using ball_subset_cball by auto
+  moreover
+  {
+    fix S y
+    assume as: "S \<subseteq> cball x e" "open S" "y\<in>S"
+    then obtain d where "d>0" and d: "\<forall>x'. dist x' y < d \<longrightarrow> x' \<in> S"
+      unfolding open_dist by blast
+    then obtain xa where xa_y: "xa \<noteq> y" and xa: "dist xa y < d"
+      using perfect_choose_dist [of d] by auto
+    have "xa \<in> S"
+      using d[THEN spec[where x = xa]]
+      using xa by (auto simp: dist_commute)
+    then have xa_cball: "xa \<in> cball x e"
+      using as(1) by auto
+    then have "y \<in> ball x e"
+    proof (cases "x = y")
+      case True
+      then have "e > 0" using cs order.order_iff_strict xa_cball xa_y by fastforce
+      then show "y \<in> ball x e"
+        using \<open>x = y \<close> by simp
+    next
+      case False
+      have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) y < d"
+        unfolding dist_norm
+        using \<open>d>0\<close> norm_ge_zero[of "y - x"] \<open>x \<noteq> y\<close> by auto
+      then have *: "y + (d / 2 / dist y x) *\<^sub>R (y - x) \<in> cball x e"
+        using d as(1)[unfolded subset_eq] by blast
+      have "y - x \<noteq> 0" using \<open>x \<noteq> y\<close> by auto
+      hence **:"d / (2 * norm (y - x)) > 0"
+        unfolding zero_less_norm_iff[symmetric] using \<open>d>0\<close> by auto
+      have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) x =
+        norm (y + (d / (2 * norm (y - x))) *\<^sub>R y - (d / (2 * norm (y - x))) *\<^sub>R x - x)"
+        by (auto simp: dist_norm algebra_simps)
+      also have "\<dots> = norm ((1 + d / (2 * norm (y - x))) *\<^sub>R (y - x))"
+        by (auto simp: algebra_simps)
+      also have "\<dots> = \<bar>1 + d / (2 * norm (y - x))\<bar> * norm (y - x)"
+        using ** by auto
+      also have "\<dots> = (dist y x) + d/2"
+        using ** by (auto simp: distrib_right dist_norm)
+      finally have "e \<ge> dist x y +d/2"
+        using *[unfolded mem_cball] by (auto simp: dist_commute)
+      then show "y \<in> ball x e"
+        unfolding mem_ball using \<open>d>0\<close> by auto
+    qed
+  }
+  then have "\<forall>S \<subseteq> cball x e. open S \<longrightarrow> S \<subseteq> ball x e"
+    by auto
+  ultimately show ?thesis
+    using interior_unique[of "ball x e" "cball x e"]
+    using open_ball[of x e]
+    by auto
+qed
+
+lemma frontier_ball [simp]:
+  fixes a :: "'a::real_normed_vector"
+  shows "0 < e \<Longrightarrow> frontier (ball a e) = sphere a e"
+  by (force simp: frontier_def)
+
+lemma frontier_cball [simp]:
+  fixes a :: "'a::{real_normed_vector, perfect_space}"
+  shows "frontier (cball a e) = sphere a e"
+  by (force simp: frontier_def)
+
+corollary compact_sphere [simp]:
+  fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
+  shows "compact (sphere a r)"
+using compact_frontier [of "cball a r"] by simp
+
+corollary bounded_sphere [simp]:
+  fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
+  shows "bounded (sphere a r)"
+by (simp add: compact_imp_bounded)
+
+corollary closed_sphere  [simp]:
+  fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
+  shows "closed (sphere a r)"
+by (simp add: compact_imp_closed)
+
+lemma image_add_ball [simp]:
+  fixes a :: "'a::real_normed_vector"
+  shows "(+) b ` ball a r = ball (a+b) r"
+apply (intro equalityI subsetI)
+apply (force simp: dist_norm)
+apply (rule_tac x="x-b" in image_eqI)
+apply (auto simp: dist_norm algebra_simps)
+done
+
+lemma image_add_cball [simp]:
+  fixes a :: "'a::real_normed_vector"
+  shows "(+) b ` cball a r = cball (a+b) r"
+apply (intro equalityI subsetI)
+apply (force simp: dist_norm)
+apply (rule_tac x="x-b" in image_eqI)
+apply (auto simp: dist_norm algebra_simps)
+done
+
 
 subsection%unimportant \<open>Various Lemmas on Normed Algebras\<close>
 
@@ -181,6 +471,14 @@
   apply (drule_tac x=UNIV in spec, simp)
   done
 
+lemma at_within_ball_bot_iff:
+  fixes x y :: "'a::{real_normed_vector,perfect_space}"
+  shows "at x within ball y r = bot \<longleftrightarrow> (r=0 \<or> x \<notin> cball y r)"
+  unfolding trivial_limit_within 
+  apply (auto simp add:trivial_limit_within islimpt_ball )
+  by (metis le_less_trans less_eq_real_def zero_le_dist)
+
+
 subsection \<open>Limits\<close>
 
 proposition Lim_at_infinity: "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)"
@@ -326,6 +624,19 @@
 
 subsection \<open>Boundedness\<close>
 
+lemma continuous_on_closure_norm_le:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  assumes "continuous_on (closure s) f"
+    and "\<forall>y \<in> s. norm(f y) \<le> b"
+    and "x \<in> (closure s)"
+  shows "norm (f x) \<le> b"
+proof -
+  have *: "f ` s \<subseteq> cball 0 b"
+    using assms(2)[unfolded mem_cball_0[symmetric]] by auto
+  show ?thesis
+    by (meson "*" assms(1) assms(3) closed_cball image_closure_subset image_subset_iff mem_cball_0)
+qed
+
 lemma bounded_pos: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x \<le> b)"
   apply (simp add: bounded_iff)
   apply (subgoal_tac "\<And>x (y::real). 0 < 1 + \<bar>y\<bar> \<and> (x \<le> y \<longrightarrow> x \<le> 1 + \<bar>y\<bar>)")
@@ -463,6 +774,33 @@
     shows "bounded (- S) \<Longrightarrow> \<not> bounded S"
   using bounded_Un [of S "-S"]  by (simp add: sup_compl_top)
 
+subsection%unimportant\<open>Relations among convergence and absolute convergence for power series\<close>
+
+lemma summable_imp_bounded:
+  fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
+  shows "summable f \<Longrightarrow> bounded (range f)"
+by (frule summable_LIMSEQ_zero) (simp add: convergent_imp_bounded)
+
+lemma summable_imp_sums_bounded:
+   "summable f \<Longrightarrow> bounded (range (\<lambda>n. sum f {..<n}))"
+by (auto simp: summable_def sums_def dest: convergent_imp_bounded)
+
+lemma power_series_conv_imp_absconv_weak:
+  fixes a:: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}" and w :: 'a
+  assumes sum: "summable (\<lambda>n. a n * z ^ n)" and no: "norm w < norm z"
+    shows "summable (\<lambda>n. of_real(norm(a n)) * w ^ n)"
+proof -
+  obtain M where M: "\<And>x. norm (a x * z ^ x) \<le> M"
+    using summable_imp_bounded [OF sum] by (force simp: bounded_iff)
+  then have *: "summable (\<lambda>n. norm (a n) * norm w ^ n)"
+    by (rule_tac M=M in Abel_lemma) (auto simp: norm_mult norm_power intro: no)
+  show ?thesis
+    apply (rule series_comparison_complex [of "(\<lambda>n. of_real(norm(a n) * norm w ^ n))"])
+    apply (simp only: summable_complex_of_real *)
+    apply (auto simp: norm_mult norm_power)
+    done
+qed
+
 
 subsection \<open>Normed spaces with the Heine-Borel property\<close>
 
@@ -492,6 +830,193 @@
     by (metis of_nat_le_iff Int_subset_iff \<open>K \<subseteq> S\<close> real_arch_simple subset_cball subset_trans)
 qed auto
 
+subsection \<open>Intersecting chains of compact sets and the Baire property\<close>
+
+proposition bounded_closed_chain:
+  fixes \<F> :: "'a::heine_borel set set"
+  assumes "B \<in> \<F>" "bounded B" and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> closed S" and "{} \<notin> \<F>"
+      and chain: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
+    shows "\<Inter>\<F> \<noteq> {}"
+proof -
+  have "B \<inter> \<Inter>\<F> \<noteq> {}"
+  proof (rule compact_imp_fip)
+    show "compact B" "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
+      by (simp_all add: assms compact_eq_bounded_closed)
+    show "\<lbrakk>finite \<G>; \<G> \<subseteq> \<F>\<rbrakk> \<Longrightarrow> B \<inter> \<Inter>\<G> \<noteq> {}" for \<G>
+    proof (induction \<G> rule: finite_induct)
+      case empty
+      with assms show ?case by force
+    next
+      case (insert U \<G>)
+      then have "U \<in> \<F>" and ne: "B \<inter> \<Inter>\<G> \<noteq> {}" by auto
+      then consider "B \<subseteq> U" | "U \<subseteq> B"
+          using \<open>B \<in> \<F>\<close> chain by blast
+        then show ?case
+        proof cases
+          case 1
+          then show ?thesis
+            using Int_left_commute ne by auto
+        next
+          case 2
+          have "U \<noteq> {}"
+            using \<open>U \<in> \<F>\<close> \<open>{} \<notin> \<F>\<close> by blast
+          moreover
+          have False if "\<And>x. x \<in> U \<Longrightarrow> \<exists>Y\<in>\<G>. x \<notin> Y"
+          proof -
+            have "\<And>x. x \<in> U \<Longrightarrow> \<exists>Y\<in>\<G>. Y \<subseteq> U"
+              by (metis chain contra_subsetD insert.prems insert_subset that)
+            then obtain Y where "Y \<in> \<G>" "Y \<subseteq> U"
+              by (metis all_not_in_conv \<open>U \<noteq> {}\<close>)
+            moreover obtain x where "x \<in> \<Inter>\<G>"
+              by (metis Int_emptyI ne)
+            ultimately show ?thesis
+              by (metis Inf_lower subset_eq that)
+          qed
+          with 2 show ?thesis
+            by blast
+        qed
+      qed
+  qed
+  then show ?thesis by blast
+qed
+
+corollary compact_chain:
+  fixes \<F> :: "'a::heine_borel set set"
+  assumes "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" "{} \<notin> \<F>"
+          "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
+    shows "\<Inter> \<F> \<noteq> {}"
+proof (cases "\<F> = {}")
+  case True
+  then show ?thesis by auto
+next
+  case False
+  show ?thesis
+    by (metis False all_not_in_conv assms compact_imp_bounded compact_imp_closed bounded_closed_chain)
+qed
+
+lemma compact_nest:
+  fixes F :: "'a::linorder \<Rightarrow> 'b::heine_borel set"
+  assumes F: "\<And>n. compact(F n)" "\<And>n. F n \<noteq> {}" and mono: "\<And>m n. m \<le> n \<Longrightarrow> F n \<subseteq> F m"
+  shows "\<Inter>range F \<noteq> {}"
+proof -
+  have *: "\<And>S T. S \<in> range F \<and> T \<in> range F \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
+    by (metis mono image_iff le_cases)
+  show ?thesis
+    apply (rule compact_chain [OF _ _ *])
+    using F apply (blast intro: dest: *)+
+    done
+qed
+
+text\<open>The Baire property of dense sets\<close>
+theorem Baire:
+  fixes S::"'a::{real_normed_vector,heine_borel} set"
+  assumes "closed S" "countable \<G>"
+      and ope: "\<And>T. T \<in> \<G> \<Longrightarrow> openin (subtopology euclidean S) T \<and> S \<subseteq> closure T"
+ shows "S \<subseteq> closure(\<Inter>\<G>)"
+proof (cases "\<G> = {}")
+  case True
+  then show ?thesis
+    using closure_subset by auto
+next
+  let ?g = "from_nat_into \<G>"
+  case False
+  then have gin: "?g n \<in> \<G>" for n
+    by (simp add: from_nat_into)
+  show ?thesis
+  proof (clarsimp simp: closure_approachable)
+    fix x and e::real
+    assume "x \<in> S" "0 < e"
+    obtain TF where opeF: "\<And>n. openin (subtopology euclidean S) (TF n)"
+               and ne: "\<And>n. TF n \<noteq> {}"
+               and subg: "\<And>n. S \<inter> closure(TF n) \<subseteq> ?g n"
+               and subball: "\<And>n. closure(TF n) \<subseteq> ball x e"
+               and decr: "\<And>n. TF(Suc n) \<subseteq> TF n"
+    proof -
+      have *: "\<exists>Y. (openin (subtopology euclidean S) Y \<and> Y \<noteq> {} \<and>
+                   S \<inter> closure Y \<subseteq> ?g n \<and> closure Y \<subseteq> ball x e) \<and> Y \<subseteq> U"
+        if opeU: "openin (subtopology euclidean S) U" and "U \<noteq> {}" and cloU: "closure U \<subseteq> ball x e" for U n
+      proof -
+        obtain T where T: "open T" "U = T \<inter> S"
+          using \<open>openin (subtopology euclidean S) U\<close> by (auto simp: openin_subtopology)
+        with \<open>U \<noteq> {}\<close> have "T \<inter> closure (?g n) \<noteq> {}"
+          using gin ope by fastforce
+        then have "T \<inter> ?g n \<noteq> {}"
+          using \<open>open T\<close> open_Int_closure_eq_empty by blast
+        then obtain y where "y \<in> U" "y \<in> ?g n"
+          using T ope [of "?g n", OF gin] by (blast dest:  openin_imp_subset)
+        moreover have "openin (subtopology euclidean S) (U \<inter> ?g n)"
+          using gin ope opeU by blast
+        ultimately obtain d where U: "U \<inter> ?g n \<subseteq> S" and "d > 0" and d: "ball y d \<inter> S \<subseteq> U \<inter> ?g n"
+          by (force simp: openin_contains_ball)
+        show ?thesis
+        proof (intro exI conjI)
+          show "openin (subtopology euclidean S) (S \<inter> ball y (d/2))"
+            by (simp add: openin_open_Int)
+          show "S \<inter> ball y (d/2) \<noteq> {}"
+            using \<open>0 < d\<close> \<open>y \<in> U\<close> opeU openin_imp_subset by fastforce
+          have "S \<inter> closure (S \<inter> ball y (d/2)) \<subseteq> S \<inter> closure (ball y (d/2))"
+            using closure_mono by blast
+          also have "... \<subseteq> ?g n"
+            using \<open>d > 0\<close> d by force
+          finally show "S \<inter> closure (S \<inter> ball y (d/2)) \<subseteq> ?g n" .
+          have "closure (S \<inter> ball y (d/2)) \<subseteq> S \<inter> ball y d"
+          proof -
+            have "closure (ball y (d/2)) \<subseteq> ball y d"
+              using \<open>d > 0\<close> by auto
+            then have "closure (S \<inter> ball y (d/2)) \<subseteq> ball y d"
+              by (meson closure_mono inf.cobounded2 subset_trans)
+            then show ?thesis
+              by (simp add: \<open>closed S\<close> closure_minimal)
+          qed
+          also have "...  \<subseteq> ball x e"
+            using cloU closure_subset d by blast
+          finally show "closure (S \<inter> ball y (d/2)) \<subseteq> ball x e" .
+          show "S \<inter> ball y (d/2) \<subseteq> U"
+            using ball_divide_subset_numeral d by blast
+        qed
+      qed
+      let ?\<Phi> = "\<lambda>n X. openin (subtopology euclidean S) X \<and> X \<noteq> {} \<and>
+                      S \<inter> closure X \<subseteq> ?g n \<and> closure X \<subseteq> ball x e"
+      have "closure (S \<inter> ball x (e / 2)) \<subseteq> closure(ball x (e/2))"
+        by (simp add: closure_mono)
+      also have "...  \<subseteq> ball x e"
+        using \<open>e > 0\<close> by auto
+      finally have "closure (S \<inter> ball x (e / 2)) \<subseteq> ball x e" .
+      moreover have"openin (subtopology euclidean S) (S \<inter> ball x (e / 2))" "S \<inter> ball x (e / 2) \<noteq> {}"
+        using \<open>0 < e\<close> \<open>x \<in> S\<close> by auto
+      ultimately obtain Y where Y: "?\<Phi> 0 Y \<and> Y \<subseteq> S \<inter> ball x (e / 2)"
+            using * [of "S \<inter> ball x (e/2)" 0] by metis
+      show thesis
+      proof (rule exE [OF dependent_nat_choice [of ?\<Phi> "\<lambda>n X Y. Y \<subseteq> X"]])
+        show "\<exists>x. ?\<Phi> 0 x"
+          using Y by auto
+        show "\<exists>Y. ?\<Phi> (Suc n) Y \<and> Y \<subseteq> X" if "?\<Phi> n X" for X n
+          using that by (blast intro: *)
+      qed (use that in metis)
+    qed
+    have "(\<Inter>n. S \<inter> closure (TF n)) \<noteq> {}"
+    proof (rule compact_nest)
+      show "\<And>n. compact (S \<inter> closure (TF n))"
+        by (metis closed_closure subball bounded_subset_ballI compact_eq_bounded_closed closed_Int_compact [OF \<open>closed S\<close>])
+      show "\<And>n. S \<inter> closure (TF n) \<noteq> {}"
+        by (metis Int_absorb1 opeF \<open>closed S\<close> closure_eq_empty closure_minimal ne openin_imp_subset)
+      show "\<And>m n. m \<le> n \<Longrightarrow> S \<inter> closure (TF n) \<subseteq> S \<inter> closure (TF m)"
+        by (meson closure_mono decr dual_order.refl inf_mono lift_Suc_antimono_le)
+    qed
+    moreover have "(\<Inter>n. S \<inter> closure (TF n)) \<subseteq> {y \<in> \<Inter>\<G>. dist y x < e}"
+    proof (clarsimp, intro conjI)
+      fix y
+      assume "y \<in> S" and y: "\<forall>n. y \<in> closure (TF n)"
+      then show "\<forall>T\<in>\<G>. y \<in> T"
+        by (metis Int_iff from_nat_into_surj [OF \<open>countable \<G>\<close>] set_mp subg)
+      show "dist y x < e"
+        by (metis y dist_commute mem_ball subball subsetCE)
+    qed
+    ultimately show "\<exists>y \<in> \<Inter>\<G>. dist y x < e"
+      by auto
+  qed
+qed
+
 
 subsection \<open>Continuity\<close>
 
diff -r 10644973cdde -r 42cc3609fedf src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Sun Jan 06 16:27:52 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Sun Jan 06 17:54:49 2019 +0100
@@ -2096,4 +2096,5 @@
     using T_def by (auto elim!: eventually_mono)
 qed
 
+
 end
\ No newline at end of file
diff -r 10644973cdde -r 42cc3609fedf src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Jan 06 16:27:52 2019 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Jan 06 17:54:49 2019 +0100
@@ -715,58 +715,21 @@
   using is_interval_translation[of "-c" X]
   by (metis image_cong uminus_add_conv_diff)
 
-lemma compact_lemma:
-  fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
-  assumes "bounded (range f)"
-  shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r.
-    strict_mono r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
-  by (rule compact_lemma_general[where unproj="\<lambda>e. \<Sum>i\<in>Basis. e i *\<^sub>R i"])
-     (auto intro!: assms bounded_linear_inner_left bounded_linear_image
-       simp: euclidean_representation)
+
+subsection%unimportant \<open>Bounded Projections\<close>
 
-instance%important euclidean_space \<subseteq> heine_borel
-proof%unimportant
-  fix f :: "nat \<Rightarrow> 'a"
-  assume f: "bounded (range f)"
-  then obtain l::'a and r where r: "strict_mono r"
-    and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
-    using compact_lemma [OF f] by blast
-  {
-    fix e::real
-    assume "e > 0"
-    hence "e / real_of_nat DIM('a) > 0" by (simp add: DIM_positive)
-    with l have "eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))) sequentially"
-      by simp
-    moreover
-    {
-      fix n
-      assume n: "\<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))"
-      have "dist (f (r n)) l \<le> (\<Sum>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i))"
-        apply (subst euclidean_dist_l2)
-        using zero_le_dist
-        apply (rule L2_set_le_sum)
-        done
-      also have "\<dots> < (\<Sum>i\<in>(Basis::'a set). e / (real_of_nat DIM('a)))"
-        apply (rule sum_strict_mono)
-        using n
-        apply auto
-        done
-      finally have "dist (f (r n)) l < e"
-        by auto
-    }
-    ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
-      by (rule eventually_mono)
-  }
-  then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
-    unfolding o_def tendsto_iff by simp
-  with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
-    by auto
-qed
+lemma bounded_inner_imp_bdd_above:
+  assumes "bounded s"
+    shows "bdd_above ((\<lambda>x. x \<bullet> a) ` s)"
+by (simp add: assms bounded_imp_bdd_above bounded_linear_image bounded_linear_inner_left)
 
-instance euclidean_space \<subseteq> banach ..
+lemma bounded_inner_imp_bdd_below:
+  assumes "bounded s"
+    shows "bdd_below ((\<lambda>x. x \<bullet> a) ` s)"
+by (simp add: assms bounded_imp_bdd_below bounded_linear_image bounded_linear_inner_left)
 
 
-subsubsection%unimportant \<open>Structural rules for pointwise continuity\<close>
+subsection%unimportant \<open>Structural rules for pointwise continuity\<close>
 
 lemma continuous_infnorm[continuous_intros]:
   "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))"
@@ -779,7 +742,7 @@
   using assms unfolding continuous_def by (rule tendsto_inner)
 
 
-subsubsection%unimportant \<open>Structural rules for setwise continuity\<close>
+subsection%unimportant \<open>Structural rules for setwise continuity\<close>
 
 lemma continuous_on_infnorm[continuous_intros]:
   "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
@@ -793,9 +756,7 @@
   using bounded_bilinear_inner assms
   by (rule bounded_bilinear.continuous_on)
 
-subsection%unimportant \<open>Intervals\<close>
-
-text \<open>Openness of halfspaces.\<close>
+subsection \<open>Openness of halfspaces.\<close>
 
 lemma open_halfspace_lt: "open {x. inner a x < b}"
   by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
@@ -809,7 +770,19 @@
 lemma open_halfspace_component_gt: "open {x::'a::euclidean_space. x\<bullet>i > a}"
   by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
 
-text \<open>This gives a simple derivation of limit component bounds.\<close>
+lemma eucl_less_eq_halfspaces:
+  fixes a :: "'a::euclidean_space"
+  shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
+        "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
+  by (auto simp: eucl_less_def)
+
+lemma open_Collect_eucl_less[simp, intro]:
+  fixes a :: "'a::euclidean_space"
+  shows "open {x. x <e a}" "open {x. a <e x}"
+  by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt)
+
+
+subsection \<open>Limit Component Bounds\<close>
 
 lemma open_box[intro]: "open (box a b)"
 proof -
@@ -820,40 +793,6 @@
   finally show ?thesis .
 qed
 
-instance euclidean_space \<subseteq> second_countable_topology
-proof
-  define a where "a f = (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i)" for f :: "'a \<Rightarrow> real \<times> real"
-  then have a: "\<And>f. (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i) = a f"
-    by simp
-  define b where "b f = (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i)" for f :: "'a \<Rightarrow> real \<times> real"
-  then have b: "\<And>f. (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i) = b f"
-    by simp
-  define B where "B = (\<lambda>f. box (a f) (b f)) ` (Basis \<rightarrow>\<^sub>E (\<rat> \<times> \<rat>))"
-
-  have "Ball B open" by (simp add: B_def open_box)
-  moreover have "(\<forall>A. open A \<longrightarrow> (\<exists>B'\<subseteq>B. \<Union>B' = A))"
-  proof safe
-    fix A::"'a set"
-    assume "open A"
-    show "\<exists>B'\<subseteq>B. \<Union>B' = A"
-      apply (rule exI[of _ "{b\<in>B. b \<subseteq> A}"])
-      apply (subst (3) open_UNION_box[OF \<open>open A\<close>])
-      apply (auto simp: a b B_def)
-      done
-  qed
-  ultimately
-  have "topological_basis B"
-    unfolding topological_basis_def by blast
-  moreover
-  have "countable B"
-    unfolding B_def
-    by (intro countable_image countable_PiE finite_Basis countable_SIGMA countable_rat)
-  ultimately show "\<exists>B::'a set set. countable B \<and> open = generate_topology B"
-    by (blast intro: topological_basis_imp_subbasis)
-qed
-
-instance euclidean_space \<subseteq> polish_space ..
-
 lemma closed_cbox[intro]:
   fixes a b :: "'a::euclidean_space"
   shows "closed (cbox a b)"
@@ -939,12 +878,6 @@
   shows "UNIV \<noteq> cbox a b" "UNIV \<noteq> box a b"
   using bounded_box[of a b] bounded_cbox[of a b] by force+
 
-lemma compact_cbox [simp]:
-  fixes a :: "'a::euclidean_space"
-  shows "compact (cbox a b)"
-  using bounded_closed_imp_seq_compact[of "cbox a b"] using bounded_cbox[of a b]
-  by (auto simp: compact_eq_seq_compact_metric)
-
 lemma box_midpoint:
   fixes a :: "'a::euclidean_space"
   assumes "box a b \<noteq> {}"
@@ -1107,16 +1040,259 @@
   unfolding closure_box[OF assms, symmetric]
   unfolding open_Int_closure_eq_empty[OF open_box] ..
 
-lemma eucl_less_eq_halfspaces:
+subsection \<open>Class Instances\<close>
+
+lemma compact_lemma:
+  fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
+  assumes "bounded (range f)"
+  shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r.
+    strict_mono r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
+  by (rule compact_lemma_general[where unproj="\<lambda>e. \<Sum>i\<in>Basis. e i *\<^sub>R i"])
+     (auto intro!: assms bounded_linear_inner_left bounded_linear_image
+       simp: euclidean_representation)
+
+instance%important euclidean_space \<subseteq> heine_borel
+proof%unimportant
+  fix f :: "nat \<Rightarrow> 'a"
+  assume f: "bounded (range f)"
+  then obtain l::'a and r where r: "strict_mono r"
+    and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
+    using compact_lemma [OF f] by blast
+  {
+    fix e::real
+    assume "e > 0"
+    hence "e / real_of_nat DIM('a) > 0" by (simp add: DIM_positive)
+    with l have "eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))) sequentially"
+      by simp
+    moreover
+    {
+      fix n
+      assume n: "\<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))"
+      have "dist (f (r n)) l \<le> (\<Sum>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i))"
+        apply (subst euclidean_dist_l2)
+        using zero_le_dist
+        apply (rule L2_set_le_sum)
+        done
+      also have "\<dots> < (\<Sum>i\<in>(Basis::'a set). e / (real_of_nat DIM('a)))"
+        apply (rule sum_strict_mono)
+        using n
+        apply auto
+        done
+      finally have "dist (f (r n)) l < e"
+        by auto
+    }
+    ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
+      by (rule eventually_mono)
+  }
+  then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
+    unfolding o_def tendsto_iff by simp
+  with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
+    by auto
+qed
+
+instance%important euclidean_space \<subseteq> banach ..
+
+instance euclidean_space \<subseteq> second_countable_topology
+proof
+  define a where "a f = (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i)" for f :: "'a \<Rightarrow> real \<times> real"
+  then have a: "\<And>f. (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i) = a f"
+    by simp
+  define b where "b f = (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i)" for f :: "'a \<Rightarrow> real \<times> real"
+  then have b: "\<And>f. (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i) = b f"
+    by simp
+  define B where "B = (\<lambda>f. box (a f) (b f)) ` (Basis \<rightarrow>\<^sub>E (\<rat> \<times> \<rat>))"
+
+  have "Ball B open" by (simp add: B_def open_box)
+  moreover have "(\<forall>A. open A \<longrightarrow> (\<exists>B'\<subseteq>B. \<Union>B' = A))"
+  proof safe
+    fix A::"'a set"
+    assume "open A"
+    show "\<exists>B'\<subseteq>B. \<Union>B' = A"
+      apply (rule exI[of _ "{b\<in>B. b \<subseteq> A}"])
+      apply (subst (3) open_UNION_box[OF \<open>open A\<close>])
+      apply (auto simp: a b B_def)
+      done
+  qed
+  ultimately
+  have "topological_basis B"
+    unfolding topological_basis_def by blast
+  moreover
+  have "countable B"
+    unfolding B_def
+    by (intro countable_image countable_PiE finite_Basis countable_SIGMA countable_rat)
+  ultimately show "\<exists>B::'a set set. countable B \<and> open = generate_topology B"
+    by (blast intro: topological_basis_imp_subbasis)
+qed
+
+instance euclidean_space \<subseteq> polish_space ..
+
+
+subsection \<open>Compact Boxes\<close>
+
+lemma compact_cbox [simp]:
   fixes a :: "'a::euclidean_space"
-  shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
-        "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
-  by (auto simp: eucl_less_def)
+  shows "compact (cbox a b)"
+  using bounded_closed_imp_seq_compact[of "cbox a b"] using bounded_cbox[of a b]
+  by (auto simp: compact_eq_seq_compact_metric)
+
+proposition is_interval_compact:
+   "is_interval S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = cbox a b)"   (is "?lhs = ?rhs")
+proof (cases "S = {}")
+  case True
+  with empty_as_interval show ?thesis by auto
+next
+  case False
+  show ?thesis
+  proof
+    assume L: ?lhs
+    then have "is_interval S" "compact S" by auto
+    define a where "a \<equiv> \<Sum>i\<in>Basis. (INF x\<in>S. x \<bullet> i) *\<^sub>R i"
+    define b where "b \<equiv> \<Sum>i\<in>Basis. (SUP x\<in>S. x \<bullet> i) *\<^sub>R i"
+    have 1: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> (INF x\<in>S. x \<bullet> i) \<le> x \<bullet> i"
+      by (simp add: cInf_lower bounded_inner_imp_bdd_below compact_imp_bounded L)
+    have 2: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)"
+      by (simp add: cSup_upper bounded_inner_imp_bdd_above compact_imp_bounded L)
+    have 3: "x \<in> S" if inf: "\<And>i. i \<in> Basis \<Longrightarrow> (INF x\<in>S. x \<bullet> i) \<le> x \<bullet> i"
+                   and sup: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)" for x
+    proof (rule mem_box_componentwiseI [OF \<open>is_interval S\<close>])
+      fix i::'a
+      assume i: "i \<in> Basis"
+      have cont: "continuous_on S (\<lambda>x. x \<bullet> i)"
+        by (intro continuous_intros)
+      obtain a where "a \<in> S" and a: "\<And>y. y\<in>S \<Longrightarrow> a \<bullet> i \<le> y \<bullet> i"
+        using continuous_attains_inf [OF \<open>compact S\<close> False cont] by blast
+      obtain b where "b \<in> S" and b: "\<And>y. y\<in>S \<Longrightarrow> y \<bullet> i \<le> b \<bullet> i"
+        using continuous_attains_sup [OF \<open>compact S\<close> False cont] by blast
+      have "a \<bullet> i \<le> (INF x\<in>S. x \<bullet> i)"
+        by (simp add: False a cINF_greatest)
+      also have "\<dots> \<le> x \<bullet> i"
+        by (simp add: i inf)
+      finally have ai: "a \<bullet> i \<le> x \<bullet> i" .
+      have "x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)"
+        by (simp add: i sup)
+      also have "(SUP x\<in>S. x \<bullet> i) \<le> b \<bullet> i"
+        by (simp add: False b cSUP_least)
+      finally have bi: "x \<bullet> i \<le> b \<bullet> i" .
+      show "x \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` S"
+        apply (rule_tac x="\<Sum>j\<in>Basis. (if j = i then x \<bullet> i else a \<bullet> j) *\<^sub>R j" in image_eqI)
+        apply (simp add: i)
+        apply (rule mem_is_intervalI [OF \<open>is_interval S\<close> \<open>a \<in> S\<close> \<open>b \<in> S\<close>])
+        using i ai bi apply force
+        done
+    qed
+    have "S = cbox a b"
+      by (auto simp: a_def b_def mem_box intro: 1 2 3)
+    then show ?rhs
+      by blast
+  next
+    assume R: ?rhs
+    then show ?lhs
+      using compact_cbox is_interval_cbox by blast
+  qed
+qed
+
+
+subsection%unimportant\<open>Relating linear images to open/closed/interior/closure\<close>
 
-lemma open_Collect_eucl_less[simp, intro]:
-  fixes a :: "'a::euclidean_space"
-  shows "open {x. x <e a}" "open {x. a <e x}"
-  by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt)
+proposition open_surjective_linear_image:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
+  assumes "open A" "linear f" "surj f"
+    shows "open(f ` A)"
+unfolding open_dist
+proof clarify
+  fix x
+  assume "x \<in> A"
+  have "bounded (inv f ` Basis)"
+    by (simp add: finite_imp_bounded)
+  with bounded_pos obtain B where "B > 0" and B: "\<And>x. x \<in> inv f ` Basis \<Longrightarrow> norm x \<le> B"
+    by metis
+  obtain e where "e > 0" and e: "\<And>z. dist z x < e \<Longrightarrow> z \<in> A"
+    by (metis open_dist \<open>x \<in> A\<close> \<open>open A\<close>)
+  define \<delta> where "\<delta> \<equiv> e / B / DIM('b)"
+  show "\<exists>e>0. \<forall>y. dist y (f x) < e \<longrightarrow> y \<in> f ` A"
+  proof (intro exI conjI)
+    show "\<delta> > 0"
+      using \<open>e > 0\<close> \<open>B > 0\<close>  by (simp add: \<delta>_def divide_simps)
+    have "y \<in> f ` A" if "dist y (f x) * (B * real DIM('b)) < e" for y
+    proof -
+      define u where "u \<equiv> y - f x"
+      show ?thesis
+      proof (rule image_eqI)
+        show "y = f (x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i))"
+          apply (simp add: linear_add linear_sum linear.scaleR \<open>linear f\<close> surj_f_inv_f \<open>surj f\<close>)
+          apply (simp add: euclidean_representation u_def)
+          done
+        have "dist (x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i)) x \<le> (\<Sum>i\<in>Basis. norm ((u \<bullet> i) *\<^sub>R inv f i))"
+          by (simp add: dist_norm sum_norm_le)
+        also have "... = (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar> * norm (inv f i))"
+          by simp
+        also have "... \<le> (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar>) * B"
+          by (simp add: B sum_distrib_right sum_mono mult_left_mono)
+        also have "... \<le> DIM('b) * dist y (f x) * B"
+          apply (rule mult_right_mono [OF sum_bounded_above])
+          using \<open>0 < B\<close> by (auto simp: Basis_le_norm dist_norm u_def)
+        also have "... < e"
+          by (metis mult.commute mult.left_commute that)
+        finally show "x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i) \<in> A"
+          by (rule e)
+      qed
+    qed
+    then show "\<forall>y. dist y (f x) < \<delta> \<longrightarrow> y \<in> f ` A"
+      using \<open>e > 0\<close> \<open>B > 0\<close>
+      by (auto simp: \<delta>_def divide_simps mult_less_0_iff)
+  qed
+qed
+
+corollary open_bijective_linear_image_eq:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "linear f" "bij f"
+    shows "open(f ` A) \<longleftrightarrow> open A"
+proof
+  assume "open(f ` A)"
+  then have "open(f -` (f ` A))"
+    using assms by (force simp: linear_continuous_at linear_conv_bounded_linear continuous_open_vimage)
+  then show "open A"
+    by (simp add: assms bij_is_inj inj_vimage_image_eq)
+next
+  assume "open A"
+  then show "open(f ` A)"
+    by (simp add: assms bij_is_surj open_surjective_linear_image)
+qed
+
+corollary interior_bijective_linear_image:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "linear f" "bij f"
+  shows "interior (f ` S) = f ` interior S"  (is "?lhs = ?rhs")
+proof safe
+  fix x
+  assume x: "x \<in> ?lhs"
+  then obtain T where "open T" and "x \<in> T" and "T \<subseteq> f ` S"
+    by (metis interiorE)
+  then show "x \<in> ?rhs"
+    by (metis (no_types, hide_lams) assms subsetD interior_maximal open_bijective_linear_image_eq subset_image_iff)
+next
+  fix x
+  assume x: "x \<in> interior S"
+  then show "f x \<in> interior (f ` S)"
+    by (meson assms imageI image_mono interiorI interior_subset open_bijective_linear_image_eq open_interior)
+qed
+
+lemma interior_injective_linear_image:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
+  assumes "linear f" "inj f"
+   shows "interior(f ` S) = f ` (interior S)"
+  by (simp add: linear_injective_imp_surjective assms bijI interior_bijective_linear_image)
+
+lemma interior_surjective_linear_image:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
+  assumes "linear f" "surj f"
+   shows "interior(f ` S) = f ` (interior S)"
+  by (simp add: assms interior_injective_linear_image linear_surjective_imp_injective)
+
+lemma interior_negations:
+  fixes S :: "'a::euclidean_space set"
+  shows "interior(uminus ` S) = image uminus (interior S)"
+  by (simp add: bij_uminus interior_bijective_linear_image linear_uminus)
 
 no_notation
   eucl_less (infix "<e" 50)
diff -r 10644973cdde -r 42cc3609fedf src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Sun Jan 06 16:27:52 2019 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Sun Jan 06 17:54:49 2019 +0100
@@ -481,6 +481,36 @@
 lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = y"
   by (auto intro!: cInf_eq_non_empty intro: dense_ge_bounded)
 
+lemma Inf_insert_finite:
+  fixes S :: "'a::conditionally_complete_linorder set"
+  shows "finite S \<Longrightarrow> Inf (insert x S) = (if S = {} then x else min x (Inf S))"
+  by (simp add: cInf_eq_Min)
+
+lemma Sup_insert_finite:
+  fixes S :: "'a::conditionally_complete_linorder set"
+  shows "finite S \<Longrightarrow> Sup (insert x S) = (if S = {} then x else max x (Sup S))"
+  by (simp add: cSup_insert sup_max)
+
+lemma finite_imp_less_Inf:
+  fixes a :: "'a::conditionally_complete_linorder"
+  shows "\<lbrakk>finite X; x \<in> X; \<And>x. x\<in>X \<Longrightarrow> a < x\<rbrakk> \<Longrightarrow> a < Inf X"
+  by (induction X rule: finite_induct) (simp_all add: cInf_eq_Min Inf_insert_finite)
+
+lemma finite_less_Inf_iff:
+  fixes a :: "'a :: conditionally_complete_linorder"
+  shows "\<lbrakk>finite X; X \<noteq> {}\<rbrakk> \<Longrightarrow> a < Inf X \<longleftrightarrow> (\<forall>x \<in> X. a < x)"
+  by (auto simp: cInf_eq_Min)
+
+lemma finite_imp_Sup_less:
+  fixes a :: "'a::conditionally_complete_linorder"
+  shows "\<lbrakk>finite X; x \<in> X; \<And>x. x\<in>X \<Longrightarrow> a > x\<rbrakk> \<Longrightarrow> a > Sup X"
+  by (induction X rule: finite_induct) (simp_all add: cSup_eq_Max Sup_insert_finite)
+
+lemma finite_Sup_less_iff:
+  fixes a :: "'a :: conditionally_complete_linorder"
+  shows "\<lbrakk>finite X; X \<noteq> {}\<rbrakk> \<Longrightarrow> a > Sup X \<longleftrightarrow> (\<forall>x \<in> X. a > x)"
+  by (auto simp: cSup_eq_Max)
+
 class linear_continuum = conditionally_complete_linorder + dense_linorder +
   assumes UNIV_not_singleton: "\<exists>a b::'a. a \<noteq> b"
 begin