# HG changeset patch
# User wenzelm
# Date 1552942251 -3600
# Node ID 5f67c5e457e34034ba91b3175ca77103416783de
# Parent  eddcc7c726f3e57e73c59d328e19a3455874f457# Parent  79c8ff387ed1cdc380fb52da194db022aa59ac51
merged

diff -r 79c8ff387ed1 -r 5f67c5e457e3 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Mon Mar 18 21:06:26 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Mon Mar 18 21:50:51 2019 +0100
@@ -403,8 +403,12 @@
      \<Longrightarrow> closedin (subtopology X (T \<union> U)) S"
 by (simp add: closedin_subtopology) blast
 
-
-subsection \<open>The standard Euclidean topology\<close>
+lemma openin_trans_full:
+   "\<lbrakk>openin (subtopology X U) S; openin X U\<rbrakk> \<Longrightarrow> openin X S"
+  by (simp add: openin_open_subtopology)
+
+
+subsection \<open>The canonical topology from the underlying type class\<close>
 
 abbreviation%important euclidean :: "'a::topological_space topology"
   where "euclidean \<equiv> topology open"
@@ -1269,6 +1273,144 @@
   by (simp add: Diff_eq discrete_topology_closure_of frontier_of_closures)
 
 
+subsection\<open>Locally finite collections\<close>
+
+definition locally_finite_in
+  where
+ "locally_finite_in X \<A> \<longleftrightarrow>
+        (\<Union>\<A> \<subseteq> topspace X) \<and>
+        (\<forall>x \<in> topspace X. \<exists>V. openin X V \<and> x \<in> V \<and> finite {U \<in> \<A>. U \<inter> V \<noteq> {}})"
+
+lemma finite_imp_locally_finite_in:
+   "\<lbrakk>finite \<A>; \<Union>\<A> \<subseteq> topspace X\<rbrakk> \<Longrightarrow> locally_finite_in X \<A>"
+  by (auto simp: locally_finite_in_def)
+
+lemma locally_finite_in_subset:
+  assumes "locally_finite_in X \<A>" "\<B> \<subseteq> \<A>"
+  shows "locally_finite_in X \<B>"
+proof -
+  have "finite {U \<in> \<A>. U \<inter> V \<noteq> {}} \<Longrightarrow> finite {U \<in> \<B>. U \<inter> V \<noteq> {}}" for V
+    apply (erule rev_finite_subset) using \<open>\<B> \<subseteq> \<A>\<close> by blast
+  then show ?thesis
+  using assms unfolding locally_finite_in_def by (fastforce simp add:)
+qed
+
+lemma locally_finite_in_refinement:
+  assumes \<A>: "locally_finite_in X \<A>" and f: "\<And>S. S \<in> \<A> \<Longrightarrow> f S \<subseteq> S"
+  shows "locally_finite_in X (f ` \<A>)"
+proof -
+  show ?thesis
+    unfolding locally_finite_in_def
+  proof safe
+    fix x
+    assume "x \<in> topspace X"
+    then obtain V where "openin X V" "x \<in> V" "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
+      using \<A> unfolding locally_finite_in_def by blast
+    moreover have "{U \<in> \<A>. f U \<inter> V \<noteq> {}} \<subseteq> {U \<in> \<A>. U \<inter> V \<noteq> {}}" for V
+      using f by blast
+    ultimately have "finite {U \<in> \<A>. f U \<inter> V \<noteq> {}}"
+      using finite_subset by blast
+    moreover have "f ` {U \<in> \<A>. f U \<inter> V \<noteq> {}} = {U \<in> f ` \<A>. U \<inter> V \<noteq> {}}"
+      by blast
+    ultimately have "finite {U \<in> f ` \<A>. U \<inter> V \<noteq> {}}"
+      by (metis (no_types, lifting) finite_imageI)
+    then show "\<exists>V. openin X V \<and> x \<in> V \<and> finite {U \<in> f ` \<A>. U \<inter> V \<noteq> {}}"
+      using \<open>openin X V\<close> \<open>x \<in> V\<close> by blast
+  next
+    show "\<And>x xa. \<lbrakk>xa \<in> \<A>; x \<in> f xa\<rbrakk> \<Longrightarrow> x \<in> topspace X"
+      by (meson Sup_upper \<A> f locally_finite_in_def subset_iff)
+  qed
+qed
+
+lemma locally_finite_in_subtopology:
+  assumes \<A>: "locally_finite_in X \<A>" "\<Union>\<A> \<subseteq> S"
+  shows "locally_finite_in (subtopology X S) \<A>"
+  unfolding locally_finite_in_def
+proof safe
+  fix x
+  assume x: "x \<in> topspace (subtopology X S)"
+  then obtain V where "openin X V" "x \<in> V" and fin: "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
+    using \<A> unfolding locally_finite_in_def topspace_subtopology by blast
+  show "\<exists>V. openin (subtopology X S) V \<and> x \<in> V \<and> finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
+  proof (intro exI conjI)
+    show "openin (subtopology X S) (S \<inter> V)"
+      by (simp add: \<open>openin X V\<close> openin_subtopology_Int2)
+    have "{U \<in> \<A>. U \<inter> (S \<inter> V) \<noteq> {}} \<subseteq> {U \<in> \<A>. U \<inter> V \<noteq> {}}"
+      by auto
+    with fin show "finite {U \<in> \<A>. U \<inter> (S \<inter> V) \<noteq> {}}"
+      using finite_subset by auto
+    show "x \<in> S \<inter> V"
+      using x \<open>x \<in> V\<close> by (simp add: topspace_subtopology)
+  qed
+next
+  show "\<And>x A. \<lbrakk>x \<in> A; A \<in> \<A>\<rbrakk> \<Longrightarrow> x \<in> topspace (subtopology X S)"
+    using assms unfolding locally_finite_in_def topspace_subtopology by blast
+qed
+
+
+lemma closedin_locally_finite_Union:
+  assumes clo: "\<And>S. S \<in> \<A> \<Longrightarrow> closedin X S" and \<A>: "locally_finite_in X \<A>"
+  shows "closedin X (\<Union>\<A>)"
+  using \<A> unfolding locally_finite_in_def closedin_def
+proof clarify
+  show "openin X (topspace X - \<Union>\<A>)"
+  proof (subst openin_subopen, clarify)
+    fix x
+    assume "x \<in> topspace X" and "x \<notin> \<Union>\<A>"
+    then obtain V where "openin X V" "x \<in> V" and fin: "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
+      using \<A> unfolding locally_finite_in_def by blast
+    let ?T = "V - \<Union>{S \<in> \<A>. S \<inter> V \<noteq> {}}"
+    show "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> topspace X - \<Union>\<A>"
+    proof (intro exI conjI)
+      show "openin X ?T"
+        by (metis (no_types, lifting) fin \<open>openin X V\<close> clo closedin_Union mem_Collect_eq openin_diff)
+      show "x \<in> ?T"
+        using \<open>x \<notin> \<Union>\<A>\<close> \<open>x \<in> V\<close> by auto
+      show "?T \<subseteq> topspace X - \<Union>\<A>"
+        using \<open>openin X V\<close> openin_subset by auto
+    qed
+  qed
+qed
+
+lemma locally_finite_in_closure:
+  assumes \<A>: "locally_finite_in X \<A>"
+  shows "locally_finite_in X ((\<lambda>S. X closure_of S) ` \<A>)"
+  using \<A> unfolding locally_finite_in_def
+proof (intro conjI; clarsimp)
+  fix x A
+  assume "x \<in> X closure_of A"
+  then show "x \<in> topspace X"
+    by (meson in_closure_of)
+next
+  fix x
+  assume "x \<in> topspace X" and "\<Union>\<A> \<subseteq> topspace X"
+  then obtain V where V: "openin X V" "x \<in> V" and fin: "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
+    using \<A> unfolding locally_finite_in_def by blast
+  have eq: "{y \<in> f ` \<A>. Q y} = f ` {x. x \<in> \<A> \<and> Q(f x)}" for f Q
+    by blast
+  have eq2: "{A \<in> \<A>. X closure_of A \<inter> V \<noteq> {}} = {A \<in> \<A>. A \<inter> V \<noteq> {}}"
+    using openin_Int_closure_of_eq_empty V  by blast
+  have "finite {U \<in> (closure_of) X ` \<A>. U \<inter> V \<noteq> {}}"
+    by (simp add: eq eq2 fin)
+  with V show "\<exists>V. openin X V \<and> x \<in> V \<and> finite {U \<in> (closure_of) X ` \<A>. U \<inter> V \<noteq> {}}"
+    by blast
+qed
+
+lemma closedin_Union_locally_finite_closure:
+   "locally_finite_in X \<A> \<Longrightarrow> closedin X (\<Union>((\<lambda>S. X closure_of S) ` \<A>))"
+  by (metis (mono_tags) closedin_closure_of closedin_locally_finite_Union imageE locally_finite_in_closure)
+
+lemma closure_of_Union_subset: "\<Union>((\<lambda>S. X closure_of S) ` \<A>) \<subseteq> X closure_of (\<Union>\<A>)"
+  by clarify (meson Union_upper closure_of_mono subsetD)
+
+lemma closure_of_locally_finite_Union:
+   "locally_finite_in X \<A> \<Longrightarrow> X closure_of (\<Union>\<A>) = \<Union>((\<lambda>S. X closure_of S) ` \<A>)"
+  apply (rule closure_of_unique)
+  apply (simp add: SUP_upper2 Sup_le_iff closure_of_subset locally_finite_in_def)
+  apply (simp add: closedin_Union_locally_finite_closure)
+  by (simp add: Sup_le_iff closure_of_minimal)
+
+
 subsection\<open>Continuous maps\<close>
 
 definition continuous_map where
diff -r 79c8ff387ed1 -r 5f67c5e457e3 src/HOL/Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Mon Mar 18 21:06:26 2019 +0100
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Mon Mar 18 21:50:51 2019 +0100
@@ -9,6 +9,8 @@
   Topology_Euclidean_Space
   Operator_Norm
   Uniform_Limit
+  Function_Topology
+
 begin
 
 lemma onorm_componentwise:
@@ -733,4 +735,86 @@
   bounded_linear.uniform_limit[OF bounded_linear_blinfun_apply]
   bounded_linear.uniform_limit[OF bounded_linear_blinfun_matrix]
 
+
+subsection \<open>The strong operator topology on continuous linear operators\<close>
+
+text \<open>Let \<open>'a\<close> and \<open>'b\<close> be two normed real vector spaces. Then the space of linear continuous
+operators from \<open>'a\<close> to \<open>'b\<close> has a canonical norm, and therefore a canonical corresponding topology
+(the type classes instantiation are given in \<^file>\<open>Bounded_Linear_Function.thy\<close>).
+
+However, there is another topology on this space, the strong operator topology, where \<open>T\<^sub>n\<close> tends to
+\<open>T\<close> iff, for all \<open>x\<close> in \<open>'a\<close>, then \<open>T\<^sub>n x\<close> tends to \<open>T x\<close>. This is precisely the product topology
+where the target space is endowed with the norm topology. It is especially useful when \<open>'b\<close> is the set
+of real numbers, since then this topology is compact.
+
+We can not implement it using type classes as there is already a topology, but at least we
+can define it as a topology.
+
+Note that there is yet another (common and useful) topology on operator spaces, the weak operator
+topology, defined analogously using the product topology, but where the target space is given the
+weak-* topology, i.e., the pullback of the weak topology on the bidual of the space under the
+canonical embedding of a space into its bidual. We do not define it there, although it could also be
+defined analogously.
+\<close>
+
+definition%important strong_operator_topology::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) topology"
+where "strong_operator_topology = pullback_topology UNIV blinfun_apply euclidean"
+
+lemma strong_operator_topology_topspace:
+  "topspace strong_operator_topology = UNIV"
+unfolding strong_operator_topology_def topspace_pullback_topology topspace_euclidean by auto
+
+lemma strong_operator_topology_basis:
+  fixes f::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector)" and U::"'i \<Rightarrow> 'b set" and x::"'i \<Rightarrow> 'a"
+  assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
+  shows "openin strong_operator_topology {f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}"
+proof -
+  have "open {g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i}"
+    by (rule product_topology_basis'[OF assms])
+  moreover have "{f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}
+                = blinfun_apply-`{g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i} \<inter> UNIV"
+    by auto
+  ultimately show ?thesis
+    unfolding strong_operator_topology_def by (subst openin_pullback_topology) auto
+qed
+
+lemma strong_operator_topology_continuous_evaluation:
+  "continuous_on_topo strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
+proof -
+  have "continuous_on_topo strong_operator_topology euclidean ((\<lambda>f. f x) o blinfun_apply)"
+    unfolding strong_operator_topology_def apply (rule continuous_on_topo_pullback)
+    using continuous_on_topo_UNIV continuous_on_product_coordinates by fastforce
+  then show ?thesis unfolding comp_def by simp
+qed
+
+lemma continuous_on_strong_operator_topo_iff_coordinatewise:
+  "continuous_on_topo T strong_operator_topology f
+    \<longleftrightarrow> (\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x))"
+proof (auto)
+  fix x::"'b"
+  assume "continuous_on_topo T strong_operator_topology f"
+  with continuous_on_topo_compose[OF this strong_operator_topology_continuous_evaluation]
+  have "continuous_on_topo T euclidean ((\<lambda>z. blinfun_apply z x) o f)"
+    by simp
+  then show "continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
+    unfolding comp_def by auto
+next
+  assume *: "\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
+  have "continuous_on_topo T euclidean (blinfun_apply o f)"
+    unfolding euclidean_product_topology
+    apply (rule continuous_on_topo_coordinatewise_then_product, auto)
+    using * unfolding comp_def by auto
+  show "continuous_on_topo T strong_operator_topology f"
+    unfolding strong_operator_topology_def
+    apply (rule continuous_on_topo_pullback')
+    by (auto simp add: \<open>continuous_on_topo T euclidean (blinfun_apply o f)\<close>)
+qed
+
+lemma strong_operator_topology_weaker_than_euclidean:
+  "continuous_on_topo euclidean strong_operator_topology (\<lambda>f. f)"
+  by (subst continuous_on_strong_operator_topo_iff_coordinatewise,
+    auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
+
+
+
 end
diff -r 79c8ff387ed1 -r 5f67c5e457e3 src/HOL/Analysis/Cartesian_Space.thy
--- a/src/HOL/Analysis/Cartesian_Space.thy	Mon Mar 18 21:06:26 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Space.thy	Mon Mar 18 21:50:51 2019 +0100
@@ -671,7 +671,7 @@
   by (metis matrix_transpose_mul rank_mul_le_right rank_transpose)
 
 
-subsection%unimportant \<open>Lemmas for working on \<open>real^1/2/3\<close>\<close>
+subsection%unimportant \<open>Lemmas for working on \<open>real^1/2/3/4\<close>\<close>
 
 lemma exhaust_2:
   fixes x :: 2
@@ -699,6 +699,19 @@
 lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3"
   by (metis exhaust_3)
 
+lemma exhaust_4:
+  fixes x :: 4
+  shows "x = 1 \<or> x = 2 \<or> x = 3 \<or> x = 4"
+proof (induct x)
+  case (of_int z)
+  then have "0 \<le> z" and "z < 4" by simp_all
+  then have "z = 0 \<or> z = 1 \<or> z = 2 \<or> z = 3" by arith
+  then show ?case by auto
+qed
+
+lemma forall_4: "(\<forall>i::4. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3 \<and> P 4"
+  by (metis exhaust_4)
+
 lemma UNIV_1 [simp]: "UNIV = {1::1}"
   by (auto simp add: num1_eq_iff)
 
@@ -708,6 +721,9 @@
 lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}"
   using exhaust_3 by auto
 
+lemma UNIV_4: "UNIV = {1::4, 2::4, 3::4, 4::4}"
+  using exhaust_4 by auto
+
 lemma sum_1: "sum f (UNIV::1 set) = f 1"
   unfolding UNIV_1 by simp
 
@@ -717,6 +733,9 @@
 lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3"
   unfolding UNIV_3 by (simp add: ac_simps)
 
+lemma sum_4: "sum f (UNIV::4 set) = f 1 + f 2 + f 3 + f 4"
+  unfolding UNIV_4 by (simp add: ac_simps)
+
 subsection%unimportant\<open>The collapse of the general concepts to dimension one\<close>
 
 lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
diff -r 79c8ff387ed1 -r 5f67c5e457e3 src/HOL/Analysis/Continuous_Extension.thy
--- a/src/HOL/Analysis/Continuous_Extension.thy	Mon Mar 18 21:06:26 2019 +0100
+++ b/src/HOL/Analysis/Continuous_Extension.thy	Mon Mar 18 21:50:51 2019 +0100
@@ -14,7 +14,7 @@
    so the "support" must be made explicit in the summation below!\<close>
 
 proposition subordinate_partition_of_unity:
-  fixes S :: "'a :: euclidean_space set"
+  fixes S :: "'a::metric_space set"
   assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
       and fin: "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. U \<inter> V \<noteq> {}}"
   obtains F :: "['a set, 'a] \<Rightarrow> real"
@@ -26,9 +26,7 @@
   case True
     then obtain W where "W \<in> \<C>" "S \<subseteq> W" by metis
     then show ?thesis
-      apply (rule_tac F = "\<lambda>V x. if V = W then 1 else 0" in that)
-      apply (auto simp: continuous_on_const supp_sum_def support_on_def)
-      done
+      by (rule_tac F = "\<lambda>V x. if V = W then 1 else 0" in that) (auto simp: supp_sum_def support_on_def)
 next
   case False
     have nonneg: "0 \<le> supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>" for x
@@ -37,9 +35,9 @@
     proof -
       have "closedin (subtopology euclidean S) (S - V)"
         by (simp add: Diff_Diff_Int closedin_def opC openin_open_Int \<open>V \<in> \<C>\<close>)
-      with that False setdist_eq_0_closedin [of S "S-V" x] setdist_pos_le [of "{x}" "S - V"]
-        show ?thesis
-          by (simp add: order_class.order.order_iff_strict)
+      with that False  setdist_pos_le [of "{x}" "S - V"]
+      show ?thesis
+        using setdist_gt_0_closedin by fastforce
     qed
     have ss_pos: "0 < supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>" if "x \<in> S" for x
     proof -
@@ -50,17 +48,16 @@
       then have *: "finite {A \<in> \<C>. \<not> S \<subseteq> A \<and> x \<notin> closure (S - A)}"
         using closure_def that by (blast intro: rev_finite_subset)
       have "x \<notin> closure (S - U)"
-        by (metis \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> less_irrefl sd_pos setdist_eq_0_sing_1 that)
+        using \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> opC open_Int_closure_eq_empty by fastforce
       then show ?thesis
         apply (simp add: setdist_eq_0_sing_1 supp_sum_def support_on_def)
         apply (rule ordered_comm_monoid_add_class.sum_pos2 [OF *, of U])
         using \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> False
-        apply (auto simp: setdist_pos_le sd_pos that)
+        apply (auto simp: sd_pos that)
         done
     qed
     define F where
-      "F \<equiv> \<lambda>W x. if x \<in> S then setdist {x} (S - W) / supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>
-                 else 0"
+      "F \<equiv> \<lambda>W x. if x \<in> S then setdist {x} (S - W) / supp_sum (\<lambda>V. setdist {x} (S - V)) \<C> else 0"
     show ?thesis
     proof (rule_tac F = F in that)
       have "continuous_on S (F U)" if "U \<in> \<C>" for U
@@ -302,7 +299,7 @@
 text \<open>See \cite{dugundji}.\<close>
 
 theorem Dugundji:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
+  fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::real_inner"
   assumes "convex C" "C \<noteq> {}"
       and cloin: "closedin (subtopology euclidean U) S"
       and contf: "continuous_on S f" and "f ` S \<subseteq> C"
@@ -325,9 +322,8 @@
     by (auto simp: sd_pos \<B>_def)
   obtain \<C> where USsub: "U - S \<subseteq> \<Union>\<C>"
        and nbrhd: "\<And>U. U \<in> \<C> \<Longrightarrow> open U \<and> (\<exists>T. T \<in> \<B> \<and> U \<subseteq> T)"
-       and fin: "\<And>x. x \<in> U - S
-                     \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U. U \<in> \<C> \<and> U \<inter> V \<noteq> {}}"
-    using paracompact [OF USS] by auto
+       and fin: "\<And>x. x \<in> U - S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U. U \<in> \<C> \<and> U \<inter> V \<noteq> {}}"
+    by (rule paracompact [OF USS]) auto
   have "\<exists>v a. v \<in> U \<and> v \<notin> S \<and> a \<in> S \<and>
               T \<subseteq> ball v (setdist {v} S / 2) \<and>
               dist v a \<le> 2 * setdist {v} S" if "T \<in> \<C>" for T
@@ -353,7 +349,7 @@
   proof -
     have "dist (\<V> T) v < setdist {\<V> T} S / 2"
       using that VA mem_ball by blast
-    also have "... \<le> setdist {v} S"
+    also have "\<dots> \<le> setdist {v} S"
       using sdle [OF \<open>T \<in> \<C>\<close> \<open>v \<in> T\<close>] by simp
     also have vS: "setdist {v} S \<le> dist a v"
       by (simp add: setdist_le_dist setdist_sym \<open>a \<in> S\<close>)
@@ -362,9 +358,9 @@
       using sdle that vS by force
     have "dist a (\<A> T) \<le> dist a v + dist v (\<V> T) + dist (\<V> T) (\<A> T)"
       by (metis add.commute add_le_cancel_left dist_commute dist_triangle2 dist_triangle_le)
-    also have "... \<le> dist a v + dist a v + dist (\<V> T) (\<A> T)"
+    also have "\<dots> \<le> dist a v + dist a v + dist (\<V> T) (\<A> T)"
       using VTV by (simp add: dist_commute)
-    also have "... \<le> 2 * dist a v + 2 * setdist {\<V> T} S"
+    also have "\<dots> \<le> 2 * dist a v + 2 * setdist {\<V> T} S"
       using VA [OF \<open>T \<in> \<C>\<close>] by auto
     finally show ?thesis
       using VTS by linarith
@@ -477,66 +473,65 @@
 
 
 corollary Tietze:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
+  fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::real_inner"
   assumes "continuous_on S f"
-      and "closedin (subtopology euclidean U) S"
-      and "0 \<le> B"
-      and "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> B"
+    and "closedin (subtopology euclidean U) S"
+    and "0 \<le> B"
+    and "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> B"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-                  "\<And>x. x \<in> U \<Longrightarrow> norm(g x) \<le> B"
-  using assms
-by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f])
+    "\<And>x. x \<in> U \<Longrightarrow> norm(g x) \<le> B"
+  using assms by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f])
 
 corollary%unimportant Tietze_closed_interval:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::euclidean_space"
   assumes "continuous_on S f"
-      and "closedin (subtopology euclidean U) S"
-      and "cbox a b \<noteq> {}"
-      and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
+    and "closedin (subtopology euclidean U) S"
+    and "cbox a b \<noteq> {}"
+    and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-                  "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
-apply (rule Dugundji [of "cbox a b" U S f])
-using assms by auto
+    "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
+  apply (rule Dugundji [of "cbox a b" U S f])
+  using assms by auto
 
 corollary%unimportant Tietze_closed_interval_1:
-  fixes f :: "'a::euclidean_space \<Rightarrow> real"
+  fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> real"
   assumes "continuous_on S f"
-      and "closedin (subtopology euclidean U) S"
-      and "a \<le> b"
-      and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
+    and "closedin (subtopology euclidean U) S"
+    and "a \<le> b"
+    and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-                  "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
-apply (rule Dugundji [of "cbox a b" U S f])
-using assms by (auto simp: image_subset_iff)
+    "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
+  apply (rule Dugundji [of "cbox a b" U S f])
+  using assms by (auto simp: image_subset_iff)
 
 corollary%unimportant Tietze_open_interval:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::euclidean_space"
   assumes "continuous_on S f"
-      and "closedin (subtopology euclidean U) S"
-      and "box a b \<noteq> {}"
-      and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
+    and "closedin (subtopology euclidean U) S"
+    and "box a b \<noteq> {}"
+    and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-                  "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
-apply (rule Dugundji [of "box a b" U S f])
-using assms by auto
+    "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
+  apply (rule Dugundji [of "box a b" U S f])
+  using assms by auto
 
 corollary%unimportant Tietze_open_interval_1:
-  fixes f :: "'a::euclidean_space \<Rightarrow> real"
+  fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> real"
   assumes "continuous_on S f"
-      and "closedin (subtopology euclidean U) S"
-      and "a < b"
-      and no: "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
+    and "closedin (subtopology euclidean U) S"
+    and "a < b"
+    and no: "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-                  "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
-apply (rule Dugundji [of "box a b" U S f])
-using assms by (auto simp: image_subset_iff)
+    "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
+  apply (rule Dugundji [of "box a b" U S f])
+  using assms by (auto simp: image_subset_iff)
 
 corollary%unimportant Tietze_unbounded:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
+  fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::real_inner"
   assumes "continuous_on S f"
-      and "closedin (subtopology euclidean U) S"
+    and "closedin (subtopology euclidean U) S"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-apply (rule Dugundji [of UNIV U S f])
-using assms by auto
+  apply (rule Dugundji [of UNIV U S f])
+  using assms by auto
 
 end
diff -r 79c8ff387ed1 -r 5f67c5e457e3 src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Mon Mar 18 21:06:26 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Mon Mar 18 21:50:51 2019 +0100
@@ -3170,4 +3170,71 @@
 lemma setdist_le_sing: "x \<in> S ==> setdist S T \<le> setdist {x} T"
   using setdist_subset_left by auto
 
+lemma infdist_eq_setdist: "infdist x A = setdist {x} A"
+  by (simp add: infdist_def setdist_def Setcompr_eq_image)
+
+lemma setdist_eq_infdist: "setdist A B = (if A = {} then 0 else INF a\<in>A. infdist a B)"
+proof -
+  have "Inf {dist x y |x y. x \<in> A \<and> y \<in> B} = (INF x\<in>A. Inf (dist x ` B))"
+    if "b \<in> B" "a \<in> A" for a b
+  proof (rule order_antisym)
+    have "Inf {dist x y |x y. x \<in> A \<and> y \<in> B} \<le> Inf (dist x ` B)"
+      if  "b \<in> B" "a \<in> A" "x \<in> A" for x 
+    proof -
+      have *: "\<And>b'. b' \<in> B \<Longrightarrow> Inf {dist x y |x y. x \<in> A \<and> y \<in> B} \<le> dist x b'"
+        by (metis (mono_tags, lifting) ex_in_conv setdist_def setdist_le_dist that(3))
+      show ?thesis
+        using that by (subst conditionally_complete_lattice_class.le_cInf_iff) (auto simp: *)+
+    qed
+    then show "Inf {dist x y |x y. x \<in> A \<and> y \<in> B} \<le> (INF x\<in>A. Inf (dist x ` B))"
+      using that
+      by (subst conditionally_complete_lattice_class.le_cInf_iff) (auto simp: bdd_below_def)
+  next
+    have *: "\<And>x y. \<lbrakk>b \<in> B; a \<in> A; x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> \<exists>a\<in>A. Inf (dist a ` B) \<le> dist x y"
+      by (meson bdd_below_image_dist cINF_lower)
+    show "(INF x\<in>A. Inf (dist x ` B)) \<le> Inf {dist x y |x y. x \<in> A \<and> y \<in> B}"
+    proof (rule conditionally_complete_lattice_class.cInf_mono)
+      show "bdd_below ((\<lambda>x. Inf (dist x ` B)) ` A)"
+        by (metis (no_types, lifting) bdd_belowI2 ex_in_conv infdist_def infdist_nonneg that(1))
+    qed (use that in \<open>auto simp: *\<close>)
+  qed
+  then show ?thesis
+    by (auto simp: setdist_def infdist_def)
+qed
+
+lemma continuous_on_infdist [continuous_intros]: "continuous_on B (\<lambda>y. infdist y A)"
+  by (simp add: continuous_on_setdist infdist_eq_setdist)
+
+proposition setdist_attains_inf:
+  assumes "compact B" "B \<noteq> {}"
+  obtains y where "y \<in> B" "setdist A B = infdist y A"
+proof (cases "A = {}")
+  case True
+  then show thesis
+    by (metis assms diameter_compact_attained infdist_def setdist_def that)
+next
+  case False
+  obtain y where "y \<in> B" and min: "\<And>y'. y' \<in> B \<Longrightarrow> infdist y A \<le> infdist y' A"
+    using continuous_attains_inf [OF assms continuous_on_infdist] by blast
+  show thesis
+  proof
+    have "setdist A B = (INF y\<in>B. infdist y A)"
+      by (metis \<open>B \<noteq> {}\<close> setdist_eq_infdist setdist_sym)
+    also have "\<dots> = infdist y A"
+    proof (rule order_antisym)
+      show "(INF y\<in>B. infdist y A) \<le> infdist y A"
+      proof (rule cInf_lower)
+        show "infdist y A \<in> (\<lambda>y. infdist y A) ` B"
+          using \<open>y \<in> B\<close> by blast
+        show "bdd_below ((\<lambda>y. infdist y A) ` B)"
+          by (meson bdd_belowI2 infdist_nonneg)
+      qed
+    next
+      show "infdist y A \<le> (INF y\<in>B. infdist y A)"
+        by (simp add: \<open>B \<noteq> {}\<close> cINF_greatest min)
+    qed
+    finally show "setdist A B = infdist y A" .
+  qed (fact \<open>y \<in> B\<close>)
+qed
+
 end
\ No newline at end of file
diff -r 79c8ff387ed1 -r 5f67c5e457e3 src/HOL/Analysis/Elementary_Normed_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Mon Mar 18 21:06:26 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Mon Mar 18 21:50:51 2019 +0100
@@ -810,6 +810,9 @@
   shows "\<not> compact (UNIV::'a set)"
     by (simp add: compact_eq_bounded_closed)
 
+lemma not_compact_space_euclideanreal [simp]: "\<not> compact_space euclideanreal"
+  by (simp add: compact_space_def)
+
 text\<open>Representing sets as the union of a chain of compact sets.\<close>
 lemma closed_Union_compact_subsets:
   fixes S :: "'a::{heine_borel,real_normed_vector} set"
diff -r 79c8ff387ed1 -r 5f67c5e457e3 src/HOL/Analysis/Finite_Product_Measure.thy
--- a/src/HOL/Analysis/Finite_Product_Measure.thy	Mon Mar 18 21:06:26 2019 +0100
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Mon Mar 18 21:50:51 2019 +0100
@@ -5,7 +5,7 @@
 section \<open>Finite Product Measure\<close>
 
 theory Finite_Product_Measure
-imports Binary_Product_Measure
+imports Binary_Product_Measure Function_Topology
 begin
 
 lemma PiE_choice: "(\<exists>f\<in>Pi\<^sub>E I F. \<forall>i\<in>I. P i (f i)) \<longleftrightarrow> (\<forall>i\<in>I. \<exists>x\<in>F i. P i x)"
@@ -1202,4 +1202,142 @@
   with E show ?thesis by auto
 qed
 
+
+
+subsection \<open>Measurability\<close>
+
+text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,
+generated by open sets in the product, and the product sigma algebra, countably generated by
+products of measurable sets along finitely many coordinates. The second one is defined and studied
+in \<^file>\<open>Finite_Product_Measure.thy\<close>.
+
+These sigma-algebra share a lot of natural properties (measurability of coordinates, for instance),
+but there is a fundamental difference: open sets are generated by arbitrary unions, not only
+countable ones, so typically many open sets will not be measurable with respect to the product sigma
+algebra (while all sets in the product sigma algebra are borel). The two sigma algebras coincide
+only when everything is countable (i.e., the product is countable, and the borel sigma algebra in
+the factor is countably generated).
+
+In this paragraph, we develop basic measurability properties for the borel sigma algebra, and
+compare it with the product sigma algebra as explained above.
+\<close>
+
+lemma measurable_product_coordinates [measurable (raw)]:
+  "(\<lambda>x. x i) \<in> measurable borel borel"
+by (rule borel_measurable_continuous_on1[OF continuous_on_product_coordinates])
+
+lemma measurable_product_then_coordinatewise:
+  fixes f::"'a \<Rightarrow> 'b \<Rightarrow> ('c::topological_space)"
+  assumes [measurable]: "f \<in> borel_measurable M"
+  shows "(\<lambda>x. f x i) \<in> borel_measurable M"
+proof -
+  have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f"
+    unfolding comp_def by auto
+  then show ?thesis by simp
+qed
+
+text \<open>To compare the Borel sigma algebra with the product sigma algebra, we give a presentation
+of the product sigma algebra that is more similar to the one we used above for the product
+topology.\<close>
+
+lemma sets_PiM_finite:
+  "sets (Pi\<^sub>M I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
+        {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
+proof
+  have "{(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}} \<subseteq> sets (Pi\<^sub>M I M)"
+  proof (auto)
+    fix X assume H: "\<forall>i. X i \<in> sets (M i)" "finite {i. X i \<noteq> space (M i)}"
+    then have *: "X i \<in> sets (M i)" for i by simp
+    define J where "J = {i \<in> I. X i \<noteq> space (M i)}"
+    have "finite J" "J \<subseteq> I" unfolding J_def using H by auto
+    define Y where "Y = (\<Pi>\<^sub>E j\<in>J. X j)"
+    have "prod_emb I M J Y \<in> sets (Pi\<^sub>M I M)"
+      unfolding Y_def apply (rule sets_PiM_I) using \<open>finite J\<close> \<open>J \<subseteq> I\<close> * by auto
+    moreover have "prod_emb I M J Y = (\<Pi>\<^sub>E i\<in>I. X i)"
+      unfolding prod_emb_def Y_def J_def using H sets.sets_into_space[OF *]
+      by (auto simp add: PiE_iff, blast)
+    ultimately show "Pi\<^sub>E I X \<in> sets (Pi\<^sub>M I M)" by simp
+  qed
+  then show "sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}
+              \<subseteq> sets (Pi\<^sub>M I M)"
+    by (metis (mono_tags, lifting) sets.sigma_sets_subset' sets.top space_PiM)
+
+  have *: "\<exists>X. {f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X \<and>
+                (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}"
+    if "i \<in> I" "A \<in> sets (M i)" for i A
+  proof -
+    define X where "X = (\<lambda>j. if j = i then A else space (M j))"
+    have "{f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X"
+      unfolding X_def using sets.sets_into_space[OF \<open>A \<in> sets (M i)\<close>] \<open>i \<in> I\<close>
+      by (auto simp add: PiE_iff extensional_def, metis subsetCE, metis)
+    moreover have "X j \<in> sets (M j)" for j
+      unfolding X_def using \<open>A \<in> sets (M i)\<close> by auto
+    moreover have "finite {j. X j \<noteq> space (M j)}"
+      unfolding X_def by simp
+    ultimately show ?thesis by auto
+  qed
+  show "sets (Pi\<^sub>M I M) \<subseteq> sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
+    unfolding sets_PiM_single
+    apply (rule sigma_sets_mono')
+    apply (auto simp add: PiE_iff *)
+    done
+qed
+
+lemma sets_PiM_subset_borel:
+  "sets (Pi\<^sub>M UNIV (\<lambda>_. borel)) \<subseteq> sets borel"
+proof -
+  have *: "Pi\<^sub>E UNIV X \<in> sets borel" if [measurable]: "\<And>i. X i \<in> sets borel" "finite {i. X i \<noteq> UNIV}" for X::"'a \<Rightarrow> 'b set"
+  proof -
+    define I where "I = {i. X i \<noteq> UNIV}"
+    have "finite I" unfolding I_def using that by simp
+    have "Pi\<^sub>E UNIV X = (\<Inter>i\<in>I. (\<lambda>x. x i)-`(X i) \<inter> space borel) \<inter> space borel"
+      unfolding I_def by auto
+    also have "... \<in> sets borel"
+      using that \<open>finite I\<close> by measurable
+    finally show ?thesis by simp
+  qed
+  then have "{(\<Pi>\<^sub>E i\<in>UNIV. X i) |X::('a \<Rightarrow> 'b set). (\<forall>i. X i \<in> sets borel) \<and> finite {i. X i \<noteq> space borel}} \<subseteq> sets borel"
+    by auto
+  then show ?thesis unfolding sets_PiM_finite space_borel
+    by (simp add: * sets.sigma_sets_subset')
+qed
+
+proposition sets_PiM_equal_borel:
+  "sets (Pi\<^sub>M UNIV (\<lambda>i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"
+proof
+  obtain K::"('a \<Rightarrow> 'b) set set" where K: "topological_basis K" "countable K"
+            "\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
+    using product_topology_countable_basis by fast
+  have *: "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> K" for k
+  proof -
+    obtain X where H: "k = Pi\<^sub>E UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
+      using K(3)[OF \<open>k \<in> K\<close>] by blast
+    show ?thesis unfolding H(1) sets_PiM_finite space_borel using borel_open[OF H(2)] H(3) by auto
+  qed
+  have **: "U \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "open U" for U::"('a \<Rightarrow> 'b) set"
+  proof -
+    obtain B where "B \<subseteq> K" "U = (\<Union>B)"
+      using \<open>open U\<close> \<open>topological_basis K\<close> by (metis topological_basis_def)
+    have "countable B" using \<open>B \<subseteq> K\<close> \<open>countable K\<close> countable_subset by blast
+    moreover have "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> B" for k
+      using \<open>B \<subseteq> K\<close> * that by auto
+    ultimately show ?thesis unfolding \<open>U = (\<Union>B)\<close> by auto
+  qed
+  have "sigma_sets UNIV (Collect open) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>i::'a. (borel::('b measure))))"
+    apply (rule sets.sigma_sets_subset') using ** by auto
+  then show "sets (borel::('a \<Rightarrow> 'b) measure) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))"
+    unfolding borel_def by auto
+qed (simp add: sets_PiM_subset_borel)
+
+lemma measurable_coordinatewise_then_product:
+  fixes f::"'a \<Rightarrow> ('b::countable) \<Rightarrow> ('c::second_countable_topology)"
+  assumes [measurable]: "\<And>i. (\<lambda>x. f x i) \<in> borel_measurable M"
+  shows "f \<in> borel_measurable M"
+proof -
+  have "f \<in> measurable M (Pi\<^sub>M UNIV (\<lambda>_. borel))"
+    by (rule measurable_PiM_single', auto simp add: assms)
+  then show ?thesis using sets_PiM_equal_borel measurable_cong_sets by blast
+qed
+
+
 end
diff -r 79c8ff387ed1 -r 5f67c5e457e3 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Mon Mar 18 21:06:26 2019 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy	Mon Mar 18 21:50:51 2019 +0100
@@ -3,7 +3,7 @@
 *)
 
 theory Function_Topology
-imports Topology_Euclidean_Space Bounded_Linear_Function Finite_Product_Measure 
+imports Topology_Euclidean_Space   
 begin
 
 
@@ -945,24 +945,37 @@
 
 lemma continuous_on_product_coordinates [simp]:
   "continuous_on UNIV (\<lambda>x. x i::('b::topological_space))"
-unfolding continuous_on_topo_UNIV euclidean_product_topology
-by (rule continuous_on_topo_product_coordinates, simp)
+  unfolding continuous_on_topo_UNIV euclidean_product_topology
+  by (rule continuous_on_topo_product_coordinates, simp)
 
 lemma continuous_on_coordinatewise_then_product [intro, continuous_intros]:
-  assumes "\<And>i. continuous_on UNIV (\<lambda>x. f x i)"
-  shows "continuous_on UNIV f"
-using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
-by (rule continuous_on_topo_coordinatewise_then_product, simp)
+  fixes f :: "('a \<Rightarrow> real) \<Rightarrow> 'b \<Rightarrow> real"
+  assumes "\<And>i. continuous_on S (\<lambda>x. f x i)"
+  shows "continuous_on S f"
+  using continuous_on_topo_coordinatewise_then_product [of UNIV, where T = "\<lambda>i. euclideanreal"]
+  by (metis UNIV_I assms continuous_on_continuous_on_topo euclidean_product_topology)
 
-lemma continuous_on_product_then_coordinatewise:
+lemma continuous_on_product_then_coordinatewise_UNIV:
   assumes "continuous_on UNIV f"
   shows "continuous_on UNIV (\<lambda>x. f x i)"
 using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
 by (rule continuous_on_topo_product_then_coordinatewise(1), simp)
 
-lemma continuous_on_product_coordinatewise_iff:
-  "continuous_on UNIV f \<longleftrightarrow> (\<forall>i. continuous_on UNIV (\<lambda>x. f x i))"
-by (auto intro: continuous_on_product_then_coordinatewise)
+lemma continuous_on_product_then_coordinatewise:
+  assumes "continuous_on S f"
+  shows "continuous_on S (\<lambda>x. f x i)"
+proof -
+  have "continuous_on S ((\<lambda>q. q i) \<circ> f)"
+    by (metis assms continuous_on_compose continuous_on_id 
+        continuous_on_product_then_coordinatewise_UNIV continuous_on_subset subset_UNIV)
+  then show ?thesis
+    by auto
+qed
+
+lemma continuous_on_coordinatewise_iff:
+  fixes f :: "('a \<Rightarrow> real) \<Rightarrow> 'b \<Rightarrow> real"
+  shows "continuous_on (A \<inter> S) f \<longleftrightarrow> (\<forall>i. continuous_on (A \<inter> S) (\<lambda>x. f x i))"
+  by (auto simp: continuous_on_product_then_coordinatewise)
 
 subsubsection%important \<open>Topological countability for product spaces\<close>
 
@@ -1194,86 +1207,6 @@
   using product_topology_countable_basis topological_basis_imp_subbasis by auto
 
 
-subsection \<open>The strong operator topology on continuous linear operators\<close> (* FIX ME mv*)
-
-text \<open>Let \<open>'a\<close> and \<open>'b\<close> be two normed real vector spaces. Then the space of linear continuous
-operators from \<open>'a\<close> to \<open>'b\<close> has a canonical norm, and therefore a canonical corresponding topology
-(the type classes instantiation are given in \<^file>\<open>Bounded_Linear_Function.thy\<close>).
-
-However, there is another topology on this space, the strong operator topology, where \<open>T\<^sub>n\<close> tends to
-\<open>T\<close> iff, for all \<open>x\<close> in \<open>'a\<close>, then \<open>T\<^sub>n x\<close> tends to \<open>T x\<close>. This is precisely the product topology
-where the target space is endowed with the norm topology. It is especially useful when \<open>'b\<close> is the set
-of real numbers, since then this topology is compact.
-
-We can not implement it using type classes as there is already a topology, but at least we
-can define it as a topology.
-
-Note that there is yet another (common and useful) topology on operator spaces, the weak operator
-topology, defined analogously using the product topology, but where the target space is given the
-weak-* topology, i.e., the pullback of the weak topology on the bidual of the space under the
-canonical embedding of a space into its bidual. We do not define it there, although it could also be
-defined analogously.
-\<close>
-
-definition%important strong_operator_topology::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) topology"
-where "strong_operator_topology = pullback_topology UNIV blinfun_apply euclidean"
-
-lemma strong_operator_topology_topspace:
-  "topspace strong_operator_topology = UNIV"
-unfolding strong_operator_topology_def topspace_pullback_topology topspace_euclidean by auto
-
-lemma strong_operator_topology_basis:
-  fixes f::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector)" and U::"'i \<Rightarrow> 'b set" and x::"'i \<Rightarrow> 'a"
-  assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
-  shows "openin strong_operator_topology {f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}"
-proof -
-  have "open {g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i}"
-    by (rule product_topology_basis'[OF assms])
-  moreover have "{f. \<forall>i\<in>I. blinfun_apply f (x i) \<in> U i}
-                = blinfun_apply-`{g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i} \<inter> UNIV"
-    by auto
-  ultimately show ?thesis
-    unfolding strong_operator_topology_def by (subst openin_pullback_topology) auto
-qed
-
-lemma strong_operator_topology_continuous_evaluation:
-  "continuous_on_topo strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
-proof -
-  have "continuous_on_topo strong_operator_topology euclidean ((\<lambda>f. f x) o blinfun_apply)"
-    unfolding strong_operator_topology_def apply (rule continuous_on_topo_pullback)
-    using continuous_on_topo_UNIV continuous_on_product_coordinates by fastforce
-  then show ?thesis unfolding comp_def by simp
-qed
-
-lemma continuous_on_strong_operator_topo_iff_coordinatewise:
-  "continuous_on_topo T strong_operator_topology f
-    \<longleftrightarrow> (\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x))"
-proof (auto)
-  fix x::"'b"
-  assume "continuous_on_topo T strong_operator_topology f"
-  with continuous_on_topo_compose[OF this strong_operator_topology_continuous_evaluation]
-  have "continuous_on_topo T euclidean ((\<lambda>z. blinfun_apply z x) o f)"
-    by simp
-  then show "continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
-    unfolding comp_def by auto
-next
-  assume *: "\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
-  have "continuous_on_topo T euclidean (blinfun_apply o f)"
-    unfolding euclidean_product_topology
-    apply (rule continuous_on_topo_coordinatewise_then_product, auto)
-    using * unfolding comp_def by auto
-  show "continuous_on_topo T strong_operator_topology f"
-    unfolding strong_operator_topology_def
-    apply (rule continuous_on_topo_pullback')
-    by (auto simp add: \<open>continuous_on_topo T euclidean (blinfun_apply o f)\<close>)
-qed
-
-lemma strong_operator_topology_weaker_than_euclidean:
-  "continuous_on_topo euclidean strong_operator_topology (\<lambda>f. f)"
-  by (subst continuous_on_strong_operator_topo_iff_coordinatewise,
-    auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
-
-
 subsection \<open>Metrics on product spaces\<close>
 
 
@@ -1650,142 +1583,4 @@
 instance "fun" :: (countable, polish_space) polish_space
 by standard
 
-
-
-
-subsection \<open>Measurability\<close> (*FIX ME move? *)
-
-text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,
-generated by open sets in the product, and the product sigma algebra, countably generated by
-products of measurable sets along finitely many coordinates. The second one is defined and studied
-in \<^file>\<open>Finite_Product_Measure.thy\<close>.
-
-These sigma-algebra share a lot of natural properties (measurability of coordinates, for instance),
-but there is a fundamental difference: open sets are generated by arbitrary unions, not only
-countable ones, so typically many open sets will not be measurable with respect to the product sigma
-algebra (while all sets in the product sigma algebra are borel). The two sigma algebras coincide
-only when everything is countable (i.e., the product is countable, and the borel sigma algebra in
-the factor is countably generated).
-
-In this paragraph, we develop basic measurability properties for the borel sigma algebra, and
-compare it with the product sigma algebra as explained above.
-\<close>
-
-lemma measurable_product_coordinates [measurable (raw)]:
-  "(\<lambda>x. x i) \<in> measurable borel borel"
-by (rule borel_measurable_continuous_on1[OF continuous_on_product_coordinates])
-
-lemma measurable_product_then_coordinatewise:
-  fixes f::"'a \<Rightarrow> 'b \<Rightarrow> ('c::topological_space)"
-  assumes [measurable]: "f \<in> borel_measurable M"
-  shows "(\<lambda>x. f x i) \<in> borel_measurable M"
-proof -
-  have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f"
-    unfolding comp_def by auto
-  then show ?thesis by simp
-qed
-
-text \<open>To compare the Borel sigma algebra with the product sigma algebra, we give a presentation
-of the product sigma algebra that is more similar to the one we used above for the product
-topology.\<close>
-
-lemma sets_PiM_finite:
-  "sets (Pi\<^sub>M I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
-        {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
-proof
-  have "{(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}} \<subseteq> sets (Pi\<^sub>M I M)"
-  proof (auto)
-    fix X assume H: "\<forall>i. X i \<in> sets (M i)" "finite {i. X i \<noteq> space (M i)}"
-    then have *: "X i \<in> sets (M i)" for i by simp
-    define J where "J = {i \<in> I. X i \<noteq> space (M i)}"
-    have "finite J" "J \<subseteq> I" unfolding J_def using H by auto
-    define Y where "Y = (\<Pi>\<^sub>E j\<in>J. X j)"
-    have "prod_emb I M J Y \<in> sets (Pi\<^sub>M I M)"
-      unfolding Y_def apply (rule sets_PiM_I) using \<open>finite J\<close> \<open>J \<subseteq> I\<close> * by auto
-    moreover have "prod_emb I M J Y = (\<Pi>\<^sub>E i\<in>I. X i)"
-      unfolding prod_emb_def Y_def J_def using H sets.sets_into_space[OF *]
-      by (auto simp add: PiE_iff, blast)
-    ultimately show "Pi\<^sub>E I X \<in> sets (Pi\<^sub>M I M)" by simp
-  qed
-  then show "sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}
-              \<subseteq> sets (Pi\<^sub>M I M)"
-    by (metis (mono_tags, lifting) sets.sigma_sets_subset' sets.top space_PiM)
-
-  have *: "\<exists>X. {f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X \<and>
-                (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}"
-    if "i \<in> I" "A \<in> sets (M i)" for i A
-  proof -
-    define X where "X = (\<lambda>j. if j = i then A else space (M j))"
-    have "{f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X"
-      unfolding X_def using sets.sets_into_space[OF \<open>A \<in> sets (M i)\<close>] \<open>i \<in> I\<close>
-      by (auto simp add: PiE_iff extensional_def, metis subsetCE, metis)
-    moreover have "X j \<in> sets (M j)" for j
-      unfolding X_def using \<open>A \<in> sets (M i)\<close> by auto
-    moreover have "finite {j. X j \<noteq> space (M j)}"
-      unfolding X_def by simp
-    ultimately show ?thesis by auto
-  qed
-  show "sets (Pi\<^sub>M I M) \<subseteq> sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
-    unfolding sets_PiM_single
-    apply (rule sigma_sets_mono')
-    apply (auto simp add: PiE_iff *)
-    done
-qed
-
-lemma sets_PiM_subset_borel:
-  "sets (Pi\<^sub>M UNIV (\<lambda>_. borel)) \<subseteq> sets borel"
-proof -
-  have *: "Pi\<^sub>E UNIV X \<in> sets borel" if [measurable]: "\<And>i. X i \<in> sets borel" "finite {i. X i \<noteq> UNIV}" for X::"'a \<Rightarrow> 'b set"
-  proof -
-    define I where "I = {i. X i \<noteq> UNIV}"
-    have "finite I" unfolding I_def using that by simp
-    have "Pi\<^sub>E UNIV X = (\<Inter>i\<in>I. (\<lambda>x. x i)-`(X i) \<inter> space borel) \<inter> space borel"
-      unfolding I_def by auto
-    also have "... \<in> sets borel"
-      using that \<open>finite I\<close> by measurable
-    finally show ?thesis by simp
-  qed
-  then have "{(\<Pi>\<^sub>E i\<in>UNIV. X i) |X::('a \<Rightarrow> 'b set). (\<forall>i. X i \<in> sets borel) \<and> finite {i. X i \<noteq> space borel}} \<subseteq> sets borel"
-    by auto
-  then show ?thesis unfolding sets_PiM_finite space_borel
-    by (simp add: * sets.sigma_sets_subset')
-qed
-
-proposition sets_PiM_equal_borel:
-  "sets (Pi\<^sub>M UNIV (\<lambda>i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"
-proof
-  obtain K::"('a \<Rightarrow> 'b) set set" where K: "topological_basis K" "countable K"
-            "\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
-    using product_topology_countable_basis by fast
-  have *: "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> K" for k
-  proof -
-    obtain X where H: "k = Pi\<^sub>E UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
-      using K(3)[OF \<open>k \<in> K\<close>] by blast
-    show ?thesis unfolding H(1) sets_PiM_finite space_borel using borel_open[OF H(2)] H(3) by auto
-  qed
-  have **: "U \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "open U" for U::"('a \<Rightarrow> 'b) set"
-  proof -
-    obtain B where "B \<subseteq> K" "U = (\<Union>B)"
-      using \<open>open U\<close> \<open>topological_basis K\<close> by (metis topological_basis_def)
-    have "countable B" using \<open>B \<subseteq> K\<close> \<open>countable K\<close> countable_subset by blast
-    moreover have "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> B" for k
-      using \<open>B \<subseteq> K\<close> * that by auto
-    ultimately show ?thesis unfolding \<open>U = (\<Union>B)\<close> by auto
-  qed
-  have "sigma_sets UNIV (Collect open) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>i::'a. (borel::('b measure))))"
-    apply (rule sets.sigma_sets_subset') using ** by auto
-  then show "sets (borel::('a \<Rightarrow> 'b) measure) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))"
-    unfolding borel_def by auto
-qed (simp add: sets_PiM_subset_borel)
-
-lemma measurable_coordinatewise_then_product:
-  fixes f::"'a \<Rightarrow> ('b::countable) \<Rightarrow> ('c::second_countable_topology)"
-  assumes [measurable]: "\<And>i. (\<lambda>x. f x i) \<in> borel_measurable M"
-  shows "f \<in> borel_measurable M"
-proof -
-  have "f \<in> measurable M (Pi\<^sub>M UNIV (\<lambda>_. borel))"
-    by (rule measurable_PiM_single', auto simp add: assms)
-  then show ?thesis using sets_PiM_equal_borel measurable_cong_sets by blast
-qed
-
 end
diff -r 79c8ff387ed1 -r 5f67c5e457e3 src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Mon Mar 18 21:06:26 2019 +0100
+++ b/src/HOL/Analysis/Homotopy.thy	Mon Mar 18 21:50:51 2019 +0100
@@ -3652,6 +3652,11 @@
     using \<open>S \<subseteq> box a b\<close> by auto
 qed
 
+corollary bounded_path_connected_Compl_real:
+  fixes S :: "real set"
+  assumes "bounded S" "path_connected(- S)" shows "S = {}"
+  by (simp add: assms bounded_connected_Compl_real path_connected_imp_connected)
+
 lemma bounded_connected_Compl_1:
   fixes S :: "'a::{euclidean_space} set"
   assumes "bounded S" and conn: "connected(- S)" and 1: "DIM('a) = 1"
diff -r 79c8ff387ed1 -r 5f67c5e457e3 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Mon Mar 18 21:06:26 2019 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Mon Mar 18 21:50:51 2019 +0100
@@ -6715,13 +6715,12 @@
 subsection\<open>Paracompactness\<close>
 
 proposition paracompact:
-  fixes S :: "'a :: euclidean_space set"
+  fixes S :: "'a :: {metric_space,second_countable_topology} set"
   assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
   obtains \<C>' where "S \<subseteq> \<Union> \<C>'"
                and "\<And>U. U \<in> \<C>' \<Longrightarrow> open U \<and> (\<exists>T. T \<in> \<C> \<and> U \<subseteq> T)"
                and "\<And>x. x \<in> S
-                       \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and>
-                               finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
+                       \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
 proof (cases "S = {}")
   case True with that show ?thesis by blast
 next
@@ -6737,7 +6736,7 @@
       apply (rule_tac x = "ball x e" in exI)
       using  \<open>T \<in> \<C>\<close>
       apply (simp add: closure_minimal)
-      done
+      using closed_cball closure_minimal by blast
   qed
   then obtain F G where Gin: "x \<in> G x" and oG: "open (G x)"
                     and clos: "closure (G x) \<subseteq> F x" and Fin: "F x \<in> \<C>"
@@ -6802,7 +6801,7 @@
 qed
 
 corollary paracompact_closedin:
-  fixes S :: "'a :: euclidean_space set"
+  fixes S :: "'a :: {metric_space,second_countable_topology} set"
   assumes cin: "closedin (subtopology euclidean U) S"
       and oin: "\<And>T. T \<in> \<C> \<Longrightarrow> openin (subtopology euclidean U) T"
       and "S \<subseteq> \<Union>\<C>"
@@ -6825,7 +6824,7 @@
   obtain \<D> where "U \<subseteq> \<Union>\<D>"
              and D1: "\<And>U. U \<in> \<D> \<Longrightarrow> open U \<and> (\<exists>T. T \<in> insert (- K) (F ` \<C>) \<and> U \<subseteq> T)"
              and D2: "\<And>x. x \<in> U \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<D>. U \<inter> V \<noteq> {}}"
-    using paracompact [OF 1 2] by auto
+    by (blast intro: paracompact [OF 1 2])
   let ?C = "{U \<inter> V |V. V \<in> \<D> \<and> (V \<inter> K \<noteq> {})}"
   show ?thesis
   proof (rule_tac \<C>' = "{U \<inter> V |V. V \<in> \<D> \<and> (V \<inter> K \<noteq> {})}" in that)
@@ -6847,7 +6846,7 @@
 qed
 
 corollary%unimportant paracompact_closed:
-  fixes S :: "'a :: euclidean_space set"
+  fixes S :: "'a :: {metric_space,second_countable_topology} set"
   assumes "closed S"
       and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
       and "S \<subseteq> \<Union>\<C>"
@@ -6855,7 +6854,7 @@
                and "\<And>U. U \<in> \<C>' \<Longrightarrow> open U \<and> (\<exists>T. T \<in> \<C> \<and> U \<subseteq> T)"
                and "\<And>x. \<exists>V. open V \<and> x \<in> V \<and>
                                finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
-using paracompact_closedin [of UNIV S \<C>] assms by auto
+  by (rule paracompact_closedin [of UNIV S \<C>]) (auto simp: assms)
 
   
 subsection%unimportant\<open>Closed-graph characterization of continuity\<close>
diff -r 79c8ff387ed1 -r 5f67c5e457e3 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Mar 18 21:06:26 2019 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Mar 18 21:50:51 2019 +0100
@@ -2241,24 +2241,22 @@
 subsection \<open>Set Distance\<close>
 
 lemma setdist_compact_closed:
-  fixes S :: "'a::{heine_borel,real_normed_vector} set"
-  assumes S: "compact S" and T: "closed T"
-      and "S \<noteq> {}" "T \<noteq> {}"
-    shows "\<exists>x \<in> S. \<exists>y \<in> T. dist x y = setdist S T"
+  fixes A :: "'a::heine_borel set"
+  assumes A: "compact A" and B: "closed B"
+    and "A \<noteq> {}" "B \<noteq> {}"
+  shows "\<exists>x \<in> A. \<exists>y \<in> B. dist x y = setdist A B"
 proof -
-  have "(\<Union>x\<in> S. \<Union>y \<in> T. {x - y}) \<noteq> {}"
-    using assms by blast
-  then have "\<exists>x \<in> S. \<exists>y \<in> T. dist x y \<le> setdist S T"
-    apply (rule distance_attains_inf [where a=0, OF compact_closed_differences [OF S T]])
-    apply (simp add: dist_norm le_setdist_iff)
-    apply blast
-    done
-  then show ?thesis
-    by (blast intro!: antisym [OF _ setdist_le_dist] )
+  obtain x where "x \<in> A" "setdist A B = infdist x B"
+    by (metis A assms(3) setdist_attains_inf setdist_sym)
+  moreover
+  obtain y where"y \<in> B" "infdist x B = dist x y"
+    using B \<open>B \<noteq> {}\<close> infdist_attains_inf by blast
+  ultimately show ?thesis
+    using \<open>x \<in> A\<close> \<open>y \<in> B\<close> by auto
 qed
 
 lemma setdist_closed_compact:
-  fixes S :: "'a::{heine_borel,real_normed_vector} set"
+  fixes S :: "'a::heine_borel set"
   assumes S: "closed S" and T: "compact T"
       and "S \<noteq> {}" "T \<noteq> {}"
     shows "\<exists>x \<in> S. \<exists>y \<in> T. dist x y = setdist S T"
@@ -2266,76 +2264,71 @@
   by (metis dist_commute setdist_sym)
 
 lemma setdist_eq_0_compact_closed:
-  fixes S :: "'a::{heine_borel,real_normed_vector} set"
   assumes S: "compact S" and T: "closed T"
     shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> S \<inter> T \<noteq> {}"
-  apply (cases "S = {} \<or> T = {}", force)
-  using setdist_compact_closed [OF S T]
-  apply (force intro: setdist_eq_0I )
-  done
+proof (cases "S = {} \<or> T = {}")
+  case True
+  then show ?thesis
+    by force
+next
+  case False
+  then show ?thesis
+    by (metis S T disjoint_iff_not_equal in_closed_iff_infdist_zero setdist_attains_inf setdist_eq_0I setdist_sym)
+qed
 
 corollary setdist_gt_0_compact_closed:
-  fixes S :: "'a::{heine_borel,real_normed_vector} set"
   assumes S: "compact S" and T: "closed T"
     shows "setdist S T > 0 \<longleftrightarrow> (S \<noteq> {} \<and> T \<noteq> {} \<and> S \<inter> T = {})"
-  using setdist_pos_le [of S T] setdist_eq_0_compact_closed [OF assms]
-  by linarith
+  using setdist_pos_le [of S T] setdist_eq_0_compact_closed [OF assms] by linarith
 
 lemma setdist_eq_0_closed_compact:
-  fixes S :: "'a::{heine_borel,real_normed_vector} set"
   assumes S: "closed S" and T: "compact T"
     shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> S \<inter> T \<noteq> {}"
   using setdist_eq_0_compact_closed [OF T S]
   by (metis Int_commute setdist_sym)
 
 lemma setdist_eq_0_bounded:
-  fixes S :: "'a::{heine_borel,real_normed_vector} set"
+  fixes S :: "'a::heine_borel set"
   assumes "bounded S \<or> bounded T"
-    shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> closure S \<inter> closure T \<noteq> {}"
-  apply (cases "S = {} \<or> T = {}", force)
-  using setdist_eq_0_compact_closed [of "closure S" "closure T"]
-        setdist_eq_0_closed_compact [of "closure S" "closure T"] assms
-  apply (force simp add:  bounded_closure compact_eq_bounded_closed)
-  done
+  shows "setdist S T = 0 \<longleftrightarrow> S = {} \<or> T = {} \<or> closure S \<inter> closure T \<noteq> {}"
+proof (cases "S = {} \<or> T = {}")
+  case False
+  then show ?thesis
+    using setdist_eq_0_compact_closed [of "closure S" "closure T"]
+          setdist_eq_0_closed_compact [of "closure S" "closure T"] assms
+    by (force simp:  bounded_closure compact_eq_bounded_closed)
+qed force
 
 lemma setdist_eq_0_sing_1:
-    fixes S :: "'a::{heine_borel,real_normed_vector} set"
-    shows "setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> closure S"
-  by (auto simp: setdist_eq_0_bounded)
+  "setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> closure S"
+  by (metis in_closure_iff_infdist_zero infdist_def infdist_eq_setdist)
 
 lemma setdist_eq_0_sing_2:
-    fixes S :: "'a::{heine_borel,real_normed_vector} set"
-    shows "setdist S {x} = 0 \<longleftrightarrow> S = {} \<or> x \<in> closure S"
-  by (auto simp: setdist_eq_0_bounded)
+  "setdist S {x} = 0 \<longleftrightarrow> S = {} \<or> x \<in> closure S"
+  by (metis setdist_eq_0_sing_1 setdist_sym)
 
 lemma setdist_neq_0_sing_1:
-    fixes S :: "'a::{heine_borel,real_normed_vector} set"
-    shows "\<lbrakk>setdist {x} S = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> S \<noteq> {} \<and> x \<notin> closure S"
-  by (auto simp: setdist_eq_0_sing_1)
+  "\<lbrakk>setdist {x} S = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> S \<noteq> {} \<and> x \<notin> closure S"
+  by (metis setdist_closure_2 setdist_empty2 setdist_eq_0I singletonI)
 
 lemma setdist_neq_0_sing_2:
-    fixes S :: "'a::{heine_borel,real_normed_vector} set"
-    shows "\<lbrakk>setdist S {x} = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> S \<noteq> {} \<and> x \<notin> closure S"
-  by (auto simp: setdist_eq_0_sing_2)
+  "\<lbrakk>setdist S {x} = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> S \<noteq> {} \<and> x \<notin> closure S"
+  by (simp add: setdist_neq_0_sing_1 setdist_sym)
 
 lemma setdist_sing_in_set:
-    fixes S :: "'a::{heine_borel,real_normed_vector} set"
-    shows "x \<in> S \<Longrightarrow> setdist {x} S = 0"
-  using closure_subset by (auto simp: setdist_eq_0_sing_1)
+   "x \<in> S \<Longrightarrow> setdist {x} S = 0"
+  by (simp add: setdist_eq_0I)
 
 lemma setdist_eq_0_closed:
-  fixes S :: "'a::{heine_borel,real_normed_vector} set"
-  shows  "closed S \<Longrightarrow> (setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> S)"
+   "closed S \<Longrightarrow> (setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> S)"
 by (simp add: setdist_eq_0_sing_1)
 
 lemma setdist_eq_0_closedin:
-  fixes S :: "'a::{heine_borel,real_normed_vector} set"
   shows "\<lbrakk>closedin (subtopology euclidean U) S; x \<in> U\<rbrakk>
          \<Longrightarrow> (setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> S)"
   by (auto simp: closedin_limpt setdist_eq_0_sing_1 closure_def)
 
 lemma setdist_gt_0_closedin:
-  fixes S :: "'a::{heine_borel,real_normed_vector} set"
   shows "\<lbrakk>closedin (subtopology euclidean U) S; x \<in> U; S \<noteq> {}; x \<notin> S\<rbrakk>
          \<Longrightarrow> setdist {x} S > 0"
   using less_eq_real_def setdist_eq_0_closedin by fastforce
diff -r 79c8ff387ed1 -r 5f67c5e457e3 src/HOL/Analysis/Winding_Numbers.thy
--- a/src/HOL/Analysis/Winding_Numbers.thy	Mon Mar 18 21:06:26 2019 +0100
+++ b/src/HOL/Analysis/Winding_Numbers.thy	Mon Mar 18 21:50:51 2019 +0100
@@ -935,11 +935,10 @@
 proof -
   obtain e where "0 < e" and e: "\<And>t. t \<in> {0..1} \<Longrightarrow> e \<le> norm(exp(p t))"
   proof
-     have "closed (path_image (exp \<circ> p))"
-       by (simp add: assms closed_path_image holomorphic_on_exp holomorphic_on_imp_continuous_on path_continuous_image)
+    have "closed (path_image (exp \<circ> p))"
+      by (simp add: assms closed_path_image holomorphic_on_exp holomorphic_on_imp_continuous_on path_continuous_image)
     then show "0 < setdist {0} (path_image (exp \<circ> p))"
-      by (metis (mono_tags, lifting) compact_sing exp_not_eq_zero imageE path_image_compose
-               path_image_nonempty setdist_eq_0_compact_closed setdist_gt_0_compact_closed setdist_eq_0_closed)
+      by (metis exp_not_eq_zero imageE image_comp infdist_eq_setdist infdist_pos_not_in_closed path_defs(4) path_image_nonempty)
   next
     fix t::real
     assume "t \<in> {0..1}"
diff -r 79c8ff387ed1 -r 5f67c5e457e3 src/HOL/Library/Set_Idioms.thy
--- a/src/HOL/Library/Set_Idioms.thy	Mon Mar 18 21:06:26 2019 +0100
+++ b/src/HOL/Library/Set_Idioms.thy	Mon Mar 18 21:50:51 2019 +0100
@@ -44,6 +44,10 @@
 lemma all_intersection_of:
      "(\<forall>S. (P intersection_of Q) S \<longrightarrow> R S) \<longleftrightarrow> (\<forall>T. P T \<and> T \<subseteq> Collect Q \<longrightarrow> R(\<Inter>T))"
   by (auto simp: intersection_of_def)
+             
+lemma intersection_ofE:
+     "\<lbrakk>(P intersection_of Q) S; \<And>T. \<lbrakk>P T; T \<subseteq> Collect Q\<rbrakk> \<Longrightarrow> R(\<Inter>T)\<rbrakk> \<Longrightarrow> R S"
+  by (auto simp: intersection_of_def)
 
 lemma union_of_empty:
      "P {} \<Longrightarrow> (P union_of Q) {}"
@@ -319,6 +323,9 @@
 lemma all_relative_to: "(\<forall>S. (P relative_to U) S \<longrightarrow> Q S) \<longleftrightarrow> (\<forall>S. P S \<longrightarrow> Q(U \<inter> S))"
   by (auto simp: relative_to_def)
 
+lemma relative_toE: "\<lbrakk>(P relative_to U) S; \<And>S. P S \<Longrightarrow> Q(U \<inter> S)\<rbrakk> \<Longrightarrow> Q S"
+  by (auto simp: relative_to_def)
+
 lemma relative_to_inc:
    "P S \<Longrightarrow> (P relative_to U) (U \<inter> S)"
   by (auto simp: relative_to_def)
diff -r 79c8ff387ed1 -r 5f67c5e457e3 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon Mar 18 21:06:26 2019 +0100
+++ b/src/HOL/Limits.thy	Mon Mar 18 21:50:51 2019 +0100
@@ -532,6 +532,9 @@
   shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. dist (f x) (g x))"
   unfolding continuous_on_def by (auto intro: tendsto_dist)
 
+lemma continuous_at_dist: "isCont (dist a) b"
+  using continuous_on_dist [OF continuous_on_const continuous_on_id] continuous_on_eq_continuous_within by blast
+
 lemma tendsto_norm [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. norm (f x)) \<longlongrightarrow> norm a) F"
   unfolding norm_conv_dist by (intro tendsto_intros)