# HG changeset patch
# User immler
# Date 1546860668 -3600
# Node ID e502cd4d706242adb39d30330ae5518099aa73f2
# Parent  d469a1340e21ad2d5b82b41b681902bb9e51c06e
moved material from Connected.thy to more appropriate places

diff -r d469a1340e21 -r e502cd4d7062 src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Mon Jan 07 11:51:18 2019 +0100
+++ b/src/HOL/Analysis/Connected.thy	Mon Jan 07 12:31:08 2019 +0100
@@ -494,118 +494,8 @@
   using closedin_connected_component componentsE by blast
 
 
-subsection%unimportant\<open>Quotient maps\<close>
-
-lemma quotient_map_imp_continuous_open:
-  assumes T: "f ` S \<subseteq> T"
-      and ope: "\<And>U. U \<subseteq> T
-              \<Longrightarrow> (openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
-                   openin (subtopology euclidean T) U)"
-    shows "continuous_on S f"
-proof -
-  have [simp]: "S \<inter> f -` f ` S = S" by auto
-  show ?thesis
-    using ope [OF T]
-    apply (simp add: continuous_on_open)
-    by (meson ope openin_imp_subset openin_trans)
-qed
-
-lemma quotient_map_imp_continuous_closed:
-  assumes T: "f ` S \<subseteq> T"
-      and ope: "\<And>U. U \<subseteq> T
-                  \<Longrightarrow> (closedin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
-                       closedin (subtopology euclidean T) U)"
-    shows "continuous_on S f"
-proof -
-  have [simp]: "S \<inter> f -` f ` S = S" by auto
-  show ?thesis
-    using ope [OF T]
-    apply (simp add: continuous_on_closed)
-    by (metis (no_types, lifting) ope closedin_imp_subset closedin_trans)
-qed
-
-lemma open_map_imp_quotient_map:
-  assumes contf: "continuous_on S f"
-      and T: "T \<subseteq> f ` S"
-      and ope: "\<And>T. openin (subtopology euclidean S) T
-                   \<Longrightarrow> openin (subtopology euclidean (f ` S)) (f ` T)"
-    shows "openin (subtopology euclidean S) (S \<inter> f -` T) =
-           openin (subtopology euclidean (f ` S)) T"
-proof -
-  have "T = f ` (S \<inter> f -` T)"
-    using T by blast
-  then show ?thesis
-    using "ope" contf continuous_on_open by metis
-qed
-
-lemma closed_map_imp_quotient_map:
-  assumes contf: "continuous_on S f"
-      and T: "T \<subseteq> f ` S"
-      and ope: "\<And>T. closedin (subtopology euclidean S) T
-              \<Longrightarrow> closedin (subtopology euclidean (f ` S)) (f ` T)"
-    shows "openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow>
-           openin (subtopology euclidean (f ` S)) T"
-          (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  then have *: "closedin (subtopology euclidean S) (S - (S \<inter> f -` T))"
-    using closedin_diff by fastforce
-  have [simp]: "(f ` S - f ` (S - (S \<inter> f -` T))) = T"
-    using T by blast
-  show ?rhs
-    using ope [OF *, unfolded closedin_def] by auto
-next
-  assume ?rhs
-  with contf show ?lhs
-    by (auto simp: continuous_on_open)
-qed
-
-lemma continuous_right_inverse_imp_quotient_map:
-  assumes contf: "continuous_on S f" and imf: "f ` S \<subseteq> T"
-      and contg: "continuous_on T g" and img: "g ` T \<subseteq> S"
-      and fg [simp]: "\<And>y. y \<in> T \<Longrightarrow> f(g y) = y"
-      and U: "U \<subseteq> T"
-    shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
-           openin (subtopology euclidean T) U"
-          (is "?lhs = ?rhs")
-proof -
-  have f: "\<And>Z. openin (subtopology euclidean (f ` S)) Z \<Longrightarrow>
-                openin (subtopology euclidean S) (S \<inter> f -` Z)"
-  and  g: "\<And>Z. openin (subtopology euclidean (g ` T)) Z \<Longrightarrow>
-                openin (subtopology euclidean T) (T \<inter> g -` Z)"
-    using contf contg by (auto simp: continuous_on_open)
-  show ?thesis
-  proof
-    have "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = {x \<in> T. f (g x) \<in> U}"
-      using imf img by blast
-    also have "... = U"
-      using U by auto
-    finally have eq: "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = U" .
-    assume ?lhs
-    then have *: "openin (subtopology euclidean (g ` T)) (g ` T \<inter> (S \<inter> f -` U))"
-      by (meson img openin_Int openin_subtopology_Int_subset openin_subtopology_self)
-    show ?rhs
-      using g [OF *] eq by auto
-  next
-    assume rhs: ?rhs
-    show ?lhs
-      by (metis f fg image_eqI image_subset_iff imf img openin_subopen openin_subtopology_self openin_trans rhs)
-  qed
-qed
-
-lemma continuous_left_inverse_imp_quotient_map:
-  assumes "continuous_on S f"
-      and "continuous_on (f ` S) g"
-      and  "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
-      and "U \<subseteq> f ` S"
-    shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
-           openin (subtopology euclidean (f ` S)) U"
-apply (rule continuous_right_inverse_imp_quotient_map)
-using assms apply force+
-done
-
-
-subsection%unimportant \<open>Proving a function is constant by proving that a level set is open\<close>
+subsection%unimportant \<open>Proving a function is constant on a connected set
+  by proving that a level set is open\<close>
 
 lemma continuous_levelset_openin_cases:
   fixes f :: "_ \<Rightarrow> 'b::t1_space"
@@ -635,273 +525,13 @@
   by fast
 
 
-subsection%unimportant \<open>Connectedness is invariant under homeomorphisms.\<close>
+subsection%unimportant \<open>Preservation of Connectedness\<close>
 
 lemma homeomorphic_connectedness:
   assumes "s homeomorphic t"
   shows "connected s \<longleftrightarrow> connected t"
 using assms unfolding homeomorphic_def homeomorphism_def by (metis connected_continuous_image)
 
-
-subsection\<open>Various separability-type properties\<close>
-
-lemma univ_second_countable:
-  obtains \<B> :: "'a::second_countable_topology set set"
-  where "countable \<B>" "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
-       "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
-by (metis ex_countable_basis topological_basis_def)
-
-lemma subset_second_countable:
-  obtains \<B> :: "'a:: second_countable_topology set set"
-    where "countable \<B>"
-          "{} \<notin> \<B>"
-          "\<And>C. C \<in> \<B> \<Longrightarrow> openin(subtopology euclidean S) C"
-          "\<And>T. openin(subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
-proof -
-  obtain \<B> :: "'a set set"
-    where "countable \<B>"
-      and opeB: "\<And>C. C \<in> \<B> \<Longrightarrow> openin(subtopology euclidean S) C"
-      and \<B>:    "\<And>T. openin(subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
-  proof -
-    obtain \<C> :: "'a set set"
-      where "countable \<C>" and ope: "\<And>C. C \<in> \<C> \<Longrightarrow> open C"
-        and \<C>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<C> \<and> S = \<Union>U"
-      by (metis univ_second_countable that)
-    show ?thesis
-    proof
-      show "countable ((\<lambda>C. S \<inter> C) ` \<C>)"
-        by (simp add: \<open>countable \<C>\<close>)
-      show "\<And>C. C \<in> (\<inter>) S ` \<C> \<Longrightarrow> openin (subtopology euclidean S) C"
-        using ope by auto
-      show "\<And>T. openin (subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>\<subseteq>(\<inter>) S ` \<C>. T = \<Union>\<U>"
-        by (metis \<C> image_mono inf_Sup openin_open)
-    qed
-  qed
-  show ?thesis
-  proof
-    show "countable (\<B> - {{}})"
-      using \<open>countable \<B>\<close> by blast
-    show "\<And>C. \<lbrakk>C \<in> \<B> - {{}}\<rbrakk> \<Longrightarrow> openin (subtopology euclidean S) C"
-      by (simp add: \<open>\<And>C. C \<in> \<B> \<Longrightarrow> openin (subtopology euclidean S) C\<close>)
-    show "\<exists>\<U>\<subseteq>\<B> - {{}}. T = \<Union>\<U>" if "openin (subtopology euclidean S) T" for T
-      using \<B> [OF that]
-      apply clarify
-      apply (rule_tac x="\<U> - {{}}" in exI, auto)
-        done
-  qed auto
-qed
-
-lemma univ_second_countable_sequence:
-  obtains B :: "nat \<Rightarrow> 'a::euclidean_space set"
-    where "inj B" "\<And>n. open(B n)" "\<And>S. open S \<Longrightarrow> \<exists>k. S = \<Union>{B n |n. n \<in> k}"
-proof -
-  obtain \<B> :: "'a set set"
-  where "countable \<B>"
-    and opn: "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
-    and Un: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
-    using univ_second_countable by blast
-  have *: "infinite (range (\<lambda>n. ball (0::'a) (inverse(Suc n))))"
-    apply (rule Infinite_Set.range_inj_infinite)
-    apply (simp add: inj_on_def ball_eq_ball_iff)
-    done
-  have "infinite \<B>"
-  proof
-    assume "finite \<B>"
-    then have "finite (Union ` (Pow \<B>))"
-      by simp
-    then have "finite (range (\<lambda>n. ball (0::'a) (inverse(Suc n))))"
-      apply (rule rev_finite_subset)
-      by (metis (no_types, lifting) PowI image_eqI image_subset_iff Un [OF open_ball])
-    with * show False by simp
-  qed
-  obtain f :: "nat \<Rightarrow> 'a set" where "\<B> = range f" "inj f"
-    by (blast intro: countable_as_injective_image [OF \<open>countable \<B>\<close> \<open>infinite \<B>\<close>])
-  have *: "\<exists>k. S = \<Union>{f n |n. n \<in> k}" if "open S" for S
-    using Un [OF that]
-    apply clarify
-    apply (rule_tac x="f-`U" in exI)
-    using \<open>inj f\<close> \<open>\<B> = range f\<close> apply force
-    done
-  show ?thesis
-    apply (rule that [OF \<open>inj f\<close> _ *])
-    apply (auto simp: \<open>\<B> = range f\<close> opn)
-    done
-qed
-
-proposition separable:
-  fixes S :: "'a::{metric_space, second_countable_topology} set"
-  obtains T where "countable T" "T \<subseteq> S" "S \<subseteq> closure T"
-proof -
-  obtain \<B> :: "'a set set"
-    where "countable \<B>"
-      and "{} \<notin> \<B>"
-      and ope: "\<And>C. C \<in> \<B> \<Longrightarrow> openin(subtopology euclidean S) C"
-      and if_ope: "\<And>T. openin(subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
-    by (meson subset_second_countable)
-  then obtain f where f: "\<And>C. C \<in> \<B> \<Longrightarrow> f C \<in> C"
-    by (metis equals0I)
-  show ?thesis
-  proof
-    show "countable (f ` \<B>)"
-      by (simp add: \<open>countable \<B>\<close>)
-    show "f ` \<B> \<subseteq> S"
-      using ope f openin_imp_subset by blast
-    show "S \<subseteq> closure (f ` \<B>)"
-    proof (clarsimp simp: closure_approachable)
-      fix x and e::real
-      assume "x \<in> S" "0 < e"
-      have "openin (subtopology euclidean S) (S \<inter> ball x e)"
-        by (simp add: openin_Int_open)
-      with if_ope obtain \<U> where  \<U>: "\<U> \<subseteq> \<B>" "S \<inter> ball x e = \<Union>\<U>"
-        by meson
-      show "\<exists>C \<in> \<B>. dist (f C) x < e"
-      proof (cases "\<U> = {}")
-        case True
-        then show ?thesis
-          using \<open>0 < e\<close>  \<U> \<open>x \<in> S\<close> by auto
-      next
-        case False
-        then obtain C where "C \<in> \<U>" by blast
-        show ?thesis
-        proof
-          show "dist (f C) x < e"
-            by (metis Int_iff Union_iff \<U> \<open>C \<in> \<U>\<close> dist_commute f mem_ball subsetCE)
-          show "C \<in> \<B>"
-            using \<open>\<U> \<subseteq> \<B>\<close> \<open>C \<in> \<U>\<close> by blast
-        qed
-      qed
-    qed
-  qed
-qed
-
-proposition Lindelof:
-  fixes \<F> :: "'a::second_countable_topology set set"
-  assumes \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> open S"
-  obtains \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
-proof -
-  obtain \<B> :: "'a set set"
-    where "countable \<B>" "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
-      and \<B>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
-    using univ_second_countable by blast
-  define \<D> where "\<D> \<equiv> {S. S \<in> \<B> \<and> (\<exists>U. U \<in> \<F> \<and> S \<subseteq> U)}"
-  have "countable \<D>"
-    apply (rule countable_subset [OF _ \<open>countable \<B>\<close>])
-    apply (force simp: \<D>_def)
-    done
-  have "\<And>S. \<exists>U. S \<in> \<D> \<longrightarrow> U \<in> \<F> \<and> S \<subseteq> U"
-    by (simp add: \<D>_def)
-  then obtain G where G: "\<And>S. S \<in> \<D> \<longrightarrow> G S \<in> \<F> \<and> S \<subseteq> G S"
-    by metis
-  have "\<Union>\<F> \<subseteq> \<Union>\<D>"
-    unfolding \<D>_def by (blast dest: \<F> \<B>)
-  moreover have "\<Union>\<D> \<subseteq> \<Union>\<F>"
-    using \<D>_def by blast
-  ultimately have eq1: "\<Union>\<F> = \<Union>\<D>" ..
-  have eq2: "\<Union>\<D> = \<Union> (G ` \<D>)"
-    using G eq1 by auto
-  show ?thesis
-    apply (rule_tac \<F>' = "G ` \<D>" in that)
-    using G \<open>countable \<D>\<close>  apply (auto simp: eq1 eq2)
-    done
-qed
-
-lemma Lindelof_openin:
-  fixes \<F> :: "'a::second_countable_topology set set"
-  assumes "\<And>S. S \<in> \<F> \<Longrightarrow> openin (subtopology euclidean U) S"
-  obtains \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
-proof -
-  have "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>T. open T \<and> S = U \<inter> T"
-    using assms by (simp add: openin_open)
-  then obtain tf where tf: "\<And>S. S \<in> \<F> \<Longrightarrow> open (tf S) \<and> (S = U \<inter> tf S)"
-    by metis
-  have [simp]: "\<And>\<F>'. \<F>' \<subseteq> \<F> \<Longrightarrow> \<Union>\<F>' = U \<inter> \<Union>(tf ` \<F>')"
-    using tf by fastforce
-  obtain \<G> where "countable \<G> \<and> \<G> \<subseteq> tf ` \<F>" "\<Union>\<G> = \<Union>(tf ` \<F>)"
-    using tf by (force intro: Lindelof [of "tf ` \<F>"])
-  then obtain \<F>' where \<F>': "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
-    by (clarsimp simp add: countable_subset_image)
-  then show ?thesis ..
-qed
-
-lemma countable_disjoint_open_subsets:
-  fixes \<F> :: "'a::second_countable_topology set set"
-  assumes "\<And>S. S \<in> \<F> \<Longrightarrow> open S" and pw: "pairwise disjnt \<F>"
-    shows "countable \<F>"
-proof -
-  obtain \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
-    by (meson assms Lindelof)
-  with pw have "\<F> \<subseteq> insert {} \<F>'"
-    by (fastforce simp add: pairwise_def disjnt_iff)
-  then show ?thesis
-    by (simp add: \<open>countable \<F>'\<close> countable_subset)
-qed
-
-lemma countable_disjoint_nonempty_interior_subsets:
-  fixes \<F> :: "'a::second_countable_topology set set"
-  assumes pw: "pairwise disjnt \<F>" and int: "\<And>S. \<lbrakk>S \<in> \<F>; interior S = {}\<rbrakk> \<Longrightarrow> S = {}"
-  shows "countable \<F>"
-proof (rule countable_image_inj_on)
-  have "disjoint (interior ` \<F>)"
-    using pw by (simp add: disjoint_image_subset interior_subset)
-  then show "countable (interior ` \<F>)"
-    by (auto intro: countable_disjoint_open_subsets)
-  show "inj_on interior \<F>"
-    using pw apply (clarsimp simp: inj_on_def pairwise_def)
-    apply (metis disjnt_def disjnt_subset1 inf.orderE int interior_subset)
-    done
-qed
-
-lemma closedin_compact:
-   "\<lbrakk>compact S; closedin (subtopology euclidean S) T\<rbrakk> \<Longrightarrow> compact T"
-by (metis closedin_closed compact_Int_closed)
-
-lemma closedin_compact_eq:
-  fixes S :: "'a::t2_space set"
-  shows
-   "compact S
-         \<Longrightarrow> (closedin (subtopology euclidean S) T \<longleftrightarrow>
-              compact T \<and> T \<subseteq> S)"
-by (metis closedin_imp_subset closedin_compact closed_subset compact_imp_closed)
-
-lemma continuous_imp_closed_map:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
-  assumes "closedin (subtopology euclidean S) U"
-          "continuous_on S f" "f ` S = T" "compact S"
-    shows "closedin (subtopology euclidean T) (f ` U)"
-  by (metis assms closedin_compact_eq compact_continuous_image continuous_on_subset subset_image_iff)
-
-lemma continuous_imp_quotient_map:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
-  assumes "continuous_on S f" "f ` S = T" "compact S" "U \<subseteq> T"
-    shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
-           openin (subtopology euclidean T) U"
-  by (metis (no_types, lifting) assms closed_map_imp_quotient_map continuous_imp_closed_map)
-
-
-lemma open_map_restrict:
-  assumes opeU: "openin (subtopology euclidean (S \<inter> f -` T')) U"
-    and oo: "\<And>U. openin (subtopology euclidean S) U \<Longrightarrow> openin (subtopology euclidean T) (f ` U)"
-    and "T' \<subseteq> T"
-  shows "openin (subtopology euclidean T') (f ` U)"
-proof -
-  obtain V where "open V" "U = S \<inter> f -` T' \<inter> V"
-    using opeU by (auto simp: openin_open)
-  with oo [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis
-    by (fastforce simp add: openin_open)
-qed
-
-lemma closed_map_restrict:
-  assumes cloU: "closedin (subtopology euclidean (S \<inter> f -` T')) U"
-    and cc: "\<And>U. closedin (subtopology euclidean S) U \<Longrightarrow> closedin (subtopology euclidean T) (f ` U)"
-    and "T' \<subseteq> T"
-  shows "closedin (subtopology euclidean T') (f ` U)"
-proof -
-  obtain V where "closed V" "U = S \<inter> f -` T' \<inter> V"
-    using cloU by (auto simp: closedin_closed)
-  with cc [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis
-    by (fastforce simp add: closedin_closed)
-qed
-
 lemma connected_monotone_quotient_preimage:
   assumes "connected T"
       and contf: "continuous_on S f" and fim: "f ` S = T"
@@ -1124,348 +754,6 @@
     by auto
 qed
 
-subsection%unimportant\<open> Finite intersection property\<close>
-
-text\<open>Also developed in HOL's toplogical spaces theory, but the Heine-Borel type class isn't available there.\<close>
-
-lemma closed_imp_fip:
-  fixes S :: "'a::heine_borel set"
-  assumes "closed S"
-      and T: "T \<in> \<F>" "bounded T"
-      and clof: "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
-      and none: "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> S \<inter> \<Inter>\<F>' \<noteq> {}"
-    shows "S \<inter> \<Inter>\<F> \<noteq> {}"
-proof -
-  have "compact (S \<inter> T)"
-    using \<open>closed S\<close> clof compact_eq_bounded_closed T by blast
-  then have "(S \<inter> T) \<inter> \<Inter>\<F> \<noteq> {}"
-    apply (rule compact_imp_fip)
-     apply (simp add: clof)
-    by (metis Int_assoc complete_lattice_class.Inf_insert finite_insert insert_subset none \<open>T \<in> \<F>\<close>)
-  then show ?thesis by blast
-qed
-
-lemma closed_imp_fip_compact:
-  fixes S :: "'a::heine_borel set"
-  shows
-   "\<lbrakk>closed S; \<And>T. T \<in> \<F> \<Longrightarrow> compact T;
-     \<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> S \<inter> \<Inter>\<F>' \<noteq> {}\<rbrakk>
-        \<Longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}"
-by (metis Inf_greatest closed_imp_fip compact_eq_bounded_closed empty_subsetI finite.emptyI inf.orderE)
-
-lemma closed_fip_Heine_Borel:
-  fixes \<F> :: "'a::heine_borel set set"
-  assumes "closed S" "T \<in> \<F>" "bounded T"
-      and "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
-      and "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> \<Inter>\<F>' \<noteq> {}"
-    shows "\<Inter>\<F> \<noteq> {}"
-proof -
-  have "UNIV \<inter> \<Inter>\<F> \<noteq> {}"
-    using assms closed_imp_fip [OF closed_UNIV] by auto
-  then show ?thesis by simp
-qed
-
-lemma compact_fip_Heine_Borel:
-  fixes \<F> :: "'a::heine_borel set set"
-  assumes clof: "\<And>T. T \<in> \<F> \<Longrightarrow> compact T"
-      and none: "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> \<Inter>\<F>' \<noteq> {}"
-    shows "\<Inter>\<F> \<noteq> {}"
-by (metis InterI all_not_in_conv clof closed_fip_Heine_Borel compact_eq_bounded_closed none)
-
-lemma compact_sequence_with_limit:
-  fixes f :: "nat \<Rightarrow> 'a::heine_borel"
-  shows "(f \<longlongrightarrow> l) sequentially \<Longrightarrow> compact (insert l (range f))"
-apply (simp add: compact_eq_bounded_closed, auto)
-apply (simp add: convergent_imp_bounded)
-by (simp add: closed_limpt islimpt_insert sequence_unique_limpt)
-
-
-subsection%unimportant\<open>Componentwise limits and continuity\<close>
-
-text\<open>But is the premise really necessary? Need to generalise @{thm euclidean_dist_l2}\<close>
-lemma Euclidean_dist_upper: "i \<in> Basis \<Longrightarrow> dist (x \<bullet> i) (y \<bullet> i) \<le> dist x y"
-  by (metis (no_types) member_le_L2_set euclidean_dist_l2 finite_Basis)
-
-text\<open>But is the premise \<^term>\<open>i \<in> Basis\<close> really necessary?\<close>
-lemma open_preimage_inner:
-  assumes "open S" "i \<in> Basis"
-    shows "open {x. x \<bullet> i \<in> S}"
-proof (rule openI, simp)
-  fix x
-  assume x: "x \<bullet> i \<in> S"
-  with assms obtain e where "0 < e" and e: "ball (x \<bullet> i) e \<subseteq> S"
-    by (auto simp: open_contains_ball_eq)
-  have "\<exists>e>0. ball (y \<bullet> i) e \<subseteq> S" if dxy: "dist x y < e / 2" for y
-  proof (intro exI conjI)
-    have "dist (x \<bullet> i) (y \<bullet> i) < e / 2"
-      by (meson \<open>i \<in> Basis\<close> dual_order.trans Euclidean_dist_upper not_le that)
-    then have "dist (x \<bullet> i) z < e" if "dist (y \<bullet> i) z < e / 2" for z
-      by (metis dist_commute dist_triangle_half_l that)
-    then have "ball (y \<bullet> i) (e / 2) \<subseteq> ball (x \<bullet> i) e"
-      using mem_ball by blast
-      with e show "ball (y \<bullet> i) (e / 2) \<subseteq> S"
-        by (metis order_trans)
-  qed (simp add: \<open>0 < e\<close>)
-  then show "\<exists>e>0. ball x e \<subseteq> {s. s \<bullet> i \<in> S}"
-    by (metis (no_types, lifting) \<open>0 < e\<close> \<open>open S\<close> half_gt_zero_iff mem_Collect_eq mem_ball open_contains_ball_eq subsetI)
-qed
-
-proposition tendsto_componentwise_iff:
-  fixes f :: "_ \<Rightarrow> 'b::euclidean_space"
-  shows "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>i \<in> Basis. ((\<lambda>x. (f x \<bullet> i)) \<longlongrightarrow> (l \<bullet> i)) F)"
-         (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  then show ?rhs
-    unfolding tendsto_def
-    apply clarify
-    apply (drule_tac x="{s. s \<bullet> i \<in> S}" in spec)
-    apply (auto simp: open_preimage_inner)
-    done
-next
-  assume R: ?rhs
-  then have "\<And>e. e > 0 \<Longrightarrow> \<forall>i\<in>Basis. \<forall>\<^sub>F x in F. dist (f x \<bullet> i) (l \<bullet> i) < e"
-    unfolding tendsto_iff by blast
-  then have R': "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F x in F. \<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e"
-      by (simp add: eventually_ball_finite_distrib [symmetric])
-  show ?lhs
-  unfolding tendsto_iff
-  proof clarify
-    fix e::real
-    assume "0 < e"
-    have *: "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e"
-             if "\<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / real DIM('b)" for x
-    proof -
-      have "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis \<le> sum (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis"
-        by (simp add: L2_set_le_sum)
-      also have "... < DIM('b) * (e / real DIM('b))"
-        apply (rule sum_bounded_above_strict)
-        using that by auto
-      also have "... = e"
-        by (simp add: field_simps)
-      finally show "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e" .
-    qed
-    have "\<forall>\<^sub>F x in F. \<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / DIM('b)"
-      apply (rule R')
-      using \<open>0 < e\<close> by simp
-    then show "\<forall>\<^sub>F x in F. dist (f x) l < e"
-      apply (rule eventually_mono)
-      apply (subst euclidean_dist_l2)
-      using * by blast
-  qed
-qed
-
-
-corollary continuous_componentwise:
-   "continuous F f \<longleftrightarrow> (\<forall>i \<in> Basis. continuous F (\<lambda>x. (f x \<bullet> i)))"
-by (simp add: continuous_def tendsto_componentwise_iff [symmetric])
-
-corollary continuous_on_componentwise:
-  fixes S :: "'a :: t2_space set"
-  shows "continuous_on S f \<longleftrightarrow> (\<forall>i \<in> Basis. continuous_on S (\<lambda>x. (f x \<bullet> i)))"
-  apply (simp add: continuous_on_eq_continuous_within)
-  using continuous_componentwise by blast
-
-lemma linear_componentwise_iff:
-     "(linear f') \<longleftrightarrow> (\<forall>i\<in>Basis. linear (\<lambda>x. f' x \<bullet> i))"
-  apply (auto simp: linear_iff inner_left_distrib)
-   apply (metis inner_left_distrib euclidean_eq_iff)
-  by (metis euclidean_eqI inner_scaleR_left)
-
-lemma bounded_linear_componentwise_iff:
-     "(bounded_linear f') \<longleftrightarrow> (\<forall>i\<in>Basis. bounded_linear (\<lambda>x. f' x \<bullet> i))"
-     (is "?lhs = ?rhs")
-proof
-  assume ?lhs then show ?rhs
-    by (simp add: bounded_linear_inner_left_comp)
-next
-  assume ?rhs
-  then have "(\<forall>i\<in>Basis. \<exists>K. \<forall>x. \<bar>f' x \<bullet> i\<bar> \<le> norm x * K)" "linear f'"
-    by (auto simp: bounded_linear_def bounded_linear_axioms_def linear_componentwise_iff [symmetric] ball_conj_distrib)
-  then obtain F where F: "\<And>i x. i \<in> Basis \<Longrightarrow> \<bar>f' x \<bullet> i\<bar> \<le> norm x * F i"
-    by metis
-  have "norm (f' x) \<le> norm x * sum F Basis" for x
-  proof -
-    have "norm (f' x) \<le> (\<Sum>i\<in>Basis. \<bar>f' x \<bullet> i\<bar>)"
-      by (rule norm_le_l1)
-    also have "... \<le> (\<Sum>i\<in>Basis. norm x * F i)"
-      by (metis F sum_mono)
-    also have "... = norm x * sum F Basis"
-      by (simp add: sum_distrib_left)
-    finally show ?thesis .
-  qed
-  then show ?lhs
-    by (force simp: bounded_linear_def bounded_linear_axioms_def \<open>linear f'\<close>)
-qed
-
-subsection%unimportant\<open>Pasting functions together\<close>
-
-subsubsection%unimportant\<open>on open sets\<close>
-
-lemma pasting_lemma:
-  fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
-  assumes clo: "\<And>i. i \<in> I \<Longrightarrow> openin (subtopology euclidean S) (T i)"
-      and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
-      and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
-      and g: "\<And>x. x \<in> S \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
-    shows "continuous_on S g"
-proof (clarsimp simp: continuous_openin_preimage_eq)
-  fix U :: "'b set"
-  assume "open U"
-  have S: "\<And>i. i \<in> I \<Longrightarrow> (T i) \<subseteq> S"
-    using clo openin_imp_subset by blast
-  have *: "(S \<inter> g -` U) = (\<Union>i \<in> I. T i \<inter> f i -` U)"
-    using S f g by fastforce
-  show "openin (subtopology euclidean S) (S \<inter> g -` U)"
-    apply (subst *)
-    apply (rule openin_Union, clarify)
-    using \<open>open U\<close> clo cont continuous_openin_preimage_gen openin_trans by blast
-qed
-
-lemma pasting_lemma_exists:
-  fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
-  assumes S: "S \<subseteq> (\<Union>i \<in> I. T i)"
-      and clo: "\<And>i. i \<in> I \<Longrightarrow> openin (subtopology euclidean S) (T i)"
-      and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
-      and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
-    obtains g where "continuous_on S g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> S \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x"
-proof
-  show "continuous_on S (\<lambda>x. f (SOME i. i \<in> I \<and> x \<in> T i) x)"
-    apply (rule pasting_lemma [OF clo cont])
-     apply (blast intro: f)+
-    apply (metis (mono_tags, lifting) S UN_iff subsetCE someI)
-    done
-next
-  fix x i
-  assume "i \<in> I" "x \<in> S \<inter> T i"
-  then show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x"
-    by (metis (no_types, lifting) IntD2 IntI f someI_ex)
-qed
-
-subsubsection%unimportant\<open>Likewise on closed sets, with a finiteness assumption\<close>
-
-lemma pasting_lemma_closed:
-  fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
-  assumes "finite I"
-      and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin (subtopology euclidean S) (T i)"
-      and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
-      and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
-      and g: "\<And>x. x \<in> S \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
-    shows "continuous_on S g"
-proof (clarsimp simp: continuous_closedin_preimage_eq)
-  fix U :: "'b set"
-  assume "closed U"
-  have S: "\<And>i. i \<in> I \<Longrightarrow> (T i) \<subseteq> S"
-    using clo closedin_imp_subset by blast
-  have *: "(S \<inter> g -` U) = (\<Union>i \<in> I. T i \<inter> f i -` U)"
-    using S f g by fastforce
-  show "closedin (subtopology euclidean S) (S \<inter> g -` U)"
-    apply (subst *)
-    apply (rule closedin_Union)
-    using \<open>finite I\<close> apply simp
-    apply (blast intro: \<open>closed U\<close> continuous_closedin_preimage cont clo closedin_trans)
-    done
-qed
-
-lemma pasting_lemma_exists_closed:
-  fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
-  assumes "finite I"
-      and S: "S \<subseteq> (\<Union>i \<in> I. T i)"
-      and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin (subtopology euclidean S) (T i)"
-      and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
-      and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
-    obtains g where "continuous_on S g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> S \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x"
-proof
-  show "continuous_on S (\<lambda>x. f (SOME i. i \<in> I \<and> x \<in> T i) x)"
-    apply (rule pasting_lemma_closed [OF \<open>finite I\<close> clo cont])
-     apply (blast intro: f)+
-    apply (metis (mono_tags, lifting) S UN_iff subsetCE someI)
-    done
-next
-  fix x i
-  assume "i \<in> I" "x \<in> S \<inter> T i"
-  then show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x"
-    by (metis (no_types, lifting) IntD2 IntI f someI_ex)
-qed
-
-lemma tube_lemma:
-  assumes "compact K"
-  assumes "open W"
-  assumes "{x0} \<times> K \<subseteq> W"
-  shows "\<exists>X0. x0 \<in> X0 \<and> open X0 \<and> X0 \<times> K \<subseteq> W"
-proof -
-  {
-    fix y assume "y \<in> K"
-    then have "(x0, y) \<in> W" using assms by auto
-    with \<open>open W\<close>
-    have "\<exists>X0 Y. open X0 \<and> open Y \<and> x0 \<in> X0 \<and> y \<in> Y \<and> X0 \<times> Y \<subseteq> W"
-      by (rule open_prod_elim) blast
-  }
-  then obtain X0 Y where
-    *: "\<forall>y \<in> K. open (X0 y) \<and> open (Y y) \<and> x0 \<in> X0 y \<and> y \<in> Y y \<and> X0 y \<times> Y y \<subseteq> W"
-    by metis
-  from * have "\<forall>t\<in>Y ` K. open t" "K \<subseteq> \<Union>(Y ` K)" by auto
-  with \<open>compact K\<close> obtain CC where CC: "CC \<subseteq> Y ` K" "finite CC" "K \<subseteq> \<Union>CC"
-    by (meson compactE)
-  then obtain c where c: "\<And>C. C \<in> CC \<Longrightarrow> c C \<in> K \<and> C = Y (c C)"
-    by (force intro!: choice)
-  with * CC show ?thesis
-    by (force intro!: exI[where x="\<Inter>C\<in>CC. X0 (c C)"]) (* SLOW *)
-qed
-
-lemma continuous_on_prod_compactE:
-  fixes fx::"'a::topological_space \<times> 'b::topological_space \<Rightarrow> 'c::metric_space"
-    and e::real
-  assumes cont_fx: "continuous_on (U \<times> C) fx"
-  assumes "compact C"
-  assumes [intro]: "x0 \<in> U"
-  notes [continuous_intros] = continuous_on_compose2[OF cont_fx]
-  assumes "e > 0"
-  obtains X0 where "x0 \<in> X0" "open X0"
-    "\<forall>x\<in>X0 \<inter> U. \<forall>t \<in> C. dist (fx (x, t)) (fx (x0, t)) \<le> e"
-proof -
-  define psi where "psi = (\<lambda>(x, t). dist (fx (x, t)) (fx (x0, t)))"
-  define W0 where "W0 = {(x, t) \<in> U \<times> C. psi (x, t) < e}"
-  have W0_eq: "W0 = psi -` {..<e} \<inter> U \<times> C"
-    by (auto simp: vimage_def W0_def)
-  have "open {..<e}" by simp
-  have "continuous_on (U \<times> C) psi"
-    by (auto intro!: continuous_intros simp: psi_def split_beta')
-  from this[unfolded continuous_on_open_invariant, rule_format, OF \<open>open {..<e}\<close>]
-  obtain W where W: "open W" "W \<inter> U \<times> C = W0 \<inter> U \<times> C"
-    unfolding W0_eq by blast
-  have "{x0} \<times> C \<subseteq> W \<inter> U \<times> C"
-    unfolding W
-    by (auto simp: W0_def psi_def \<open>0 < e\<close>)
-  then have "{x0} \<times> C \<subseteq> W" by blast
-  from tube_lemma[OF \<open>compact C\<close> \<open>open W\<close> this]
-  obtain X0 where X0: "x0 \<in> X0" "open X0" "X0 \<times> C \<subseteq> W"
-    by blast
-
-  have "\<forall>x\<in>X0 \<inter> U. \<forall>t \<in> C. dist (fx (x, t)) (fx (x0, t)) \<le> e"
-  proof safe
-    fix x assume x: "x \<in> X0" "x \<in> U"
-    fix t assume t: "t \<in> C"
-    have "dist (fx (x, t)) (fx (x0, t)) = psi (x, t)"
-      by (auto simp: psi_def)
-    also
-    {
-      have "(x, t) \<in> X0 \<times> C"
-        using t x
-        by auto
-      also note \<open>\<dots> \<subseteq> W\<close>
-      finally have "(x, t) \<in> W" .
-      with t x have "(x, t) \<in> W \<inter> U \<times> C"
-        by blast
-      also note \<open>W \<inter> U \<times> C = W0 \<inter> U \<times> C\<close>
-      finally  have "psi (x, t) < e"
-        by (auto simp: W0_def)
-    }
-    finally show "dist (fx (x, t)) (fx (x0, t)) \<le> e" by simp
-  qed
-  from X0(1,2) this show ?thesis ..
-qed
-
 
 subsection%unimportant\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
 
@@ -1523,33 +811,6 @@
     by blast
 qed
 
-lemma finite_implies_discrete:
-  fixes S :: "'a::topological_space set"
-  assumes "finite (f ` S)"
-  shows "(\<forall>x \<in> S. \<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x))"
-proof -
-  have "\<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" if "x \<in> S" for x
-  proof (cases "f ` S - {f x} = {}")
-    case True
-    with zero_less_numeral show ?thesis
-      by (fastforce simp add: Set.image_subset_iff cong: conj_cong)
-  next
-    case False
-    then obtain z where z: "z \<in> S" "f z \<noteq> f x"
-      by blast
-    have finn: "finite {norm (z - f x) |z. z \<in> f ` S - {f x}}"
-      using assms by simp
-    then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` S - {f x}}"
-      apply (rule finite_imp_less_Inf)
-      using z apply force+
-      done
-    show ?thesis
-      by (force intro!: * cInf_le_finite [OF finn])
-  qed
-  with assms show ?thesis
-    by blast
-qed
-
 text\<open>This proof requires the existence of two separate values of the range type.\<close>
 lemma finite_range_constant_imp_connected:
   assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
@@ -1624,108 +885,4 @@
     shows "f constant_on S"
   using assms continuous_finite_range_constant_eq  by blast
 
-
-
-subsection%unimportant \<open>Continuous Extension\<close>
-
-definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
-  "clamp a b x = (if (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)
-    then (\<Sum>i\<in>Basis. (if x\<bullet>i < a\<bullet>i then a\<bullet>i else if x\<bullet>i \<le> b\<bullet>i then x\<bullet>i else b\<bullet>i) *\<^sub>R i)
-    else a)"
-
-lemma clamp_in_interval[simp]:
-  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
-  shows "clamp a b x \<in> cbox a b"
-  unfolding clamp_def
-  using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def)
-
-lemma clamp_cancel_cbox[simp]:
-  fixes x a b :: "'a::euclidean_space"
-  assumes x: "x \<in> cbox a b"
-  shows "clamp a b x = x"
-  using assms
-  by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a])
-
-lemma clamp_empty_interval:
-  assumes "i \<in> Basis" "a \<bullet> i > b \<bullet> i"
-  shows "clamp a b = (\<lambda>_. a)"
-  using assms
-  by (force simp: clamp_def[abs_def] split: if_splits intro!: ext)
-
-lemma dist_clamps_le_dist_args:
-  fixes x :: "'a::euclidean_space"
-  shows "dist (clamp a b y) (clamp a b x) \<le> dist y x"
-proof cases
-  assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
-  then have "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) \<le>
-    (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
-    by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
-  then show ?thesis
-    by (auto intro: real_sqrt_le_mono
-      simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] L2_set_def)
-qed (auto simp: clamp_def)
-
-lemma clamp_continuous_at:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
-    and x :: 'a
-  assumes f_cont: "continuous_on (cbox a b) f"
-  shows "continuous (at x) (\<lambda>x. f (clamp a b x))"
-proof cases
-  assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
-  show ?thesis
-    unfolding continuous_at_eps_delta
-  proof safe
-    fix x :: 'a
-    fix e :: real
-    assume "e > 0"
-    moreover have "clamp a b x \<in> cbox a b"
-      by (simp add: clamp_in_interval le)
-    moreover note f_cont[simplified continuous_on_iff]
-    ultimately
-    obtain d where d: "0 < d"
-      "\<And>x'. x' \<in> cbox a b \<Longrightarrow> dist x' (clamp a b x) < d \<Longrightarrow> dist (f x') (f (clamp a b x)) < e"
-      by force
-    show "\<exists>d>0. \<forall>x'. dist x' x < d \<longrightarrow>
-      dist (f (clamp a b x')) (f (clamp a b x)) < e"
-      using le
-      by (auto intro!: d clamp_in_interval dist_clamps_le_dist_args[THEN le_less_trans])
-  qed
-qed (auto simp: clamp_empty_interval)
-
-lemma clamp_continuous_on:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
-  assumes f_cont: "continuous_on (cbox a b) f"
-  shows "continuous_on S (\<lambda>x. f (clamp a b x))"
-  using assms
-  by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at)
-
-lemma clamp_bounded:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
-  assumes bounded: "bounded (f ` (cbox a b))"
-  shows "bounded (range (\<lambda>x. f (clamp a b x)))"
-proof cases
-  assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
-  from bounded obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. dist undefined x \<le> c"
-    by (auto simp: bounded_any_center[where a=undefined])
-  then show ?thesis
-    by (auto intro!: exI[where x=c] clamp_in_interval[OF le[rule_format]]
-        simp: bounded_any_center[where a=undefined])
-qed (auto simp: clamp_empty_interval image_def)
-
-
-definition ext_cont :: "('a::euclidean_space \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b"
-  where "ext_cont f a b = (\<lambda>x. f (clamp a b x))"
-
-lemma ext_cont_cancel_cbox[simp]:
-  fixes x a b :: "'a::euclidean_space"
-  assumes x: "x \<in> cbox a b"
-  shows "ext_cont f a b x = f x"
-  using assms
-  unfolding ext_cont_def
-  by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a] arg_cong[where f=f])
-
-lemma continuous_on_ext_cont[continuous_intros]:
-  "continuous_on (cbox a b) f \<Longrightarrow> continuous_on S (ext_cont f a b)"
-  by (auto intro!: clamp_continuous_on simp: ext_cont_def)
-
 end
diff -r d469a1340e21 -r e502cd4d7062 src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Mon Jan 07 11:51:18 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Mon Jan 07 12:31:08 2019 +0100
@@ -85,6 +85,18 @@
     openin (subtopology euclidean (S \<times> T)) (S' \<times> T')"
   unfolding openin_open using open_Times by blast
 
+lemma closedin_compact:
+   "\<lbrakk>compact S; closedin (subtopology euclidean S) T\<rbrakk> \<Longrightarrow> compact T"
+by (metis closedin_closed compact_Int_closed)
+
+lemma closedin_compact_eq:
+  fixes S :: "'a::t2_space set"
+  shows
+   "compact S
+         \<Longrightarrow> (closedin (subtopology euclidean S) T \<longleftrightarrow>
+              compact T \<and> T \<subseteq> S)"
+by (metis closedin_imp_subset closedin_compact closed_subset compact_imp_closed)
+
 
 subsubsection \<open>Closure\<close>
 
@@ -395,6 +407,310 @@
     by (simp add: continuous_on_closed oo)
 qed
 
+subsubsection%unimportant \<open>Seperability\<close>
+
+lemma subset_second_countable:
+  obtains \<B> :: "'a:: second_countable_topology set set"
+    where "countable \<B>"
+          "{} \<notin> \<B>"
+          "\<And>C. C \<in> \<B> \<Longrightarrow> openin(subtopology euclidean S) C"
+          "\<And>T. openin(subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
+proof -
+  obtain \<B> :: "'a set set"
+    where "countable \<B>"
+      and opeB: "\<And>C. C \<in> \<B> \<Longrightarrow> openin(subtopology euclidean S) C"
+      and \<B>:    "\<And>T. openin(subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
+  proof -
+    obtain \<C> :: "'a set set"
+      where "countable \<C>" and ope: "\<And>C. C \<in> \<C> \<Longrightarrow> open C"
+        and \<C>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<C> \<and> S = \<Union>U"
+      by (metis univ_second_countable that)
+    show ?thesis
+    proof
+      show "countable ((\<lambda>C. S \<inter> C) ` \<C>)"
+        by (simp add: \<open>countable \<C>\<close>)
+      show "\<And>C. C \<in> (\<inter>) S ` \<C> \<Longrightarrow> openin (subtopology euclidean S) C"
+        using ope by auto
+      show "\<And>T. openin (subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>\<subseteq>(\<inter>) S ` \<C>. T = \<Union>\<U>"
+        by (metis \<C> image_mono inf_Sup openin_open)
+    qed
+  qed
+  show ?thesis
+  proof
+    show "countable (\<B> - {{}})"
+      using \<open>countable \<B>\<close> by blast
+    show "\<And>C. \<lbrakk>C \<in> \<B> - {{}}\<rbrakk> \<Longrightarrow> openin (subtopology euclidean S) C"
+      by (simp add: \<open>\<And>C. C \<in> \<B> \<Longrightarrow> openin (subtopology euclidean S) C\<close>)
+    show "\<exists>\<U>\<subseteq>\<B> - {{}}. T = \<Union>\<U>" if "openin (subtopology euclidean S) T" for T
+      using \<B> [OF that]
+      apply clarify
+      apply (rule_tac x="\<U> - {{}}" in exI, auto)
+        done
+  qed auto
+qed
+
+lemma Lindelof_openin:
+  fixes \<F> :: "'a::second_countable_topology set set"
+  assumes "\<And>S. S \<in> \<F> \<Longrightarrow> openin (subtopology euclidean U) S"
+  obtains \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
+proof -
+  have "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>T. open T \<and> S = U \<inter> T"
+    using assms by (simp add: openin_open)
+  then obtain tf where tf: "\<And>S. S \<in> \<F> \<Longrightarrow> open (tf S) \<and> (S = U \<inter> tf S)"
+    by metis
+  have [simp]: "\<And>\<F>'. \<F>' \<subseteq> \<F> \<Longrightarrow> \<Union>\<F>' = U \<inter> \<Union>(tf ` \<F>')"
+    using tf by fastforce
+  obtain \<G> where "countable \<G> \<and> \<G> \<subseteq> tf ` \<F>" "\<Union>\<G> = \<Union>(tf ` \<F>)"
+    using tf by (force intro: Lindelof [of "tf ` \<F>"])
+  then obtain \<F>' where \<F>': "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
+    by (clarsimp simp add: countable_subset_image)
+  then show ?thesis ..
+qed
+
+
+subsubsection%unimportant\<open>Closed Maps\<close>
+
+lemma continuous_imp_closed_map:
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::t2_space"
+  assumes "closedin (subtopology euclidean S) U"
+          "continuous_on S f" "f ` S = T" "compact S"
+    shows "closedin (subtopology euclidean T) (f ` U)"
+  by (metis assms closedin_compact_eq compact_continuous_image continuous_on_subset subset_image_iff)
+
+lemma closed_map_restrict:
+  assumes cloU: "closedin (subtopology euclidean (S \<inter> f -` T')) U"
+    and cc: "\<And>U. closedin (subtopology euclidean S) U \<Longrightarrow> closedin (subtopology euclidean T) (f ` U)"
+    and "T' \<subseteq> T"
+  shows "closedin (subtopology euclidean T') (f ` U)"
+proof -
+  obtain V where "closed V" "U = S \<inter> f -` T' \<inter> V"
+    using cloU by (auto simp: closedin_closed)
+  with cc [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis
+    by (fastforce simp add: closedin_closed)
+qed
+
+subsubsection%unimportant\<open>Open Maps\<close>
+
+lemma open_map_restrict:
+  assumes opeU: "openin (subtopology euclidean (S \<inter> f -` T')) U"
+    and oo: "\<And>U. openin (subtopology euclidean S) U \<Longrightarrow> openin (subtopology euclidean T) (f ` U)"
+    and "T' \<subseteq> T"
+  shows "openin (subtopology euclidean T') (f ` U)"
+proof -
+  obtain V where "open V" "U = S \<inter> f -` T' \<inter> V"
+    using opeU by (auto simp: openin_open)
+  with oo [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis
+    by (fastforce simp add: openin_open)
+qed
+
+
+subsubsection%unimportant\<open>Quotient maps\<close>
+
+lemma quotient_map_imp_continuous_open:
+  assumes T: "f ` S \<subseteq> T"
+      and ope: "\<And>U. U \<subseteq> T
+              \<Longrightarrow> (openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
+                   openin (subtopology euclidean T) U)"
+    shows "continuous_on S f"
+proof -
+  have [simp]: "S \<inter> f -` f ` S = S" by auto
+  show ?thesis
+    using ope [OF T]
+    apply (simp add: continuous_on_open)
+    by (meson ope openin_imp_subset openin_trans)
+qed
+
+lemma quotient_map_imp_continuous_closed:
+  assumes T: "f ` S \<subseteq> T"
+      and ope: "\<And>U. U \<subseteq> T
+                  \<Longrightarrow> (closedin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
+                       closedin (subtopology euclidean T) U)"
+    shows "continuous_on S f"
+proof -
+  have [simp]: "S \<inter> f -` f ` S = S" by auto
+  show ?thesis
+    using ope [OF T]
+    apply (simp add: continuous_on_closed)
+    by (metis (no_types, lifting) ope closedin_imp_subset closedin_trans)
+qed
+
+lemma open_map_imp_quotient_map:
+  assumes contf: "continuous_on S f"
+      and T: "T \<subseteq> f ` S"
+      and ope: "\<And>T. openin (subtopology euclidean S) T
+                   \<Longrightarrow> openin (subtopology euclidean (f ` S)) (f ` T)"
+    shows "openin (subtopology euclidean S) (S \<inter> f -` T) =
+           openin (subtopology euclidean (f ` S)) T"
+proof -
+  have "T = f ` (S \<inter> f -` T)"
+    using T by blast
+  then show ?thesis
+    using "ope" contf continuous_on_open by metis
+qed
+
+lemma closed_map_imp_quotient_map:
+  assumes contf: "continuous_on S f"
+      and T: "T \<subseteq> f ` S"
+      and ope: "\<And>T. closedin (subtopology euclidean S) T
+              \<Longrightarrow> closedin (subtopology euclidean (f ` S)) (f ` T)"
+    shows "openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow>
+           openin (subtopology euclidean (f ` S)) T"
+          (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then have *: "closedin (subtopology euclidean S) (S - (S \<inter> f -` T))"
+    using closedin_diff by fastforce
+  have [simp]: "(f ` S - f ` (S - (S \<inter> f -` T))) = T"
+    using T by blast
+  show ?rhs
+    using ope [OF *, unfolded closedin_def] by auto
+next
+  assume ?rhs
+  with contf show ?lhs
+    by (auto simp: continuous_on_open)
+qed
+
+lemma continuous_right_inverse_imp_quotient_map:
+  assumes contf: "continuous_on S f" and imf: "f ` S \<subseteq> T"
+      and contg: "continuous_on T g" and img: "g ` T \<subseteq> S"
+      and fg [simp]: "\<And>y. y \<in> T \<Longrightarrow> f(g y) = y"
+      and U: "U \<subseteq> T"
+    shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
+           openin (subtopology euclidean T) U"
+          (is "?lhs = ?rhs")
+proof -
+  have f: "\<And>Z. openin (subtopology euclidean (f ` S)) Z \<Longrightarrow>
+                openin (subtopology euclidean S) (S \<inter> f -` Z)"
+  and  g: "\<And>Z. openin (subtopology euclidean (g ` T)) Z \<Longrightarrow>
+                openin (subtopology euclidean T) (T \<inter> g -` Z)"
+    using contf contg by (auto simp: continuous_on_open)
+  show ?thesis
+  proof
+    have "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = {x \<in> T. f (g x) \<in> U}"
+      using imf img by blast
+    also have "... = U"
+      using U by auto
+    finally have eq: "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = U" .
+    assume ?lhs
+    then have *: "openin (subtopology euclidean (g ` T)) (g ` T \<inter> (S \<inter> f -` U))"
+      by (meson img openin_Int openin_subtopology_Int_subset openin_subtopology_self)
+    show ?rhs
+      using g [OF *] eq by auto
+  next
+    assume rhs: ?rhs
+    show ?lhs
+      by (metis f fg image_eqI image_subset_iff imf img openin_subopen openin_subtopology_self openin_trans rhs)
+  qed
+qed
+
+lemma continuous_left_inverse_imp_quotient_map:
+  assumes "continuous_on S f"
+      and "continuous_on (f ` S) g"
+      and  "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
+      and "U \<subseteq> f ` S"
+    shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
+           openin (subtopology euclidean (f ` S)) U"
+apply (rule continuous_right_inverse_imp_quotient_map)
+using assms apply force+
+done
+
+lemma continuous_imp_quotient_map:
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::t2_space"
+  assumes "continuous_on S f" "f ` S = T" "compact S" "U \<subseteq> T"
+    shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
+           openin (subtopology euclidean T) U"
+  by (metis (no_types, lifting) assms closed_map_imp_quotient_map continuous_imp_closed_map)
+
+subsubsection%unimportant\<open>Pasting functions together\<close>
+
+text\<open>on open sets\<close>
+
+lemma pasting_lemma:
+  fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
+  assumes clo: "\<And>i. i \<in> I \<Longrightarrow> openin (subtopology euclidean S) (T i)"
+      and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
+      and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
+      and g: "\<And>x. x \<in> S \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
+    shows "continuous_on S g"
+proof (clarsimp simp: continuous_openin_preimage_eq)
+  fix U :: "'b set"
+  assume "open U"
+  have S: "\<And>i. i \<in> I \<Longrightarrow> (T i) \<subseteq> S"
+    using clo openin_imp_subset by blast
+  have *: "(S \<inter> g -` U) = (\<Union>i \<in> I. T i \<inter> f i -` U)"
+    using S f g by fastforce
+  show "openin (subtopology euclidean S) (S \<inter> g -` U)"
+    apply (subst *)
+    apply (rule openin_Union, clarify)
+    using \<open>open U\<close> clo cont continuous_openin_preimage_gen openin_trans by blast
+qed
+
+lemma pasting_lemma_exists:
+  fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
+  assumes S: "S \<subseteq> (\<Union>i \<in> I. T i)"
+      and clo: "\<And>i. i \<in> I \<Longrightarrow> openin (subtopology euclidean S) (T i)"
+      and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
+      and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
+    obtains g where "continuous_on S g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> S \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x"
+proof
+  show "continuous_on S (\<lambda>x. f (SOME i. i \<in> I \<and> x \<in> T i) x)"
+    apply (rule pasting_lemma [OF clo cont])
+     apply (blast intro: f)+
+    apply (metis (mono_tags, lifting) S UN_iff subsetCE someI)
+    done
+next
+  fix x i
+  assume "i \<in> I" "x \<in> S \<inter> T i"
+  then show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x"
+    by (metis (no_types, lifting) IntD2 IntI f someI_ex)
+qed
+
+text\<open>Likewise on closed sets, with a finiteness assumption\<close>
+
+lemma pasting_lemma_closed:
+  fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
+  assumes "finite I"
+      and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin (subtopology euclidean S) (T i)"
+      and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
+      and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
+      and g: "\<And>x. x \<in> S \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
+    shows "continuous_on S g"
+proof (clarsimp simp: continuous_closedin_preimage_eq)
+  fix U :: "'b set"
+  assume "closed U"
+  have S: "\<And>i. i \<in> I \<Longrightarrow> (T i) \<subseteq> S"
+    using clo closedin_imp_subset by blast
+  have *: "(S \<inter> g -` U) = (\<Union>i \<in> I. T i \<inter> f i -` U)"
+    using S f g by fastforce
+  show "closedin (subtopology euclidean S) (S \<inter> g -` U)"
+    apply (subst *)
+    apply (rule closedin_Union)
+    using \<open>finite I\<close> apply simp
+    apply (blast intro: \<open>closed U\<close> continuous_closedin_preimage cont clo closedin_trans)
+    done
+qed
+
+lemma pasting_lemma_exists_closed:
+  fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
+  assumes "finite I"
+      and S: "S \<subseteq> (\<Union>i \<in> I. T i)"
+      and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin (subtopology euclidean S) (T i)"
+      and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_on (T i) (f i)"
+      and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> S \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
+    obtains g where "continuous_on S g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> S \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x"
+proof
+  show "continuous_on S (\<lambda>x. f (SOME i. i \<in> I \<and> x \<in> T i) x)"
+    apply (rule pasting_lemma_closed [OF \<open>finite I\<close> clo cont])
+     apply (blast intro: f)+
+    apply (metis (mono_tags, lifting) S UN_iff subsetCE someI)
+    done
+next
+  fix x i
+  assume "i \<in> I" "x \<in> S \<inter> T i"
+  then show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x"
+    by (metis (no_types, lifting) IntD2 IntI f someI_ex)
+qed
+
 
 subsection \<open>Open and closed balls\<close>
 
@@ -2227,6 +2543,62 @@
   by auto
 
 
+subsection%unimportant\<open> Finite intersection property\<close>
+
+text\<open>Also developed in HOL's toplogical spaces theory, but the Heine-Borel type class isn't available there.\<close>
+
+lemma closed_imp_fip:
+  fixes S :: "'a::heine_borel set"
+  assumes "closed S"
+      and T: "T \<in> \<F>" "bounded T"
+      and clof: "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
+      and none: "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> S \<inter> \<Inter>\<F>' \<noteq> {}"
+    shows "S \<inter> \<Inter>\<F> \<noteq> {}"
+proof -
+  have "compact (S \<inter> T)"
+    using \<open>closed S\<close> clof compact_eq_bounded_closed T by blast
+  then have "(S \<inter> T) \<inter> \<Inter>\<F> \<noteq> {}"
+    apply (rule compact_imp_fip)
+     apply (simp add: clof)
+    by (metis Int_assoc complete_lattice_class.Inf_insert finite_insert insert_subset none \<open>T \<in> \<F>\<close>)
+  then show ?thesis by blast
+qed
+
+lemma closed_imp_fip_compact:
+  fixes S :: "'a::heine_borel set"
+  shows
+   "\<lbrakk>closed S; \<And>T. T \<in> \<F> \<Longrightarrow> compact T;
+     \<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> S \<inter> \<Inter>\<F>' \<noteq> {}\<rbrakk>
+        \<Longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}"
+by (metis Inf_greatest closed_imp_fip compact_eq_bounded_closed empty_subsetI finite.emptyI inf.orderE)
+
+lemma closed_fip_Heine_Borel:
+  fixes \<F> :: "'a::heine_borel set set"
+  assumes "closed S" "T \<in> \<F>" "bounded T"
+      and "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
+      and "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> \<Inter>\<F>' \<noteq> {}"
+    shows "\<Inter>\<F> \<noteq> {}"
+proof -
+  have "UNIV \<inter> \<Inter>\<F> \<noteq> {}"
+    using assms closed_imp_fip [OF closed_UNIV] by auto
+  then show ?thesis by simp
+qed
+
+lemma compact_fip_Heine_Borel:
+  fixes \<F> :: "'a::heine_borel set set"
+  assumes clof: "\<And>T. T \<in> \<F> \<Longrightarrow> compact T"
+      and none: "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> \<Inter>\<F>' \<noteq> {}"
+    shows "\<Inter>\<F> \<noteq> {}"
+by (metis InterI all_not_in_conv clof closed_fip_Heine_Borel compact_eq_bounded_closed none)
+
+lemma compact_sequence_with_limit:
+  fixes f :: "nat \<Rightarrow> 'a::heine_borel"
+  shows "(f \<longlongrightarrow> l) sequentially \<Longrightarrow> compact (insert l (range f))"
+apply (simp add: compact_eq_bounded_closed, auto)
+apply (simp add: convergent_imp_bounded)
+by (simp add: closed_limpt islimpt_insert sequence_unique_limpt)
+
+
 subsection \<open>Properties of Balls and Spheres\<close>
 
 lemma compact_cball[simp]:
diff -r d469a1340e21 -r e502cd4d7062 src/HOL/Analysis/Elementary_Normed_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Mon Jan 07 11:51:18 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Mon Jan 07 12:31:08 2019 +0100
@@ -1573,6 +1573,36 @@
   using assms homeomorphic_ball01_UNIV homeomorphic_balls(1) homeomorphic_trans zero_less_one by blast
 
 
+subsection%unimportant \<open>Discrete\<close>
+
+lemma finite_implies_discrete:
+  fixes S :: "'a::topological_space set"
+  assumes "finite (f ` S)"
+  shows "(\<forall>x \<in> S. \<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x))"
+proof -
+  have "\<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" if "x \<in> S" for x
+  proof (cases "f ` S - {f x} = {}")
+    case True
+    with zero_less_numeral show ?thesis
+      by (fastforce simp add: Set.image_subset_iff cong: conj_cong)
+  next
+    case False
+    then obtain z where z: "z \<in> S" "f z \<noteq> f x"
+      by blast
+    have finn: "finite {norm (z - f x) |z. z \<in> f ` S - {f x}}"
+      using assms by simp
+    then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` S - {f x}}"
+      apply (rule finite_imp_less_Inf)
+      using z apply force+
+      done
+    show ?thesis
+      by (force intro!: * cInf_le_finite [OF finn])
+  qed
+  with assms show ?thesis
+    by blast
+qed
+
+
 subsection%unimportant \<open>Completeness of "Isometry" (up to constant bounds)\<close>
 
 lemma cauchy_isometric:\<comment> \<open>TODO: rename lemma to \<open>Cauchy_isometric\<close>\<close>
diff -r d469a1340e21 -r e502cd4d7062 src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Mon Jan 07 11:51:18 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Mon Jan 07 12:31:08 2019 +0100
@@ -9,6 +9,7 @@
 theory Elementary_Topology
 imports
   "HOL-Library.Set_Idioms"
+  "HOL-Library.Disjoint_Sets"
   Product_Vector
 begin
 
@@ -463,13 +464,65 @@
   qed
 qed
 
+
 end
 
+lemma univ_second_countable:
+  obtains \<B> :: "'a::second_countable_topology set set"
+  where "countable \<B>" "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
+       "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
+by (metis ex_countable_basis topological_basis_def)
+
+proposition Lindelof:
+  fixes \<F> :: "'a::second_countable_topology set set"
+  assumes \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> open S"
+  obtains \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
+proof -
+  obtain \<B> :: "'a set set"
+    where "countable \<B>" "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
+      and \<B>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
+    using univ_second_countable by blast
+  define \<D> where "\<D> \<equiv> {S. S \<in> \<B> \<and> (\<exists>U. U \<in> \<F> \<and> S \<subseteq> U)}"
+  have "countable \<D>"
+    apply (rule countable_subset [OF _ \<open>countable \<B>\<close>])
+    apply (force simp: \<D>_def)
+    done
+  have "\<And>S. \<exists>U. S \<in> \<D> \<longrightarrow> U \<in> \<F> \<and> S \<subseteq> U"
+    by (simp add: \<D>_def)
+  then obtain G where G: "\<And>S. S \<in> \<D> \<longrightarrow> G S \<in> \<F> \<and> S \<subseteq> G S"
+    by metis
+  have "\<Union>\<F> \<subseteq> \<Union>\<D>"
+    unfolding \<D>_def by (blast dest: \<F> \<B>)
+  moreover have "\<Union>\<D> \<subseteq> \<Union>\<F>"
+    using \<D>_def by blast
+  ultimately have eq1: "\<Union>\<F> = \<Union>\<D>" ..
+  have eq2: "\<Union>\<D> = \<Union> (G ` \<D>)"
+    using G eq1 by auto
+  show ?thesis
+    apply (rule_tac \<F>' = "G ` \<D>" in that)
+    using G \<open>countable \<D>\<close>
+    by (auto simp: eq1 eq2)
+qed
+
+lemma countable_disjoint_open_subsets:
+  fixes \<F> :: "'a::second_countable_topology set set"
+  assumes "\<And>S. S \<in> \<F> \<Longrightarrow> open S" and pw: "pairwise disjnt \<F>"
+    shows "countable \<F>"
+proof -
+  obtain \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
+    by (meson assms Lindelof)
+  with pw have "\<F> \<subseteq> insert {} \<F>'"
+    by (fastforce simp add: pairwise_def disjnt_iff)
+  then show ?thesis
+    by (simp add: \<open>countable \<F>'\<close> countable_subset)
+qed
+
 sublocale second_countable_topology <
   countable_basis "SOME B. countable B \<and> topological_basis B"
   using someI_ex[OF ex_countable_basis]
   by unfold_locales safe
 
+
 instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology
 proof
   obtain A :: "'a set set" where "countable A" "topological_basis A"
@@ -594,6 +647,7 @@
   then show ?thesis using B(1) by auto
 qed
 
+
 subsection%important \<open>Polish spaces\<close>
 
 text \<open>Textbooks define Polish spaces as completely metrizable.
@@ -966,6 +1020,20 @@
     by (auto simp: subset_eq less_le)
 qed auto
 
+lemma countable_disjoint_nonempty_interior_subsets:
+  fixes \<F> :: "'a::second_countable_topology set set"
+  assumes pw: "pairwise disjnt \<F>" and int: "\<And>S. \<lbrakk>S \<in> \<F>; interior S = {}\<rbrakk> \<Longrightarrow> S = {}"
+  shows "countable \<F>"
+proof (rule countable_image_inj_on)
+  have "disjoint (interior ` \<F>)"
+    using pw by (simp add: disjoint_image_subset interior_subset)
+  then show "countable (interior ` \<F>)"
+    by (auto intro: countable_disjoint_open_subsets)
+  show "inj_on interior \<F>"
+    using pw apply (clarsimp simp: inj_on_def pairwise_def)
+    apply (metis disjnt_def disjnt_subset1 inf.orderE int interior_subset)
+    done
+qed
 
 subsection \<open>Closure of a Set\<close>
 
@@ -2172,6 +2240,85 @@
 qed
 
 
+lemma tube_lemma:
+  assumes "compact K"
+  assumes "open W"
+  assumes "{x0} \<times> K \<subseteq> W"
+  shows "\<exists>X0. x0 \<in> X0 \<and> open X0 \<and> X0 \<times> K \<subseteq> W"
+proof -
+  {
+    fix y assume "y \<in> K"
+    then have "(x0, y) \<in> W" using assms by auto
+    with \<open>open W\<close>
+    have "\<exists>X0 Y. open X0 \<and> open Y \<and> x0 \<in> X0 \<and> y \<in> Y \<and> X0 \<times> Y \<subseteq> W"
+      by (rule open_prod_elim) blast
+  }
+  then obtain X0 Y where
+    *: "\<forall>y \<in> K. open (X0 y) \<and> open (Y y) \<and> x0 \<in> X0 y \<and> y \<in> Y y \<and> X0 y \<times> Y y \<subseteq> W"
+    by metis
+  from * have "\<forall>t\<in>Y ` K. open t" "K \<subseteq> \<Union>(Y ` K)" by auto
+  with \<open>compact K\<close> obtain CC where CC: "CC \<subseteq> Y ` K" "finite CC" "K \<subseteq> \<Union>CC"
+    by (meson compactE)
+  then obtain c where c: "\<And>C. C \<in> CC \<Longrightarrow> c C \<in> K \<and> C = Y (c C)"
+    by (force intro!: choice)
+  with * CC show ?thesis
+    by (force intro!: exI[where x="\<Inter>C\<in>CC. X0 (c C)"]) (* SLOW *)
+qed
+
+lemma continuous_on_prod_compactE:
+  fixes fx::"'a::topological_space \<times> 'b::topological_space \<Rightarrow> 'c::metric_space"
+    and e::real
+  assumes cont_fx: "continuous_on (U \<times> C) fx"
+  assumes "compact C"
+  assumes [intro]: "x0 \<in> U"
+  notes [continuous_intros] = continuous_on_compose2[OF cont_fx]
+  assumes "e > 0"
+  obtains X0 where "x0 \<in> X0" "open X0"
+    "\<forall>x\<in>X0 \<inter> U. \<forall>t \<in> C. dist (fx (x, t)) (fx (x0, t)) \<le> e"
+proof -
+  define psi where "psi = (\<lambda>(x, t). dist (fx (x, t)) (fx (x0, t)))"
+  define W0 where "W0 = {(x, t) \<in> U \<times> C. psi (x, t) < e}"
+  have W0_eq: "W0 = psi -` {..<e} \<inter> U \<times> C"
+    by (auto simp: vimage_def W0_def)
+  have "open {..<e}" by simp
+  have "continuous_on (U \<times> C) psi"
+    by (auto intro!: continuous_intros simp: psi_def split_beta')
+  from this[unfolded continuous_on_open_invariant, rule_format, OF \<open>open {..<e}\<close>]
+  obtain W where W: "open W" "W \<inter> U \<times> C = W0 \<inter> U \<times> C"
+    unfolding W0_eq by blast
+  have "{x0} \<times> C \<subseteq> W \<inter> U \<times> C"
+    unfolding W
+    by (auto simp: W0_def psi_def \<open>0 < e\<close>)
+  then have "{x0} \<times> C \<subseteq> W" by blast
+  from tube_lemma[OF \<open>compact C\<close> \<open>open W\<close> this]
+  obtain X0 where X0: "x0 \<in> X0" "open X0" "X0 \<times> C \<subseteq> W"
+    by blast
+
+  have "\<forall>x\<in>X0 \<inter> U. \<forall>t \<in> C. dist (fx (x, t)) (fx (x0, t)) \<le> e"
+  proof safe
+    fix x assume x: "x \<in> X0" "x \<in> U"
+    fix t assume t: "t \<in> C"
+    have "dist (fx (x, t)) (fx (x0, t)) = psi (x, t)"
+      by (auto simp: psi_def)
+    also
+    {
+      have "(x, t) \<in> X0 \<times> C"
+        using t x
+        by auto
+      also note \<open>\<dots> \<subseteq> W\<close>
+      finally have "(x, t) \<in> W" .
+      with t x have "(x, t) \<in> W \<inter> U \<times> C"
+        by blast
+      also note \<open>W \<inter> U \<times> C = W0 \<inter> U \<times> C\<close>
+      finally  have "psi (x, t) < e"
+        by (auto simp: W0_def)
+    }
+    finally show "dist (fx (x, t)) (fx (x0, t)) \<le> e" by simp
+  qed
+  from X0(1,2) this show ?thesis ..
+qed
+
+
 subsection \<open>Continuity\<close>
 
 lemma continuous_at_imp_continuous_within:
diff -r d469a1340e21 -r e502cd4d7062 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Jan 07 11:51:18 2019 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Jan 07 12:31:08 2019 +0100
@@ -1586,6 +1586,313 @@
 qed
 
 
+subsection%unimportant\<open>Componentwise limits and continuity\<close>
+
+text\<open>But is the premise really necessary? Need to generalise @{thm euclidean_dist_l2}\<close>
+lemma Euclidean_dist_upper: "i \<in> Basis \<Longrightarrow> dist (x \<bullet> i) (y \<bullet> i) \<le> dist x y"
+  by (metis (no_types) member_le_L2_set euclidean_dist_l2 finite_Basis)
+
+text\<open>But is the premise \<^term>\<open>i \<in> Basis\<close> really necessary?\<close>
+lemma open_preimage_inner:
+  assumes "open S" "i \<in> Basis"
+    shows "open {x. x \<bullet> i \<in> S}"
+proof (rule openI, simp)
+  fix x
+  assume x: "x \<bullet> i \<in> S"
+  with assms obtain e where "0 < e" and e: "ball (x \<bullet> i) e \<subseteq> S"
+    by (auto simp: open_contains_ball_eq)
+  have "\<exists>e>0. ball (y \<bullet> i) e \<subseteq> S" if dxy: "dist x y < e / 2" for y
+  proof (intro exI conjI)
+    have "dist (x \<bullet> i) (y \<bullet> i) < e / 2"
+      by (meson \<open>i \<in> Basis\<close> dual_order.trans Euclidean_dist_upper not_le that)
+    then have "dist (x \<bullet> i) z < e" if "dist (y \<bullet> i) z < e / 2" for z
+      by (metis dist_commute dist_triangle_half_l that)
+    then have "ball (y \<bullet> i) (e / 2) \<subseteq> ball (x \<bullet> i) e"
+      using mem_ball by blast
+      with e show "ball (y \<bullet> i) (e / 2) \<subseteq> S"
+        by (metis order_trans)
+  qed (simp add: \<open>0 < e\<close>)
+  then show "\<exists>e>0. ball x e \<subseteq> {s. s \<bullet> i \<in> S}"
+    by (metis (no_types, lifting) \<open>0 < e\<close> \<open>open S\<close> half_gt_zero_iff mem_Collect_eq mem_ball open_contains_ball_eq subsetI)
+qed
+
+proposition tendsto_componentwise_iff:
+  fixes f :: "_ \<Rightarrow> 'b::euclidean_space"
+  shows "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>i \<in> Basis. ((\<lambda>x. (f x \<bullet> i)) \<longlongrightarrow> (l \<bullet> i)) F)"
+         (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    unfolding tendsto_def
+    apply clarify
+    apply (drule_tac x="{s. s \<bullet> i \<in> S}" in spec)
+    apply (auto simp: open_preimage_inner)
+    done
+next
+  assume R: ?rhs
+  then have "\<And>e. e > 0 \<Longrightarrow> \<forall>i\<in>Basis. \<forall>\<^sub>F x in F. dist (f x \<bullet> i) (l \<bullet> i) < e"
+    unfolding tendsto_iff by blast
+  then have R': "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F x in F. \<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e"
+      by (simp add: eventually_ball_finite_distrib [symmetric])
+  show ?lhs
+  unfolding tendsto_iff
+  proof clarify
+    fix e::real
+    assume "0 < e"
+    have *: "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e"
+             if "\<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / real DIM('b)" for x
+    proof -
+      have "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis \<le> sum (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis"
+        by (simp add: L2_set_le_sum)
+      also have "... < DIM('b) * (e / real DIM('b))"
+        apply (rule sum_bounded_above_strict)
+        using that by auto
+      also have "... = e"
+        by (simp add: field_simps)
+      finally show "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e" .
+    qed
+    have "\<forall>\<^sub>F x in F. \<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / DIM('b)"
+      apply (rule R')
+      using \<open>0 < e\<close> by simp
+    then show "\<forall>\<^sub>F x in F. dist (f x) l < e"
+      apply (rule eventually_mono)
+      apply (subst euclidean_dist_l2)
+      using * by blast
+  qed
+qed
+
+
+corollary continuous_componentwise:
+   "continuous F f \<longleftrightarrow> (\<forall>i \<in> Basis. continuous F (\<lambda>x. (f x \<bullet> i)))"
+by (simp add: continuous_def tendsto_componentwise_iff [symmetric])
+
+corollary continuous_on_componentwise:
+  fixes S :: "'a :: t2_space set"
+  shows "continuous_on S f \<longleftrightarrow> (\<forall>i \<in> Basis. continuous_on S (\<lambda>x. (f x \<bullet> i)))"
+  apply (simp add: continuous_on_eq_continuous_within)
+  using continuous_componentwise by blast
+
+lemma linear_componentwise_iff:
+     "(linear f') \<longleftrightarrow> (\<forall>i\<in>Basis. linear (\<lambda>x. f' x \<bullet> i))"
+  apply (auto simp: linear_iff inner_left_distrib)
+   apply (metis inner_left_distrib euclidean_eq_iff)
+  by (metis euclidean_eqI inner_scaleR_left)
+
+lemma bounded_linear_componentwise_iff:
+     "(bounded_linear f') \<longleftrightarrow> (\<forall>i\<in>Basis. bounded_linear (\<lambda>x. f' x \<bullet> i))"
+     (is "?lhs = ?rhs")
+proof
+  assume ?lhs then show ?rhs
+    by (simp add: bounded_linear_inner_left_comp)
+next
+  assume ?rhs
+  then have "(\<forall>i\<in>Basis. \<exists>K. \<forall>x. \<bar>f' x \<bullet> i\<bar> \<le> norm x * K)" "linear f'"
+    by (auto simp: bounded_linear_def bounded_linear_axioms_def linear_componentwise_iff [symmetric] ball_conj_distrib)
+  then obtain F where F: "\<And>i x. i \<in> Basis \<Longrightarrow> \<bar>f' x \<bullet> i\<bar> \<le> norm x * F i"
+    by metis
+  have "norm (f' x) \<le> norm x * sum F Basis" for x
+  proof -
+    have "norm (f' x) \<le> (\<Sum>i\<in>Basis. \<bar>f' x \<bullet> i\<bar>)"
+      by (rule norm_le_l1)
+    also have "... \<le> (\<Sum>i\<in>Basis. norm x * F i)"
+      by (metis F sum_mono)
+    also have "... = norm x * sum F Basis"
+      by (simp add: sum_distrib_left)
+    finally show ?thesis .
+  qed
+  then show ?lhs
+    by (force simp: bounded_linear_def bounded_linear_axioms_def \<open>linear f'\<close>)
+qed
+
+subsection%unimportant \<open>Continuous Extension\<close>
+
+definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
+  "clamp a b x = (if (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)
+    then (\<Sum>i\<in>Basis. (if x\<bullet>i < a\<bullet>i then a\<bullet>i else if x\<bullet>i \<le> b\<bullet>i then x\<bullet>i else b\<bullet>i) *\<^sub>R i)
+    else a)"
+
+lemma clamp_in_interval[simp]:
+  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
+  shows "clamp a b x \<in> cbox a b"
+  unfolding clamp_def
+  using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def)
+
+lemma clamp_cancel_cbox[simp]:
+  fixes x a b :: "'a::euclidean_space"
+  assumes x: "x \<in> cbox a b"
+  shows "clamp a b x = x"
+  using assms
+  by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a])
+
+lemma clamp_empty_interval:
+  assumes "i \<in> Basis" "a \<bullet> i > b \<bullet> i"
+  shows "clamp a b = (\<lambda>_. a)"
+  using assms
+  by (force simp: clamp_def[abs_def] split: if_splits intro!: ext)
+
+lemma dist_clamps_le_dist_args:
+  fixes x :: "'a::euclidean_space"
+  shows "dist (clamp a b y) (clamp a b x) \<le> dist y x"
+proof cases
+  assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
+  then have "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) \<le>
+    (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
+    by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
+  then show ?thesis
+    by (auto intro: real_sqrt_le_mono
+      simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] L2_set_def)
+qed (auto simp: clamp_def)
+
+lemma clamp_continuous_at:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
+    and x :: 'a
+  assumes f_cont: "continuous_on (cbox a b) f"
+  shows "continuous (at x) (\<lambda>x. f (clamp a b x))"
+proof cases
+  assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
+  show ?thesis
+    unfolding continuous_at_eps_delta
+  proof safe
+    fix x :: 'a
+    fix e :: real
+    assume "e > 0"
+    moreover have "clamp a b x \<in> cbox a b"
+      by (simp add: clamp_in_interval le)
+    moreover note f_cont[simplified continuous_on_iff]
+    ultimately
+    obtain d where d: "0 < d"
+      "\<And>x'. x' \<in> cbox a b \<Longrightarrow> dist x' (clamp a b x) < d \<Longrightarrow> dist (f x') (f (clamp a b x)) < e"
+      by force
+    show "\<exists>d>0. \<forall>x'. dist x' x < d \<longrightarrow>
+      dist (f (clamp a b x')) (f (clamp a b x)) < e"
+      using le
+      by (auto intro!: d clamp_in_interval dist_clamps_le_dist_args[THEN le_less_trans])
+  qed
+qed (auto simp: clamp_empty_interval)
+
+lemma clamp_continuous_on:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
+  assumes f_cont: "continuous_on (cbox a b) f"
+  shows "continuous_on S (\<lambda>x. f (clamp a b x))"
+  using assms
+  by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at)
+
+lemma clamp_bounded:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
+  assumes bounded: "bounded (f ` (cbox a b))"
+  shows "bounded (range (\<lambda>x. f (clamp a b x)))"
+proof cases
+  assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
+  from bounded obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. dist undefined x \<le> c"
+    by (auto simp: bounded_any_center[where a=undefined])
+  then show ?thesis
+    by (auto intro!: exI[where x=c] clamp_in_interval[OF le[rule_format]]
+        simp: bounded_any_center[where a=undefined])
+qed (auto simp: clamp_empty_interval image_def)
+
+
+definition ext_cont :: "('a::euclidean_space \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b"
+  where "ext_cont f a b = (\<lambda>x. f (clamp a b x))"
+
+lemma ext_cont_cancel_cbox[simp]:
+  fixes x a b :: "'a::euclidean_space"
+  assumes x: "x \<in> cbox a b"
+  shows "ext_cont f a b x = f x"
+  using assms
+  unfolding ext_cont_def
+  by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a] arg_cong[where f=f])
+
+lemma continuous_on_ext_cont[continuous_intros]:
+  "continuous_on (cbox a b) f \<Longrightarrow> continuous_on S (ext_cont f a b)"
+  by (auto intro!: clamp_continuous_on simp: ext_cont_def)
+
+
+subsection \<open>Separability\<close>
+
+lemma univ_second_countable_sequence:
+  obtains B :: "nat \<Rightarrow> 'a::euclidean_space set"
+    where "inj B" "\<And>n. open(B n)" "\<And>S. open S \<Longrightarrow> \<exists>k. S = \<Union>{B n |n. n \<in> k}"
+proof -
+  obtain \<B> :: "'a set set"
+  where "countable \<B>"
+    and opn: "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
+    and Un: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
+    using univ_second_countable by blast
+  have *: "infinite (range (\<lambda>n. ball (0::'a) (inverse(Suc n))))"
+    apply (rule Infinite_Set.range_inj_infinite)
+    apply (simp add: inj_on_def ball_eq_ball_iff)
+    done
+  have "infinite \<B>"
+  proof
+    assume "finite \<B>"
+    then have "finite (Union ` (Pow \<B>))"
+      by simp
+    then have "finite (range (\<lambda>n. ball (0::'a) (inverse(Suc n))))"
+      apply (rule rev_finite_subset)
+      by (metis (no_types, lifting) PowI image_eqI image_subset_iff Un [OF open_ball])
+    with * show False by simp
+  qed
+  obtain f :: "nat \<Rightarrow> 'a set" where "\<B> = range f" "inj f"
+    by (blast intro: countable_as_injective_image [OF \<open>countable \<B>\<close> \<open>infinite \<B>\<close>])
+  have *: "\<exists>k. S = \<Union>{f n |n. n \<in> k}" if "open S" for S
+    using Un [OF that]
+    apply clarify
+    apply (rule_tac x="f-`U" in exI)
+    using \<open>inj f\<close> \<open>\<B> = range f\<close> apply force
+    done
+  show ?thesis
+    apply (rule that [OF \<open>inj f\<close> _ *])
+    apply (auto simp: \<open>\<B> = range f\<close> opn)
+    done
+qed
+
+proposition separable:
+  fixes S :: "'a::{metric_space, second_countable_topology} set"
+  obtains T where "countable T" "T \<subseteq> S" "S \<subseteq> closure T"
+proof -
+  obtain \<B> :: "'a set set"
+    where "countable \<B>"
+      and "{} \<notin> \<B>"
+      and ope: "\<And>C. C \<in> \<B> \<Longrightarrow> openin(subtopology euclidean S) C"
+      and if_ope: "\<And>T. openin(subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
+    by (meson subset_second_countable)
+  then obtain f where f: "\<And>C. C \<in> \<B> \<Longrightarrow> f C \<in> C"
+    by (metis equals0I)
+  show ?thesis
+  proof
+    show "countable (f ` \<B>)"
+      by (simp add: \<open>countable \<B>\<close>)
+    show "f ` \<B> \<subseteq> S"
+      using ope f openin_imp_subset by blast
+    show "S \<subseteq> closure (f ` \<B>)"
+    proof (clarsimp simp: closure_approachable)
+      fix x and e::real
+      assume "x \<in> S" "0 < e"
+      have "openin (subtopology euclidean S) (S \<inter> ball x e)"
+        by (simp add: openin_Int_open)
+      with if_ope obtain \<U> where  \<U>: "\<U> \<subseteq> \<B>" "S \<inter> ball x e = \<Union>\<U>"
+        by meson
+      show "\<exists>C \<in> \<B>. dist (f C) x < e"
+      proof (cases "\<U> = {}")
+        case True
+        then show ?thesis
+          using \<open>0 < e\<close>  \<U> \<open>x \<in> S\<close> by auto
+      next
+        case False
+        then obtain C where "C \<in> \<U>" by blast
+        show ?thesis
+        proof
+          show "dist (f C) x < e"
+            by (metis Int_iff Union_iff \<U> \<open>C \<in> \<U>\<close> dist_commute f mem_ball subsetCE)
+          show "C \<in> \<B>"
+            using \<open>\<U> \<subseteq> \<B>\<close> \<open>C \<in> \<U>\<close> by blast
+        qed
+      qed
+    qed
+  qed
+qed
+
+
 subsection%unimportant \<open>Diameter\<close>
 
 lemma diameter_cball [simp]: