# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1465914861 -3600
# Node ID d3c87eb0bad2c38482f14ff523cdd8bc75d49da6
# Parent  ce995deef4b07e747da7a77e5bed096ee13760d3
new results about topology

diff -r ce995deef4b0 -r d3c87eb0bad2 src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Library/Countable_Set.thy	Tue Jun 14 15:34:21 2016 +0100
@@ -299,6 +299,20 @@
 
 subsection \<open>Misc lemmas\<close>
 
+lemma countable_subset_image:
+   "countable B \<and> B \<subseteq> (f ` A) \<longleftrightarrow> (\<exists>A'. countable A' \<and> A' \<subseteq> A \<and> (B = f ` A'))"
+   (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    apply (rule_tac x="inv_into A f ` B" in exI)
+    apply (auto simp: f_inv_into_f subset_iff image_inv_into_cancel inv_into_into)
+    done
+next
+  assume ?rhs
+  then show ?lhs by force
+qed
+
 lemma infinite_countable_subset':
   assumes X: "infinite X" shows "\<exists>C\<subseteq>X. countable C \<and> infinite C"
 proof -
diff -r ce995deef4b0 -r d3c87eb0bad2 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Limits.thy	Tue Jun 14 15:34:21 2016 +0100
@@ -611,21 +611,21 @@
 
 lemma tendsto_setsum [tendsto_intros]:
   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_add"
-  assumes "\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> a i) F"
-  shows "((\<lambda>x. \<Sum>i\<in>S. f i x) \<longlongrightarrow> (\<Sum>i\<in>S. a i)) F"
-proof (cases "finite S")
-  assume "finite S" thus ?thesis using assms
+  assumes "\<And>i. i \<in> I \<Longrightarrow> (f i \<longlongrightarrow> a i) F"
+  shows "((\<lambda>x. \<Sum>i\<in>I. f i x) \<longlongrightarrow> (\<Sum>i\<in>I. a i)) F"
+proof (cases "finite I")
+  assume "finite I" thus ?thesis using assms
     by (induct, simp, simp add: tendsto_add)
 qed simp
 
 lemma continuous_setsum [continuous_intros]:
   fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_add"
-  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Sum>i\<in>S. f i x)"
+  shows "(\<And>i. i \<in> I \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Sum>i\<in>I. f i x)"
   unfolding continuous_def by (rule tendsto_setsum)
 
 lemma continuous_on_setsum [continuous_intros]:
   fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::topological_comm_monoid_add"
-  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Sum>i\<in>S. f i x)"
+  shows "(\<And>i. i \<in> I \<Longrightarrow> continuous_on S (f i)) \<Longrightarrow> continuous_on S (\<lambda>x. \<Sum>i\<in>I. f i x)"
   unfolding continuous_on_def by (auto intro: tendsto_setsum)
 
 instance nat :: topological_comm_monoid_add
diff -r ce995deef4b0 -r d3c87eb0bad2 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue Jun 14 15:34:21 2016 +0100
@@ -2088,6 +2088,11 @@
     by (simp add: \<open>continuous_on t r\<close> continuous_on_diff continuous_on_id continuous_on_norm)
 qed
 
+lemma closedin_self [simp]:
+    fixes S :: "'a :: real_normed_vector set"
+    shows "closedin (subtopology euclidean S) S"
+  by (simp add: closedin_retract)
+
 lemma retract_of_contractible:
   assumes "contractible t" "s retract_of t"
     shows "contractible s"
@@ -2195,4 +2200,97 @@
 apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+
 done
 
+subsection\<open>Borsuk-style characterization of separation\<close>
+
+lemma continuous_on_Borsuk_map:
+   "a \<notin> s \<Longrightarrow>  continuous_on s (\<lambda>x. inverse(norm (x - a)) *\<^sub>R (x - a))"
+by (rule continuous_intros | force)+
+
+lemma Borsuk_map_into_sphere:
+   "(\<lambda>x. inverse(norm (x - a)) *\<^sub>R (x - a)) ` s \<subseteq> sphere 0 1 \<longleftrightarrow> (a \<notin> s)"
+  by auto (metis eq_iff_diff_eq_0 left_inverse norm_eq_zero)
+
+lemma Borsuk_maps_homotopic_in_path_component:
+  assumes "path_component (- s) a b"
+    shows "homotopic_with (\<lambda>x. True) s (sphere 0 1)
+                   (\<lambda>x. inverse(norm(x - a)) *\<^sub>R (x - a))
+                   (\<lambda>x. inverse(norm(x - b)) *\<^sub>R (x - b))"
+proof -
+  obtain g where "path g" "path_image g \<subseteq> -s" "pathstart g = a" "pathfinish g = b"
+    using assms by (auto simp: path_component_def)
+  then show ?thesis
+    apply (simp add: path_def path_image_def pathstart_def pathfinish_def homotopic_with_def)
+    apply (rule_tac x = "\<lambda>z. inverse(norm(snd z - (g o fst)z)) *\<^sub>R (snd z - (g o fst)z)" in exI)
+    apply (intro conjI continuous_intros)
+    apply (rule continuous_intros | erule continuous_on_subset | fastforce simp: divide_simps sphere_def)+
+    done
+qed
+
+lemma non_extensible_Borsuk_map:
+  fixes a :: "'a :: euclidean_space"
+  assumes "compact s" and cin: "c \<in> components(- s)" and boc: "bounded c" and "a \<in> c"
+    shows "~ (\<exists>g. continuous_on (s \<union> c) g \<and>
+                  g ` (s \<union> c) \<subseteq> sphere 0 1 \<and>
+                  (\<forall>x \<in> s. g x = inverse(norm(x - a)) *\<^sub>R (x - a)))"
+proof -
+  have "closed s" using assms by (simp add: compact_imp_closed)
+  have "c \<subseteq> -s"
+    using assms by (simp add: in_components_subset)
+  with \<open>a \<in> c\<close> have "a \<notin> s" by blast
+  then have ceq: "c = connected_component_set (- s) a"
+    by (metis \<open>a \<in> c\<close> cin components_iff connected_component_eq)
+  then have "bounded (s \<union> connected_component_set (- s) a)"
+    using \<open>compact s\<close> boc compact_imp_bounded by auto
+  with bounded_subset_ballD obtain r where "0 < r" and r: "(s \<union> connected_component_set (- s) a) \<subseteq> ball a r"
+    by blast
+  { fix g
+    assume "continuous_on (s \<union> c) g"
+            "g ` (s \<union> c) \<subseteq> sphere 0 1"
+       and [simp]: "\<And>x. x \<in> s \<Longrightarrow> g x = (x - a) /\<^sub>R norm (x - a)"
+    then have [simp]: "\<And>x. x \<in> s \<union> c \<Longrightarrow> norm (g x) = 1"
+      by force
+    have cb_eq: "cball a r = (s \<union> connected_component_set (- s) a) \<union>
+                      (cball a r - connected_component_set (- s) a)"
+      using ball_subset_cball [of a r] r by auto
+    have cont1: "continuous_on (s \<union> connected_component_set (- s) a)
+                     (\<lambda>x. a + r *\<^sub>R g x)"
+      apply (rule continuous_intros)+
+      using \<open>continuous_on (s \<union> c) g\<close> ceq by blast
+    have cont2: "continuous_on (cball a r - connected_component_set (- s) a)
+            (\<lambda>x. a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
+      by (rule continuous_intros | force simp: \<open>a \<notin> s\<close>)+
+    have 1: "continuous_on (cball a r)
+             (\<lambda>x. if connected_component (- s) a x
+                  then a + r *\<^sub>R g x
+                  else a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
+      apply (subst cb_eq)
+      apply (rule continuous_on_cases [OF _ _ cont1 cont2])
+        using ceq cin
+      apply (auto intro: closed_Un_complement_component
+                  simp: \<open>closed s\<close> open_Compl open_connected_component)
+      done
+    have 2: "(\<lambda>x. a + r *\<^sub>R g x) ` (cball a r \<inter> connected_component_set (- s) a)
+             \<subseteq> sphere a r "
+      using \<open>0 < r\<close> by (force simp: dist_norm ceq)
+    have "retraction (cball a r) (sphere a r)
+            (\<lambda>x. if x \<in> connected_component_set (- s) a
+                 then a + r *\<^sub>R g x
+                 else a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
+      using  \<open>0 < r\<close>
+      apply (simp add: retraction_def dist_norm 1 2, safe)
+      apply (force simp: dist_norm abs_if mult_less_0_iff divide_simps \<open>a \<notin> s\<close>)
+      using r
+      by (auto simp: dist_norm norm_minus_commute)
+    then have False
+      using no_retraction_cball
+             [OF \<open>0 < r\<close>, of a, unfolded retract_of_def, simplified, rule_format,
+              of "\<lambda>x. if x \<in> connected_component_set (- s) a
+                      then a + r *\<^sub>R g x
+                      else a + r *\<^sub>R inverse(norm(x - a)) *\<^sub>R (x - a)"]
+      by blast
+  }
+  then show ?thesis
+    by blast
+qed
+
 end
diff -r ce995deef4b0 -r d3c87eb0bad2 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Jun 14 15:34:21 2016 +0100
@@ -6196,7 +6196,7 @@
     done
 qed
 
-lemma midpoint_eq_endpoint:
+lemma midpoint_eq_endpoint [simp]:
   "midpoint a b = a \<longleftrightarrow> a = b"
   "midpoint a b = b \<longleftrightarrow> a = b"
   unfolding midpoint_eq_iff by auto
@@ -6432,6 +6432,17 @@
 apply (simp add: convex_contains_open_segment, clarify)
 by (metis (no_types, hide_lams) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment)
 
+lemma csegment_midpoint_subset: "closed_segment (midpoint a b) b \<subseteq> closed_segment a b"
+  apply (clarsimp simp: midpoint_def in_segment)
+  apply (rule_tac x="(1 + u) / 2" in exI)
+  apply (auto simp: algebra_simps add_divide_distrib diff_divide_distrib)
+  by (metis real_sum_of_halves scaleR_left.add)
+
+lemma notin_segment_midpoint:
+  fixes a :: "'a :: euclidean_space"
+  shows "a \<noteq> b \<Longrightarrow> a \<notin> closed_segment (midpoint a b) b"
+by (auto simp: dist_midpoint dest!: dist_in_closed_segment)
+
 subsubsection\<open>More lemmas, especially for working with the underlying formula\<close>
 
 lemma segment_eq_compose:
@@ -10243,7 +10254,7 @@
 lemma setdist_empty2 [simp]: "setdist t {} = 0"
   by (simp add: setdist_def)
 
-lemma setdist_pos_le: "0 \<le> setdist s t"
+lemma setdist_pos_le [simp]: "0 \<le> setdist s t"
   by (auto simp: setdist_def ex_in_conv [symmetric] intro: cInf_greatest)
 
 lemma le_setdistI:
@@ -10307,10 +10318,10 @@
   apply (subst setdist_singletons [symmetric])
   by (metis abs_diff_le_iff diff_le_eq setdist_triangle setdist_sym)
 
-lemma continuous_at_setdist: "continuous (at x) (\<lambda>y. (setdist {y} s))"
+lemma continuous_at_setdist [continuous_intros]: "continuous (at x) (\<lambda>y. (setdist {y} s))"
   by (force simp: continuous_at_eps_delta dist_real_def intro: le_less_trans [OF setdist_Lipschitz])
 
-lemma continuous_on_setdist: "continuous_on t (\<lambda>y. (setdist {y} s))"
+lemma continuous_on_setdist [continuous_intros]: "continuous_on t (\<lambda>y. (setdist {y} s))"
   by (metis continuous_at_setdist continuous_at_imp_continuous_on)
 
 lemma uniformly_continuous_on_setdist: "uniformly_continuous_on t (\<lambda>y. (setdist {y} s))"
@@ -10424,34 +10435,44 @@
   apply (auto simp: closest_point_in_set)
   done
 
-lemma setdist_eq_0_sing_1 [simp]:
-  fixes s :: "'a::euclidean_space set"
-  shows "setdist {x} s = 0 \<longleftrightarrow> s = {} \<or> x \<in> closure s"
-by (auto simp: setdist_eq_0_bounded)
-
-lemma setdist_eq_0_sing_2 [simp]:
-  fixes s :: "'a::euclidean_space set"
-  shows "setdist s {x} = 0 \<longleftrightarrow> s = {} \<or> x \<in> closure s"
-by (auto simp: setdist_eq_0_bounded)
+lemma setdist_eq_0_sing_1:
+    fixes s :: "'a::euclidean_space set"
+    shows "setdist {x} s = 0 \<longleftrightarrow> s = {} \<or> x \<in> closure s"
+  by (auto simp: setdist_eq_0_bounded)
+
+lemma setdist_eq_0_sing_2:
+    fixes s :: "'a::euclidean_space set"
+    shows "setdist s {x} = 0 \<longleftrightarrow> s = {} \<or> x \<in> closure s"
+  by (auto simp: setdist_eq_0_bounded)
 
 lemma setdist_neq_0_sing_1:
     fixes s :: "'a::euclidean_space set"
     shows "\<lbrakk>setdist {x} s = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> s \<noteq> {} \<and> x \<notin> closure s"
-by auto
+  by (auto simp: setdist_eq_0_sing_1)
 
 lemma setdist_neq_0_sing_2:
-  fixes s :: "'a::euclidean_space set"
+    fixes s :: "'a::euclidean_space set"
     shows "\<lbrakk>setdist s {x} = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> s \<noteq> {} \<and> x \<notin> closure s"
-by auto
+  by (auto simp: setdist_eq_0_sing_2)
 
 lemma setdist_sing_in_set:
-  fixes s :: "'a::euclidean_space set"
-  shows "x \<in> s \<Longrightarrow> setdist {x} s = 0"
-using closure_subset by force
+    fixes s :: "'a::euclidean_space set"
+    shows "x \<in> s \<Longrightarrow> setdist {x} s = 0"
+  using closure_subset by (auto simp: setdist_eq_0_sing_1)
 
 lemma setdist_le_sing: "x \<in> s ==> setdist s t \<le> setdist {x} t"
   using setdist_subset_left by auto
 
+lemma setdist_eq_0_closed:
+  fixes s :: "'a::euclidean_space set"
+  shows  "closed s \<Longrightarrow> (setdist {x} s = 0 \<longleftrightarrow> s = {} \<or> x \<in> s)"
+by (simp add: setdist_eq_0_sing_1)
+
+lemma setdist_eq_0_closedin:
+  fixes s :: "'a::euclidean_space set"
+  shows "\<lbrakk>closedin (subtopology euclidean u) s; x \<in> u\<rbrakk>
+         \<Longrightarrow> (setdist {x} s = 0 \<longleftrightarrow> s = {} \<or> x \<in> s)"
+  by (auto simp: closedin_limpt setdist_eq_0_sing_1 closure_def)
 
 subsection\<open>Basic lemmas about hyperplanes and halfspaces\<close>
 
@@ -10506,6 +10527,294 @@
 using halfspace_eq_empty_le [of "-a" "-b"]
 by simp
 
+subsection\<open>Use set distance for an easy proof of separation properties\<close>
+
+proposition separation_closures:
+  fixes S :: "'a::euclidean_space set"
+  assumes "S \<inter> closure T = {}" "T \<inter> closure S = {}"
+  obtains U V where "U \<inter> V = {}" "open U" "open V" "S \<subseteq> U" "T \<subseteq> V"
+proof (cases "S = {} \<or> T = {}")
+  case True with that show ?thesis by auto
+next
+  case False
+  define f where "f \<equiv> \<lambda>x. setdist {x} T - setdist {x} S"
+  have contf: "\<And>x. isCont f x"
+    unfolding f_def by (intro continuous_intros continuous_at_setdist)
+  show ?thesis
+  proof (rule_tac U = "{x. f x > 0}" and V = "{x. f x < 0}" in that)
+    show "{x. 0 < f x} \<inter> {x. f x < 0} = {}"
+      by auto
+    show "open {x. 0 < f x}"
+      by (simp add: open_Collect_less contf)
+    show "open {x. f x < 0}"
+      by (simp add: open_Collect_less contf)
+    show "S \<subseteq> {x. 0 < f x}"
+      apply (clarsimp simp add: f_def setdist_sing_in_set)
+      using assms
+      by (metis False IntI empty_iff le_less setdist_eq_0_sing_2 setdist_pos_le setdist_sym)
+    show "T \<subseteq> {x. f x < 0}"
+      apply (clarsimp simp add: f_def setdist_sing_in_set)
+      using assms
+      by (metis False IntI empty_iff le_less setdist_eq_0_sing_2 setdist_pos_le setdist_sym)
+  qed
+qed
+
+lemma separation_normal:
+  fixes S :: "'a::euclidean_space set"
+  assumes "closed S" "closed T" "S \<inter> T = {}"
+  obtains U V where "open U" "open V" "S \<subseteq> U" "T \<subseteq> V" "U \<inter> V = {}"
+using separation_closures [of S T]
+by (metis assms closure_closed disjnt_def inf_commute)
+
+
+lemma separation_normal_local:
+  fixes S :: "'a::euclidean_space set"
+  assumes US: "closedin (subtopology euclidean U) S"
+      and UT: "closedin (subtopology euclidean U) T"
+      and "S \<inter> T = {}"
+  obtains S' T' where "openin (subtopology euclidean U) S'"
+                      "openin (subtopology euclidean U) T'"
+                      "S \<subseteq> S'"  "T \<subseteq> T'"  "S' \<inter> T' = {}"
+proof (cases "S = {} \<or> T = {}")
+  case True with that show ?thesis
+    apply safe
+    using UT closedin_subset apply blast
+    using US closedin_subset apply blast
+    done
+next
+  case False
+  define f where "f \<equiv> \<lambda>x. setdist {x} T - setdist {x} S"
+  have contf: "continuous_on U f"
+    unfolding f_def by (intro continuous_intros)
+  show ?thesis
+  proof (rule_tac S' = "{x\<in>U. f x > 0}" and T' = "{x\<in>U. f x < 0}" in that)
+    show "{x \<in> U. 0 < f x} \<inter> {x \<in> U. f x < 0} = {}"
+      by auto
+    have "openin (subtopology euclidean U) {x \<in> U. f x \<in> {0<..}}"
+      apply (rule continuous_openin_preimage [where T=UNIV])
+        apply (simp_all add: contf)
+      using open_greaterThan open_openin by blast
+    then show "openin (subtopology euclidean U) {x \<in> U. 0 < f x}" by simp
+  next
+    have "openin (subtopology euclidean U) {x \<in> U. f x \<in> {..<0}}"
+      apply (rule continuous_openin_preimage [where T=UNIV])
+        apply (simp_all add: contf)
+      using open_lessThan open_openin by blast
+    then show "openin (subtopology euclidean U) {x \<in> U. f x < 0}" by simp
+  next
+    show "S \<subseteq> {x \<in> U. 0 < f x}"
+      apply (clarsimp simp add: f_def setdist_sing_in_set)
+      using assms
+      by (metis False Int_insert_right closedin_imp_subset empty_not_insert insert_absorb insert_subset linorder_neqE_linordered_idom not_le setdist_eq_0_closedin setdist_pos_le)
+    show "T \<subseteq> {x \<in> U. f x < 0}"
+      apply (clarsimp simp add: f_def setdist_sing_in_set)
+      using assms
+      by (metis False closedin_subset disjoint_iff_not_equal insert_absorb insert_subset linorder_neqE_linordered_idom not_less setdist_eq_0_closedin setdist_pos_le topspace_euclidean_subtopology)
+  qed
+qed
+
+lemma separation_normal_compact:
+  fixes S :: "'a::euclidean_space set"
+  assumes "compact S" "closed T" "S \<inter> T = {}"
+  obtains U V where "open U" "compact(closure U)" "open V" "S \<subseteq> U" "T \<subseteq> V" "U \<inter> V = {}"
+proof -
+  have "closed S" "bounded S"
+    using assms by (auto simp: compact_eq_bounded_closed)
+  then obtain r where "r>0" and r: "S \<subseteq> ball 0 r"
+    by (auto dest!: bounded_subset_ballD)
+  have **: "closed (T \<union> - ball 0 r)" "S \<inter> (T \<union> - ball 0 r) = {}"
+    using assms r by blast+
+  then show ?thesis
+    apply (rule separation_normal [OF \<open>closed S\<close>])
+    apply (rule_tac U=U and V=V in that)
+    by auto (meson bounded_ball bounded_subset compl_le_swap2 disjoint_eq_subset_Compl)
+qed
+
+subsection\<open>Proper maps, including projections out of compact sets\<close>
+
+lemma finite_indexed_bound:
+  assumes A: "finite A" "\<And>x. x \<in> A \<Longrightarrow> \<exists>n::'a::linorder. P x n"
+    shows "\<exists>m. \<forall>x \<in> A. \<exists>k\<le>m. P x k"
+using A
+proof (induction A)
+  case empty then show ?case by force
+next
+  case (insert a A)
+    then obtain m n where "\<forall>x \<in> A. \<exists>k\<le>m. P x k" "P a n"
+      by force
+    then show ?case
+      apply (rule_tac x="max m n" in exI, safe)
+      using max.cobounded2 apply blast
+      by (meson le_max_iff_disj)
+qed
+
+proposition proper_map:
+  fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
+  assumes "closedin (subtopology euclidean S) K"
+      and com: "\<And>U. \<lbrakk>U \<subseteq> T; compact U\<rbrakk> \<Longrightarrow> compact {x \<in> S. f x \<in> U}"
+      and "f ` S \<subseteq> T"
+    shows "closedin (subtopology euclidean T) (f ` K)"
+proof -
+  have "K \<subseteq> S"
+    using assms closedin_imp_subset by metis
+  obtain C where "closed C" and Keq: "K = S \<inter> C"
+    using assms by (auto simp: closedin_closed)
+  have *: "y \<in> f ` K" if "y \<in> T" and y: "y islimpt f ` K" for y
+  proof -
+    obtain h where "\<forall>n. (\<exists>x\<in>K. h n = f x) \<and> h n \<noteq> y" "inj h" and hlim: "(h \<longlongrightarrow> y) sequentially"
+      using \<open>y \<in> T\<close> y by (force simp: limpt_sequential_inj)
+    then obtain X where X: "\<And>n. X n \<in> K \<and> h n = f (X n) \<and> h n \<noteq> y"
+      by metis
+    then have fX: "\<And>n. f (X n) = h n"
+      by metis
+    have "compact (C \<inter> {a \<in> S. f a \<in> insert y (range (\<lambda>i. f(X(n + i))))})" for n
+      apply (rule closed_Int_compact [OF \<open>closed C\<close>])
+      apply (rule com)
+       using X \<open>K \<subseteq> S\<close> \<open>f ` S \<subseteq> T\<close> \<open>y \<in> T\<close> apply blast
+      apply (rule compact_sequence_with_limit)
+      apply (simp add: fX add.commute [of n] LIMSEQ_ignore_initial_segment [OF hlim])
+      done
+    then have comf: "compact {a \<in> K. f a \<in> insert y (range (\<lambda>i. f(X(n + i))))}" for n
+      by (simp add: Keq Int_def conj_commute)
+    have ne: "\<Inter>\<F> \<noteq> {}"
+             if "finite \<F>"
+                and \<F>: "\<And>t. t \<in> \<F> \<Longrightarrow>
+                           (\<exists>n. t = {a \<in> K. f a \<in> insert y (range (\<lambda>i. f (X (n + i))))})"
+             for \<F>
+    proof -
+      obtain m where m: "\<And>t. t \<in> \<F> \<Longrightarrow> \<exists>k\<le>m. t = {a \<in> K. f a \<in> insert y (range (\<lambda>i. f (X (k + i))))}"
+        apply (rule exE)
+        apply (rule finite_indexed_bound [OF \<open>finite \<F>\<close> \<F>], assumption, force)
+        done
+      have "X m \<in> \<Inter>\<F>"
+        using X le_Suc_ex by (fastforce dest: m)
+      then show ?thesis by blast
+    qed
+    have "\<Inter>{{a. a \<in> K \<and> f a \<in> insert y (range (\<lambda>i. f(X(n + i))))} |n. n \<in> UNIV}
+               \<noteq> {}"
+      apply (rule compact_fip_heine_borel)
+       using comf apply force
+      using ne  apply (simp add: subset_iff del: insert_iff)
+      done
+    then have "\<exists>x. x \<in> (\<Inter>n. {a \<in> K. f a \<in> insert y (range (\<lambda>i. f (X (n + i))))})"
+      by blast
+    then show ?thesis
+      apply (simp add: image_iff fX)
+      by (metis \<open>inj h\<close> le_add1 not_less_eq_eq rangeI range_ex1_eq)
+  qed
+  with assms closedin_subset show ?thesis
+    by (force simp: closedin_limpt)
+qed
+
+
+lemma compact_continuous_image_eq:
+  fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
+  assumes f: "inj_on f S"
+  shows "continuous_on S f \<longleftrightarrow> (\<forall>T. compact T \<and> T \<subseteq> S \<longrightarrow> compact(f ` T))"
+           (is "?lhs = ?rhs")
+proof
+  assume ?lhs then show ?rhs
+    by (metis continuous_on_subset compact_continuous_image)
+next
+  assume RHS: ?rhs
+  obtain g where gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
+    by (metis inv_into_f_f f)
+  then have *: "{x \<in> S. f x \<in> U} = g ` U" if "U \<subseteq> f ` S" for U
+    using that by fastforce
+  have gfim: "g ` f ` S \<subseteq> S" using gf by auto
+  have **: "compact {x \<in> f ` S. g x \<in> C}" if C: "C \<subseteq> S" "compact C" for C
+  proof -
+    obtain h :: "'a set \<Rightarrow> 'a" where "h C \<in> C \<and> h C \<notin> S \<or> compact (f ` C)"
+      by (force simp: C RHS)
+    moreover have "f ` C = {b \<in> f ` S. g b \<in> C}"
+      using C gf by auto
+    ultimately show "compact {b \<in> f ` S. g b \<in> C}"
+      using C by auto
+  qed
+  show ?lhs
+    using proper_map [OF _ _ gfim] **
+    by (simp add: continuous_on_closed * closedin_imp_subset)
+qed
+
+lemma proper_map_from_compact:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes contf: "continuous_on S f" and imf: "f ` S \<subseteq> T" and "compact S"
+          "closedin (subtopology euclidean T) K"
+  shows "compact {x. x \<in> S \<and> f x \<in> K}"
+by (rule closedin_compact [OF \<open>compact S\<close>] continuous_closedin_preimage_gen assms)+
+
+lemma proper_map_fst:
+  assumes "compact T" "K \<subseteq> S" "compact K"
+    shows "compact {z \<in> S \<times> T. fst z \<in> K}"
+proof -
+  have "{z \<in> S \<times> T. fst z \<in> K} = K \<times> T"
+    using assms by auto
+  then show ?thesis by (simp add: assms compact_Times)
+qed
+
+lemma closed_map_fst:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "compact T" "closedin (subtopology euclidean (S \<times> T)) c"
+   shows "closedin (subtopology euclidean S) (fst ` c)"
+proof -
+  have *: "fst ` (S \<times> T) \<subseteq> S"
+    by auto
+  show ?thesis
+    using proper_map [OF _ _ *] by (simp add: proper_map_fst assms)
+qed
+
+lemma proper_map_snd:
+  assumes "compact S" "K \<subseteq> T" "compact K"
+    shows "compact {z \<in> S \<times> T. snd z \<in> K}"
+proof -
+  have "{z \<in> S \<times> T. snd z \<in> K} = S \<times> K"
+    using assms by auto
+  then show ?thesis by (simp add: assms compact_Times)
+qed
+
+lemma closed_map_snd:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "compact S" "closedin (subtopology euclidean (S \<times> T)) c"
+   shows "closedin (subtopology euclidean T) (snd ` c)"
+proof -
+  have *: "snd ` (S \<times> T) \<subseteq> T"
+    by auto
+  show ?thesis
+    using proper_map [OF _ _ *] by (simp add: proper_map_snd assms)
+qed
+
+lemma closedin_compact_projection:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "compact S" and clo: "closedin (subtopology euclidean (S \<times> T)) U"
+    shows "closedin (subtopology euclidean T) {y. \<exists>x. x \<in> S \<and> (x, y) \<in> U}"
+proof -
+  have "U \<subseteq> S \<times> T"
+    by (metis clo closedin_imp_subset)
+  then have "{y. \<exists>x. x \<in> S \<and> (x, y) \<in> U} = snd ` U"
+    by force
+  moreover have "closedin (subtopology euclidean T) (snd ` U)"
+    by (rule closed_map_snd [OF assms])
+  ultimately show ?thesis
+    by simp
+qed
+
+
+lemma closed_compact_projection:
+  fixes S :: "'a::euclidean_space set"
+    and T :: "('a * 'b::euclidean_space) set"
+  assumes "compact S" and clo: "closed T"
+    shows "closed {y. \<exists>x. x \<in> S \<and> (x, y) \<in> T}"
+proof -
+  have *: "{y. \<exists>x. x \<in> S \<and> Pair x y \<in> T} =
+        {y. \<exists>x. x \<in> S \<and> Pair x y \<in> ((S \<times> UNIV) \<inter> T)}"
+    by auto
+  show ?thesis
+    apply (subst *)
+    apply (rule closedin_closed_trans [OF _ closed_UNIV])
+    apply (rule closedin_compact_projection [OF \<open>compact S\<close>])
+    by (simp add: clo closedin_closed_Int)
+qed
+
 subsubsection\<open>Representing affine hull as a finite intersection of hyperplanes\<close>
 
 proposition affine_hull_convex_Int_nonempty_interior:
@@ -12082,4 +12391,151 @@
     by (rule that)
 qed
 
+subsection\<open>Several Variants of Paracompactness\<close>
+
+proposition paracompact:
+  fixes S :: "'a :: euclidean_space 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> {})}"
+proof (cases "S = {}")
+  case True with that show ?thesis by blast
+next
+  case False
+  have "\<exists>T U. x \<in> U \<and> open U \<and> closure U \<subseteq> T \<and> T \<in> \<C>" if "x \<in> S" for x
+  proof -
+    obtain T where "x \<in> T" "T \<in> \<C>" "open T"
+      using assms \<open>x \<in> S\<close> by blast
+    then obtain e where "e > 0" "cball x e \<subseteq> T"
+      by (force simp: open_contains_cball)
+    then show ?thesis
+      apply (rule_tac x = T in exI)
+      apply (rule_tac x = "ball x e" in exI)
+      using  \<open>T \<in> \<C>\<close>
+      apply (simp add: closure_minimal)
+      done
+  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>"
+         if "x \<in> S" for x
+    by metis
+  then obtain \<F> where "\<F> \<subseteq> G ` S" "countable \<F>" "\<Union>\<F> = UNION S G"
+    using Lindelof [of "G ` S"] by (metis image_iff)
+  then obtain K where K: "K \<subseteq> S" "countable K" and eq: "UNION K G = UNION S G"
+    by (metis countable_subset_image)
+  with False Gin have "K \<noteq> {}" by force
+  then obtain a :: "nat \<Rightarrow> 'a" where "range a = K"
+    by (metis range_from_nat_into \<open>countable K\<close>)
+  then have odif: "\<And>n. open (F (a n) - \<Union>{closure (G (a m)) |m. m < n})"
+    using \<open>K \<subseteq> S\<close> Fin opC by (fastforce simp add:)
+  let ?C = "range (\<lambda>n. F(a n) - \<Union>{closure(G(a m)) |m. m < n})"
+  have enum_S: "\<exists>n. x \<in> F(a n) \<and> x \<in> G(a n)" if "x \<in> S" for x
+  proof -
+    have "\<exists>y \<in> K. x \<in> G y" using eq that Gin by fastforce
+    then show ?thesis
+      using clos K \<open>range a = K\<close> closure_subset by blast
+  qed
+  have 1: "S \<subseteq> Union ?C"
+  proof
+    fix x assume "x \<in> S"
+    define n where "n \<equiv> LEAST n. x \<in> F(a n)"
+    have n: "x \<in> F(a n)"
+      using enum_S [OF \<open>x \<in> S\<close>] by (force simp: n_def intro: LeastI)
+    have notn: "x \<notin> F(a m)" if "m < n" for m
+      using that not_less_Least by (force simp: n_def)
+    then have "x \<notin> \<Union>{closure (G (a m)) |m. m < n}"
+      using n \<open>K \<subseteq> S\<close> \<open>range a = K\<close> clos notn by fastforce
+    with n show "x \<in> Union ?C"
+      by blast
+  qed
+  have 3: "\<exists>V. open V \<and> x \<in> V \<and> finite {U. U \<in> ?C \<and> (U \<inter> V \<noteq> {})}" if "x \<in> S" for x
+  proof -
+    obtain n where n: "x \<in> F(a n)" "x \<in> G(a n)"
+      using \<open>x \<in> S\<close> enum_S by auto
+    have "{U \<in> ?C. U \<inter> G (a n) \<noteq> {}} \<subseteq> (\<lambda>n. F(a n) - \<Union>{closure(G(a m)) |m. m < n}) ` atMost n"
+    proof clarsimp
+      fix k  assume "(F (a k) - \<Union>{closure (G (a m)) |m. m < k}) \<inter> G (a n) \<noteq> {}"
+      then have "k \<le> n"
+        by auto (metis closure_subset not_le subsetCE)
+      then show "F (a k) - \<Union>{closure (G (a m)) |m. m < k}
+                 \<in> (\<lambda>n. F (a n) - \<Union>{closure (G (a m)) |m. m < n}) ` {..n}"
+        by force
+    qed
+    moreover have "finite ((\<lambda>n. F(a n) - \<Union>{closure(G(a m)) |m. m < n}) ` atMost n)"
+      by force
+    ultimately have *: "finite {U \<in> ?C. U \<inter> G (a n) \<noteq> {}}"
+      using finite_subset by blast
+    show ?thesis
+      apply (rule_tac x="G (a n)" in exI)
+      apply (intro conjI oG n *)
+      using \<open>K \<subseteq> S\<close> \<open>range a = K\<close> apply blast
+      done
+  qed
+  show ?thesis
+    apply (rule that [OF 1 _ 3])
+    using Fin \<open>K \<subseteq> S\<close> \<open>range a = K\<close>  apply (auto simp: odif)
+    done
+qed
+
+
+corollary paracompact_closedin:
+  fixes S :: "'a :: euclidean_space 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>"
+  obtains \<C>' where "S \<subseteq> \<Union> \<C>'"
+               and "\<And>V. V \<in> \<C>' \<Longrightarrow> openin (subtopology euclidean U) V \<and> (\<exists>T. T \<in> \<C> \<and> V \<subseteq> T)"
+               and "\<And>x. x \<in> U
+                       \<Longrightarrow> \<exists>V. openin (subtopology euclidean U) V \<and> x \<in> V \<and>
+                               finite {X. X \<in> \<C>' \<and> (X \<inter> V \<noteq> {})}"
+proof -
+  have "\<exists>Z. open Z \<and> (T = U \<inter> Z)" if "T \<in> \<C>" for T
+    using oin [OF that] by (auto simp: openin_open)
+  then obtain F where opF: "open (F T)" and intF: "U \<inter> F T = T" if "T \<in> \<C>" for T
+    by metis
+  obtain K where K: "closed K" "U \<inter> K = S"
+    using cin by (auto simp: closedin_closed)
+  have 1: "U \<subseteq> \<Union>insert (- K) (F ` \<C>)"
+    by clarsimp (metis Int_iff Union_iff \<open>U \<inter> K = S\<close> \<open>S \<subseteq> \<Union>\<C>\<close> subsetD intF)
+  have 2: "\<And>T. T \<in> insert (- K) (F ` \<C>) \<Longrightarrow> open T"
+    using \<open>closed K\<close> by (auto simp: opF)
+  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
+  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)
+    show "S \<subseteq> \<Union>?C"
+      using \<open>U \<inter> K = S\<close> \<open>U \<subseteq> \<Union>\<D>\<close> K by (blast dest!: subsetD)
+    show "\<And>V. V \<in> ?C \<Longrightarrow> openin (subtopology euclidean U) V \<and> (\<exists>T. T \<in> \<C> \<and> V \<subseteq> T)"
+      using D1 intF by fastforce
+    have *: "{X. (\<exists>V. X = U \<inter> V \<and> V \<in> \<D> \<and> V \<inter> K \<noteq> {}) \<and> X \<inter> (U \<inter> V) \<noteq> {}} \<subseteq>
+             (\<lambda>x. U \<inter> x) ` {U \<in> \<D>. U \<inter> V \<noteq> {}}" for V
+      by blast
+    show "\<exists>V. openin (subtopology euclidean U) V \<and> x \<in> V \<and> finite {X \<in> ?C. X \<inter> V \<noteq> {}}"
+         if "x \<in> U" for x
+      using D2 [OF that]
+      apply clarify
+      apply (rule_tac x="U \<inter> V" in exI)
+      apply (auto intro: that finite_subset [OF *])
+      done
+    qed
+qed
+
+corollary paracompact_closed:
+  fixes S :: "'a :: euclidean_space set"
+  assumes "closed S"
+      and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
+      and "S \<subseteq> \<Union>\<C>"
+  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. \<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 simp: open_openin [symmetric] closed_closedin [symmetric])
+
 end
diff -r ce995deef4b0 -r d3c87eb0bad2 src/HOL/Multivariate_Analysis/Homeomorphism.thy
--- a/src/HOL/Multivariate_Analysis/Homeomorphism.thy	Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Homeomorphism.thy	Tue Jun 14 15:34:21 2016 +0100
@@ -933,7 +933,8 @@
       by (simp add: \<open>open U\<close> closed_Compl)
     define f :: "'a \<Rightarrow> 'a \<times> 'b" where "f \<equiv> \<lambda>x. (x, One /\<^sub>R setdist {x} (- U))"
     have "continuous_on U (\<lambda>x. (x, One /\<^sub>R setdist {x} (- U)))"
-      by (auto simp: Ucomp continuous_intros continuous_on_setdist)
+      apply (intro continuous_intros continuous_on_setdist)
+      by (simp add: Ucomp setdist_eq_0_sing_1)
     then have homU: "homeomorphism U (f`U) f fst"
       by (auto simp: f_def homeomorphism_def image_iff continuous_intros)
     have cloS: "closedin (subtopology euclidean U) S"
@@ -945,9 +946,9 @@
     have *: "r *\<^sub>R b = One \<Longrightarrow> b = (1 / r) *\<^sub>R One" for r and b::'b
       by (metis One_non_0 nonzero_divide_eq_eq real_vector.scale_eq_0_iff real_vector.scale_scale scaleR_one)
     have "f ` U = {z. (setdist {fst z} (- U) *\<^sub>R snd z) \<in> {One}}"
-      apply (auto simp: f_def field_simps Ucomp)
+      apply (auto simp: f_def setdist_eq_0_sing_1 field_simps Ucomp)
       apply (rule_tac x=a in image_eqI)
-      apply (auto simp: * dest: setdist1D)
+      apply (auto simp: * setdist_eq_0_sing_1 dest: setdist1D)
       done
     then have clfU: "closed (f ` U)"
       apply (rule ssubst)
@@ -1103,4 +1104,176 @@
   using assms
   by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)
 
+subsection\<open>Covering spaces and lifting results for them\<close>
+
+definition covering_space
+           :: "'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
+  where
+  "covering_space c p s \<equiv>
+       continuous_on c p \<and> p ` c = s \<and>
+       (\<forall>x \<in> s. \<exists>t. x \<in> t \<and> openin (subtopology euclidean s) t \<and>
+                    (\<exists>v. \<Union>v = {x. x \<in> c \<and> p x \<in> t} \<and>
+                        (\<forall>u \<in> v. openin (subtopology euclidean c) u) \<and>
+                        pairwise disjnt v \<and>
+                        (\<forall>u \<in> v. \<exists>q. homeomorphism u t p q)))"
+
+lemma covering_space_imp_continuous: "covering_space c p s \<Longrightarrow> continuous_on c p"
+  by (simp add: covering_space_def)
+
+lemma covering_space_imp_surjective: "covering_space c p s \<Longrightarrow> p ` c = s"
+  by (simp add: covering_space_def)
+
+lemma homeomorphism_imp_covering_space: "homeomorphism s t f g \<Longrightarrow> covering_space s f t"
+  apply (simp add: homeomorphism_def covering_space_def, clarify)
+  apply (rule_tac x=t in exI, simp)
+  apply (rule_tac x="{s}" in exI, auto)
+  done
+
+lemma covering_space_local_homeomorphism:
+  assumes "covering_space c p s" "x \<in> c"
+  obtains t u q where "x \<in> t" "openin (subtopology euclidean c) t"
+                      "p x \<in> u" "openin (subtopology euclidean s) u"
+                      "homeomorphism t u p q"
+using assms
+apply (simp add: covering_space_def, clarify)
+apply (drule_tac x="p x" in bspec, force)
+by (metis (no_types, lifting) Union_iff mem_Collect_eq)
+
+
+lemma covering_space_local_homeomorphism_alt:
+  assumes p: "covering_space c p s" and "y \<in> s"
+  obtains x t u q where "p x = y"
+                        "x \<in> t" "openin (subtopology euclidean c) t"
+                        "y \<in> u" "openin (subtopology euclidean s) u"
+                          "homeomorphism t u p q"
+proof -
+  obtain x where "p x = y" "x \<in> c"
+    using assms covering_space_imp_surjective by blast
+  show ?thesis
+    apply (rule covering_space_local_homeomorphism [OF p \<open>x \<in> c\<close>])
+    using that \<open>p x = y\<close> by blast
+qed
+
+proposition covering_space_open_map:
+  fixes s :: "'a :: metric_space set" and t :: "'b :: metric_space set"
+  assumes p: "covering_space c p s" and t: "openin (subtopology euclidean c) t"
+    shows "openin (subtopology euclidean s) (p ` t)"
+proof -
+  have pce: "p ` c = s"
+   and covs:
+       "\<And>x. x \<in> s \<Longrightarrow>
+            \<exists>X VS. x \<in> X \<and> openin (subtopology euclidean s) X \<and>
+                  \<Union>VS = {x. x \<in> c \<and> p x \<in> X} \<and>
+                  (\<forall>u \<in> VS. openin (subtopology euclidean c) u) \<and>
+                  pairwise disjnt VS \<and>
+                  (\<forall>u \<in> VS. \<exists>q. homeomorphism u X p q)"
+    using p by (auto simp: covering_space_def)
+  have "t \<subseteq> c"  by (metis openin_euclidean_subtopology_iff t)
+  have "\<exists>T. openin (subtopology euclidean s) T \<and> y \<in> T \<and> T \<subseteq> p ` t"
+          if "y \<in> p ` t" for y
+  proof -
+    have "y \<in> s" using \<open>t \<subseteq> c\<close> pce that by blast
+    obtain U VS where "y \<in> U" and U: "openin (subtopology euclidean s) U"
+                  and VS: "\<Union>VS = {x. x \<in> c \<and> p x \<in> U}"
+                  and openVS: "\<forall>V \<in> VS. openin (subtopology euclidean c) V"
+                  and homVS: "\<And>V. V \<in> VS \<Longrightarrow> \<exists>q. homeomorphism V U p q"
+      using covs [OF \<open>y \<in> s\<close>] by auto
+    obtain x where "x \<in> c" "p x \<in> U" "x \<in> t" "p x = y"
+      apply simp
+      using t [unfolded openin_euclidean_subtopology_iff] \<open>y \<in> U\<close> \<open>y \<in> p ` t\<close> by blast
+    with VS obtain V where "x \<in> V" "V \<in> VS" by auto
+    then obtain q where q: "homeomorphism V U p q" using homVS by blast
+    then have ptV: "p ` (t \<inter> V) = U \<inter> {z. q z \<in> (t \<inter> V)}"
+      using VS \<open>V \<in> VS\<close> by (auto simp: homeomorphism_def)
+    have ocv: "openin (subtopology euclidean c) V"
+      by (simp add: \<open>V \<in> VS\<close> openVS)
+    have "openin (subtopology euclidean U) {z \<in> U. q z \<in> t \<inter> V}"
+      apply (rule continuous_on_open [THEN iffD1, rule_format])
+       using homeomorphism_def q apply blast
+      using openin_subtopology_Int_subset [of c] q t unfolding homeomorphism_def
+      by (metis inf.absorb_iff2 Int_commute ocv openin_euclidean_subtopology_iff)
+    then have os: "openin (subtopology euclidean s) (U \<inter> {z. q z \<in> t \<inter> V})"
+      using openin_trans [of U] by (simp add: Collect_conj_eq U)
+    show ?thesis
+      apply (rule_tac x = "p ` (t \<inter> V)" in exI)
+      apply (rule conjI)
+      apply (simp only: ptV os)
+      using \<open>p x = y\<close> \<open>x \<in> V\<close> \<open>x \<in> t\<close> apply blast
+      done
+  qed
+  with openin_subopen show ?thesis by blast
+qed
+
+lemma covering_space_lift_unique_gen:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
+  fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
+  assumes cov: "covering_space c p s"
+      and eq: "g1 a = g2 a"
+      and f: "continuous_on t f"  "f ` t \<subseteq> s"
+      and g1: "continuous_on t g1"  "g1 ` t \<subseteq> c"
+      and fg1: "\<And>x. x \<in> t \<Longrightarrow> f x = p(g1 x)"
+      and g2: "continuous_on t g2"  "g2 ` t \<subseteq> c"
+      and fg2: "\<And>x. x \<in> t \<Longrightarrow> f x = p(g2 x)"
+      and u_compt: "u \<in> components t" and "a \<in> u" "x \<in> u"
+    shows "g1 x = g2 x"
+proof -
+  have "u \<subseteq> t" by (rule in_components_subset [OF u_compt])
+  def G12 \<equiv> "{x \<in> u. g1 x - g2 x = 0}"
+  have "connected u" by (rule in_components_connected [OF u_compt])
+  have contu: "continuous_on u g1" "continuous_on u g2"
+       using \<open>u \<subseteq> t\<close> continuous_on_subset g1 g2 by blast+
+  have o12: "openin (subtopology euclidean u) G12"
+  unfolding G12_def
+  proof (subst openin_subopen, clarify)
+    fix z
+    assume z: "z \<in> u" "g1 z - g2 z = 0"
+    obtain v w q where "g1 z \<in> v" and ocv: "openin (subtopology euclidean c) v"
+                   and "p (g1 z) \<in> w" and osw: "openin (subtopology euclidean s) w"
+                   and hom: "homeomorphism v w p q"
+      apply (rule_tac x = "g1 z" in covering_space_local_homeomorphism [OF cov])
+       using \<open>u \<subseteq> t\<close> \<open>z \<in> u\<close> g1(2) apply blast+
+      done
+    have "g2 z \<in> v" using \<open>g1 z \<in> v\<close> z by auto
+    have gg: "{x \<in> u. g x \<in> v} = {x \<in> u. g x \<in> (v \<inter> g ` u)}" for g
+      by auto
+    have "openin (subtopology euclidean (g1 ` u)) (v \<inter> g1 ` u)"
+      using ocv \<open>u \<subseteq> t\<close> g1 by (fastforce simp add: openin_open)
+    then have 1: "openin (subtopology euclidean u) {x \<in> u. g1 x \<in> v}"
+      unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
+    have "openin (subtopology euclidean (g2 ` u)) (v \<inter> g2 ` u)"
+      using ocv \<open>u \<subseteq> t\<close> g2 by (fastforce simp add: openin_open)
+    then have 2: "openin (subtopology euclidean u) {x \<in> u. g2 x \<in> v}"
+      unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
+    show "\<exists>T. openin (subtopology euclidean u) T \<and>
+              z \<in> T \<and> T \<subseteq> {z \<in> u. g1 z - g2 z = 0}"
+      using z
+      apply (rule_tac x = "{x. x \<in> u \<and> g1 x \<in> v} \<inter> {x. x \<in> u \<and> g2 x \<in> v}" in exI)
+      apply (intro conjI)
+      apply (rule openin_Int [OF 1 2])
+      using \<open>g1 z \<in> v\<close>  \<open>g2 z \<in> v\<close>  apply (force simp:, clarify)
+      apply (metis \<open>u \<subseteq> t\<close> subsetD eq_iff_diff_eq_0 fg1 fg2 hom homeomorphism_def)
+      done
+  qed
+  have c12: "closedin (subtopology euclidean u) G12"
+    unfolding G12_def
+    by (intro continuous_intros continuous_closedin_preimage_constant contu)
+  have "G12 = {} \<or> G12 = u"
+    by (intro connected_clopen [THEN iffD1, rule_format] \<open>connected u\<close> conjI o12 c12)
+  with eq \<open>a \<in> u\<close> have "\<And>x. x \<in> u \<Longrightarrow> g1 x - g2 x = 0" by (auto simp: G12_def)
+  then show ?thesis
+    using \<open>x \<in> u\<close> by force
+qed
+
+proposition covering_space_lift_unique:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
+  fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
+  assumes "covering_space c p s"
+          "g1 a = g2 a"
+          "continuous_on t f"  "f ` t \<subseteq> s"
+          "continuous_on t g1"  "g1 ` t \<subseteq> c"  "\<And>x. x \<in> t \<Longrightarrow> f x = p(g1 x)"
+          "continuous_on t g2"  "g2 ` t \<subseteq> c"  "\<And>x. x \<in> t \<Longrightarrow> f x = p(g2 x)"
+          "connected t"  "a \<in> t"   "x \<in> t"
+   shows "g1 x = g2 x"
+using covering_space_lift_unique_gen [of c p s] in_components_self assms ex_in_conv by blast
+
 end
diff -r ce995deef4b0 -r d3c87eb0bad2 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Jun 14 15:34:21 2016 +0100
@@ -11,6 +11,173 @@
   "~~/src/HOL/Library/Indicator_Function"
 begin
 
+(*FIXME: move elsewhere and use the existing locales*)
+
+subsection \<open>Using additivity of lifted function to encode definedness.\<close>
+
+definition "neutral opp = (SOME x. \<forall>y. opp x y = y \<and> opp y x = y)"
+
+fun lifted where
+  "lifted (opp :: 'a \<Rightarrow> 'a \<Rightarrow> 'b) (Some x) (Some y) = Some (opp x y)"
+| "lifted opp None _ = (None::'b option)"
+| "lifted opp _ None = None"
+
+lemma lifted_simp_1[simp]: "lifted opp v None = None"
+  by (induct v) auto
+
+definition "monoidal opp \<longleftrightarrow>
+  (\<forall>x y. opp x y = opp y x) \<and>
+  (\<forall>x y z. opp x (opp y z) = opp (opp x y) z) \<and>
+  (\<forall>x. opp (neutral opp) x = x)"
+
+lemma monoidalI:
+  assumes "\<And>x y. opp x y = opp y x"
+    and "\<And>x y z. opp x (opp y z) = opp (opp x y) z"
+    and "\<And>x. opp (neutral opp) x = x"
+  shows "monoidal opp"
+  unfolding monoidal_def using assms by fastforce
+
+lemma monoidal_ac:
+  assumes "monoidal opp"
+  shows [simp]: "opp (neutral opp) a = a"
+    and [simp]: "opp a (neutral opp) = a"
+    and "opp a b = opp b a"
+    and "opp (opp a b) c = opp a (opp b c)"
+    and "opp a (opp b c) = opp b (opp a c)"
+  using assms unfolding monoidal_def by metis+
+
+lemma neutral_lifted [cong]:
+  assumes "monoidal opp"
+  shows "neutral (lifted opp) = Some (neutral opp)"
+proof -
+  { fix x
+    assume "\<forall>y. lifted opp x y = y \<and> lifted opp y x = y"
+    then have "Some (neutral opp) = x"
+      apply (induct x)
+      apply force
+      by (metis assms lifted.simps(1) monoidal_ac(2) option.inject) }
+  note [simp] = this
+  show ?thesis
+    apply (subst neutral_def)
+    apply (intro some_equality allI)
+    apply (induct_tac y)
+    apply (auto simp add:monoidal_ac[OF assms])
+    done
+qed
+
+lemma monoidal_lifted[intro]:
+  assumes "monoidal opp"
+  shows "monoidal (lifted opp)"
+  unfolding monoidal_def split_option_all neutral_lifted[OF assms]
+  using monoidal_ac[OF assms]
+  by auto
+
+definition "support opp f s = {x. x\<in>s \<and> f x \<noteq> neutral opp}"
+definition "fold' opp e s = (if finite s then Finite_Set.fold opp e s else e)"
+definition "iterate opp s f = fold' (\<lambda>x a. opp (f x) a) (neutral opp) (support opp f s)"
+
+lemma support_subset[intro]: "support opp f s \<subseteq> s"
+  unfolding support_def by auto
+
+lemma support_empty[simp]: "support opp f {} = {}"
+  using support_subset[of opp f "{}"] by auto
+
+lemma comp_fun_commute_monoidal[intro]:
+  assumes "monoidal opp"
+  shows "comp_fun_commute opp"
+  unfolding comp_fun_commute_def
+  using monoidal_ac[OF assms]
+  by auto
+
+lemma support_clauses:
+  "\<And>f g s. support opp f {} = {}"
+  "\<And>f g s. support opp f (insert x s) =
+    (if f(x) = neutral opp then support opp f s else insert x (support opp f s))"
+  "\<And>f g s. support opp f (s - {x}) = (support opp f s) - {x}"
+  "\<And>f g s. support opp f (s \<union> t) = (support opp f s) \<union> (support opp f t)"
+  "\<And>f g s. support opp f (s \<inter> t) = (support opp f s) \<inter> (support opp f t)"
+  "\<And>f g s. support opp f (s - t) = (support opp f s) - (support opp f t)"
+  "\<And>f g s. support opp g (f ` s) = f ` (support opp (g \<circ> f) s)"
+  unfolding support_def by auto
+
+lemma finite_support[intro]: "finite s \<Longrightarrow> finite (support opp f s)"
+  unfolding support_def by auto
+
+lemma iterate_empty[simp]: "iterate opp {} f = neutral opp"
+  unfolding iterate_def fold'_def by auto
+
+lemma iterate_insert[simp]:
+  assumes "monoidal opp"
+    and "finite s"
+  shows "iterate opp (insert x s) f =
+         (if x \<in> s then iterate opp s f else opp (f x) (iterate opp s f))"
+proof (cases "x \<in> s")
+  case True
+  then show ?thesis by (auto simp: insert_absorb iterate_def)
+next
+  case False
+  note * = comp_fun_commute.comp_comp_fun_commute [OF comp_fun_commute_monoidal[OF assms(1)]]
+  show ?thesis
+  proof (cases "f x = neutral opp")
+    case True
+    then show ?thesis
+      using assms \<open>x \<notin> s\<close>
+      by (auto simp: iterate_def support_clauses)
+  next
+    case False
+    with \<open>x \<notin> s\<close> \<open>finite s\<close> support_subset show ?thesis
+      apply (simp add: iterate_def fold'_def support_clauses)
+      apply (subst comp_fun_commute.fold_insert[OF * finite_support, simplified comp_def])
+      apply (force simp add: )+
+      done
+  qed
+qed
+
+lemma iterate_some:
+    "\<lbrakk>monoidal opp; finite s\<rbrakk> \<Longrightarrow> iterate (lifted opp) s (\<lambda>x. Some(f x)) = Some (iterate opp s f)"
+  by (erule finite_induct) (auto simp: monoidal_lifted)
+
+lemma neutral_add[simp]: "neutral op + = (0::'a::comm_monoid_add)"
+  unfolding neutral_def
+  by (force elim: allE [where x=0])
+
+lemma support_if: "a \<noteq> neutral opp \<Longrightarrow> support opp (\<lambda>x. if P x then a else neutral opp) A = {x \<in> A. P x}"
+unfolding support_def
+by (force intro: Collect_cong)
+
+lemma support_if_subset: "support opp (\<lambda>x. if P x then a else neutral opp) A \<subseteq> {x \<in> A. P x}"
+by (simp add: subset_iff support_def)
+
+definition supp_setsum where "supp_setsum f A \<equiv> setsum f (support op+ f A)"
+
+lemma supp_setsum_divide_distrib:
+    "supp_setsum f A / (r::'a::field) = supp_setsum (\<lambda>n. f n / r) A"
+apply (cases "r = 0")
+apply (simp add: supp_setsum_def)
+apply (simp add: supp_setsum_def setsum_divide_distrib support_def)
+done
+
+(*FIXME move up e.g. to Library/Convex.thy*)
+lemma convex_supp_setsum:
+  assumes "convex S" and 1: "supp_setsum u I = 1"
+      and "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> u i \<and> (u i = 0 \<or> f i \<in> S)"
+    shows "supp_setsum (\<lambda>i. u i *\<^sub>R f i) I \<in> S"
+proof -
+  have fin: "finite {i \<in> I. u i \<noteq> 0}"
+    using 1 setsum.infinite by (force simp: supp_setsum_def support_def)
+  then have eq: "supp_setsum(\<lambda>i. u i *\<^sub>R f i) I =
+            setsum (\<lambda>i. u i *\<^sub>R f i) {i \<in> I. u i \<noteq> 0}"
+    by (force intro: setsum.mono_neutral_left simp: supp_setsum_def support_def)
+  show ?thesis
+    apply (simp add: eq)
+    apply (rule convex_setsum [OF fin \<open>convex S\<close>])
+    using 1 assms apply (auto simp: supp_setsum_def support_def)
+    done
+qed
+
+(*END OF SUPPORT, ETC.*)
+
+
 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
   scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
   scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
@@ -3565,8 +3732,6 @@
 
 subsection \<open>Generalized notion of additivity.\<close>
 
-definition "neutral opp = (SOME x. \<forall>y. opp x y = y \<and> opp y x = y)"
-
 definition operative :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (('b::euclidean_space) set \<Rightarrow> 'a) \<Rightarrow> bool"
   where "operative opp f \<longleftrightarrow>
     (\<forall>a b. content (cbox a b) = 0 \<longrightarrow> f (cbox a b) = neutral opp) \<and>
@@ -3587,135 +3752,8 @@
   unfolding operative_def by (rule property_empty_interval) auto
 
 
-subsection \<open>Using additivity of lifted function to encode definedness.\<close>
-
-fun lifted where
-  "lifted (opp :: 'a \<Rightarrow> 'a \<Rightarrow> 'b) (Some x) (Some y) = Some (opp x y)"
-| "lifted opp None _ = (None::'b option)"
-| "lifted opp _ None = None"
-
-lemma lifted_simp_1[simp]: "lifted opp v None = None"
-  by (induct v) auto
-
-definition "monoidal opp \<longleftrightarrow>
-  (\<forall>x y. opp x y = opp y x) \<and>
-  (\<forall>x y z. opp x (opp y z) = opp (opp x y) z) \<and>
-  (\<forall>x. opp (neutral opp) x = x)"
-
-lemma monoidalI:
-  assumes "\<And>x y. opp x y = opp y x"
-    and "\<And>x y z. opp x (opp y z) = opp (opp x y) z"
-    and "\<And>x. opp (neutral opp) x = x"
-  shows "monoidal opp"
-  unfolding monoidal_def using assms by fastforce
-
-lemma monoidal_ac:
-  assumes "monoidal opp"
-  shows [simp]: "opp (neutral opp) a = a"
-    and [simp]: "opp a (neutral opp) = a"
-    and "opp a b = opp b a"
-    and "opp (opp a b) c = opp a (opp b c)"
-    and "opp a (opp b c) = opp b (opp a c)"
-  using assms unfolding monoidal_def by metis+
-
-lemma neutral_lifted [cong]:
-  assumes "monoidal opp"
-  shows "neutral (lifted opp) = Some (neutral opp)"
-proof -
-  { fix x
-    assume "\<forall>y. lifted opp x y = y \<and> lifted opp y x = y"
-    then have "Some (neutral opp) = x"
-      apply (induct x)
-      apply force
-      by (metis assms lifted.simps(1) monoidal_ac(2) option.inject) }
-  note [simp] = this
-  show ?thesis
-    apply (subst neutral_def)
-    apply (intro some_equality allI)
-    apply (induct_tac y)
-    apply (auto simp add:monoidal_ac[OF assms])
-    done
-qed
-
-lemma monoidal_lifted[intro]:
-  assumes "monoidal opp"
-  shows "monoidal (lifted opp)"
-  unfolding monoidal_def split_option_all neutral_lifted[OF assms]
-  using monoidal_ac[OF assms]
-  by auto
-
-definition "support opp f s = {x. x\<in>s \<and> f x \<noteq> neutral opp}"
-definition "fold' opp e s = (if finite s then Finite_Set.fold opp e s else e)"
-definition "iterate opp s f = fold' (\<lambda>x a. opp (f x) a) (neutral opp) (support opp f s)"
-
-lemma support_subset[intro]: "support opp f s \<subseteq> s"
-  unfolding support_def by auto
-
-lemma support_empty[simp]: "support opp f {} = {}"
-  using support_subset[of opp f "{}"] by auto
-
-lemma comp_fun_commute_monoidal[intro]:
-  assumes "monoidal opp"
-  shows "comp_fun_commute opp"
-  unfolding comp_fun_commute_def
-  using monoidal_ac[OF assms]
-  by auto
-
-lemma support_clauses:
-  "\<And>f g s. support opp f {} = {}"
-  "\<And>f g s. support opp f (insert x s) =
-    (if f(x) = neutral opp then support opp f s else insert x (support opp f s))"
-  "\<And>f g s. support opp f (s - {x}) = (support opp f s) - {x}"
-  "\<And>f g s. support opp f (s \<union> t) = (support opp f s) \<union> (support opp f t)"
-  "\<And>f g s. support opp f (s \<inter> t) = (support opp f s) \<inter> (support opp f t)"
-  "\<And>f g s. support opp f (s - t) = (support opp f s) - (support opp f t)"
-  "\<And>f g s. support opp g (f ` s) = f ` (support opp (g \<circ> f) s)"
-  unfolding support_def by auto
-
-lemma finite_support[intro]: "finite s \<Longrightarrow> finite (support opp f s)"
-  unfolding support_def by auto
-
-lemma iterate_empty[simp]: "iterate opp {} f = neutral opp"
-  unfolding iterate_def fold'_def by auto
-
-lemma iterate_insert[simp]:
-  assumes "monoidal opp"
-    and "finite s"
-  shows "iterate opp (insert x s) f =
-         (if x \<in> s then iterate opp s f else opp (f x) (iterate opp s f))"
-proof (cases "x \<in> s")
-  case True
-  then show ?thesis by (auto simp: insert_absorb iterate_def)
-next
-  case False
-  note * = comp_fun_commute.comp_comp_fun_commute [OF comp_fun_commute_monoidal[OF assms(1)]]
-  show ?thesis
-  proof (cases "f x = neutral opp")
-    case True
-    then show ?thesis
-      using assms \<open>x \<notin> s\<close>
-      by (auto simp: iterate_def support_clauses)
-  next
-    case False
-    with \<open>x \<notin> s\<close> \<open>finite s\<close> support_subset show ?thesis
-      apply (simp add: iterate_def fold'_def support_clauses)
-      apply (subst comp_fun_commute.fold_insert[OF * finite_support, simplified comp_def])
-      apply (force simp add: )+
-      done
-  qed
-qed
-
-lemma iterate_some:
-    "\<lbrakk>monoidal opp; finite s\<rbrakk> \<Longrightarrow> iterate (lifted opp) s (\<lambda>x. Some(f x)) = Some (iterate opp s f)"
-  by (erule finite_induct) (auto simp: monoidal_lifted)
-
-
 subsection \<open>Two key instances of additivity.\<close>
 
-lemma neutral_add[simp]: "neutral op + = (0::'a::comm_monoid_add)"
-  unfolding neutral_def
-  by (force elim: allE [where x=0])
-
 lemma operative_content[intro]: "operative (op +) content"
   by (force simp add: operative_def content_split[symmetric])
 
diff -r ce995deef4b0 -r d3c87eb0bad2 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Tue Jun 14 15:34:21 2016 +0100
@@ -1433,8 +1433,8 @@
   ultimately show False
     using *[unfolded connected_local not_ex, rule_format,
       of "{x\<in>{0..1}. g x \<in> e1}" "{x\<in>{0..1}. g x \<in> e2}"]
-    using continuous_openin_preimage[OF g(1)[unfolded path_def] as(1)]
-    using continuous_openin_preimage[OF g(1)[unfolded path_def] as(2)]
+    using continuous_openin_preimage_gen[OF g(1)[unfolded path_def] as(1)]
+    using continuous_openin_preimage_gen[OF g(1)[unfolded path_def] as(2)]
     by auto
 qed
 
@@ -4605,6 +4605,24 @@
 using eq homeomorphism_sym homeomorphism_symD [OF hom] apply blast+
 done
 
+lemma homeomorphic_locally:
+  fixes S:: "'a::metric_space set" and T:: "'b::metric_space set"
+  assumes hom: "S homeomorphic T"
+          and iff: "\<And>X Y. X homeomorphic Y \<Longrightarrow> (P X \<longleftrightarrow> Q Y)"
+    shows "locally P S \<longleftrightarrow> locally Q T"
+proof -
+  obtain f g where hom: "homeomorphism S T f g"
+    using assms by (force simp: homeomorphic_def)
+  then show ?thesis
+    using homeomorphic_def local.iff
+    by (blast intro!: homeomorphism_locally)
+qed
+
+lemma homeomorphic_local_compactness:
+  fixes S:: "'a::metric_space set" and T:: "'b::metric_space set"
+  shows "S homeomorphic T \<Longrightarrow> locally compact S \<longleftrightarrow> locally compact T"
+by (simp add: homeomorphic_compactness homeomorphic_locally)
+
 lemma locally_translation:
   fixes P :: "'a :: real_normed_vector set \<Rightarrow> bool"
   shows
@@ -4651,6 +4669,107 @@
     done
 qed
 
+subsection\<open>Sort of induction principle for connected sets\<close>
+
+lemma connected_induction:
+  assumes "connected S"
+      and opD: "\<And>T a. \<lbrakk>openin (subtopology euclidean S) T; a \<in> T\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> T \<and> P z"
+      and opI: "\<And>a. a \<in> S
+             \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and>
+                     (\<forall>x \<in> T. \<forall>y \<in> T. P x \<and> P y \<and> Q x \<longrightarrow> Q y)"
+      and etc: "a \<in> S" "b \<in> S" "P a" "P b" "Q a"
+    shows "Q b"
+proof -
+  have 1: "openin (subtopology euclidean S)
+             {b. \<exists>T. openin (subtopology euclidean S) T \<and>
+                     b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> Q x)}"
+    apply (subst openin_subopen, clarify)
+    apply (rule_tac x=T in exI, auto)
+    done
+  have 2: "openin (subtopology euclidean S)
+             {b. \<exists>T. openin (subtopology euclidean S) T \<and>
+                     b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> ~ Q x)}"
+    apply (subst openin_subopen, clarify)
+    apply (rule_tac x=T in exI, auto)
+    done
+  show ?thesis
+    using \<open>connected S\<close>
+    apply (simp only: connected_openin HOL.not_ex HOL.de_Morgan_conj)
+    apply (elim disjE allE)
+         apply (blast intro: 1)
+        apply (blast intro: 2, simp_all)
+       apply clarify apply (metis opI)
+      using opD apply (blast intro: etc elim: dest:)
+     using opI etc apply meson+
+    done
+qed
+
+lemma connected_equivalence_relation_gen:
+  assumes "connected S"
+      and etc: "a \<in> S" "b \<in> S" "P a" "P b"
+      and trans: "\<And>x y z. \<lbrakk>R x y; R y z\<rbrakk> \<Longrightarrow> R x z"
+      and opD: "\<And>T a. \<lbrakk>openin (subtopology euclidean S) T; a \<in> T\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> T \<and> P z"
+      and opI: "\<And>a. a \<in> S
+             \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and>
+                     (\<forall>x \<in> T. \<forall>y \<in> T. P x \<and> P y \<longrightarrow> R x y)"
+    shows "R a b"
+proof -
+  have "\<And>a b c. \<lbrakk>a \<in> S; P a; b \<in> S; c \<in> S; P b; P c; R a b\<rbrakk> \<Longrightarrow> R a c"
+    apply (rule connected_induction [OF \<open>connected S\<close> opD], simp_all)
+    by (meson trans opI)
+  then show ?thesis by (metis etc opI)
+qed
+
+lemma connected_induction_simple:
+  assumes "connected S"
+      and etc: "a \<in> S" "b \<in> S" "P a"
+      and opI: "\<And>a. a \<in> S
+             \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and>
+                     (\<forall>x \<in> T. \<forall>y \<in> T. P x \<longrightarrow> P y)"
+    shows "P b"
+apply (rule connected_induction [OF \<open>connected S\<close> _, where P = "\<lambda>x. True"], blast)
+apply (frule opI)
+using etc apply simp_all
+done
+
+lemma connected_equivalence_relation:
+  assumes "connected S"
+      and etc: "a \<in> S" "b \<in> S"
+      and sym: "\<And>x y z. R x y \<Longrightarrow> R y x"
+      and trans: "\<And>x y z. R x y \<and> R y z \<Longrightarrow> R x z"
+      and opI: "\<And>a. a \<in> S
+             \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and> (\<forall>x \<in> T. R a x)"
+    shows "R a b"
+proof -
+  have "\<And>a b c. \<lbrakk>a \<in> S; b \<in> S; c \<in> S; R a b\<rbrakk> \<Longrightarrow> R a c"
+    apply (rule connected_induction_simple [OF \<open>connected S\<close>], simp_all)
+    by (meson local.sym local.trans opI)
+  then show ?thesis by (metis etc opI)
+qed
+
+
+lemma locally_constant_imp_constant:
+  assumes "connected S"
+      and opI: "\<And>a. a \<in> S
+             \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and> (\<forall>x \<in> T. f x = f a)"
+    shows "f constant_on S"
+proof -
+  have "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> f x = f y"
+    apply (rule connected_equivalence_relation [OF \<open>connected S\<close>], simp_all)
+    by (metis opI)
+  then show ?thesis
+    by (metis constant_on_def)
+qed
+
+lemma locally_constant:
+     "connected S \<Longrightarrow> locally (\<lambda>U. f constant_on U) S \<longleftrightarrow> f constant_on S"
+apply (simp add: locally_def)
+apply (rule iffI)
+ apply (rule locally_constant_imp_constant, assumption)
+ apply (metis (mono_tags, hide_lams) constant_on_def constant_on_subset openin_subtopology_self)
+by (meson constant_on_subset openin_imp_subset order_refl)
+
+
 subsection\<open>Basic properties of local compactness\<close>
 
 lemma locally_compact:
@@ -5145,7 +5264,7 @@
 lemma continuous_openin_preimage_eq:
    "continuous_on S f \<longleftrightarrow>
     (\<forall>t. open t \<longrightarrow> openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
-apply (auto simp: continuous_openin_preimage)
+apply (auto simp: continuous_openin_preimage_gen)
 apply (fastforce simp add: continuous_on_open openin_open)
 done
 
@@ -5171,7 +5290,7 @@
     using Union_components by blast
   then show "openin (subtopology euclidean S) {x \<in> S. f x \<in> t}"
     using \<open>open t\<close> assms
-    by (fastforce intro: openin_trans continuous_openin_preimage)
+    by (fastforce intro: openin_trans continuous_openin_preimage_gen)
 qed
 
 lemma continuous_on_components:
diff -r ce995deef4b0 -r d3c87eb0bad2 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Jun 14 15:34:21 2016 +0100
@@ -1906,12 +1906,12 @@
 lemma islimpt_in_closure: "(x islimpt S) = (x:closure(S-{x}))"
   unfolding closure_def using islimpt_punctured by blast
 
-lemma connected_imp_connected_closure: "connected s \<Longrightarrow> connected (closure s)"
+lemma connected_imp_connected_closure: "connected S \<Longrightarrow> connected (closure S)"
     by (rule connectedI) (meson closure_subset open_Int open_Int_closure_eq_empty subset_trans connectedD)
 
 lemma limpt_of_limpts:
       fixes x :: "'a::metric_space"
-      shows "x islimpt {y. y islimpt s} \<Longrightarrow> x islimpt s"
+      shows "x islimpt {y. y islimpt S} \<Longrightarrow> x islimpt S"
   apply (clarsimp simp add: islimpt_approachable)
   apply (drule_tac x="e/2" in spec)
   apply (auto simp: simp del: less_divide_eq_numeral1)
@@ -1920,27 +1920,37 @@
   apply (erule rev_bexI)
   by (metis dist_commute dist_triangle_half_r less_trans less_irrefl)
 
-lemma closed_limpts:  "closed {x::'a::metric_space. x islimpt s}"
+lemma closed_limpts:  "closed {x::'a::metric_space. x islimpt S}"
   using closed_limpt limpt_of_limpts by blast
 
 lemma limpt_of_closure:
       fixes x :: "'a::metric_space"
-      shows "x islimpt closure s \<longleftrightarrow> x islimpt s"
+      shows "x islimpt closure S \<longleftrightarrow> x islimpt S"
   by (auto simp: closure_def islimpt_Un dest: limpt_of_limpts)
 
 lemma closedin_limpt:
-   "closedin (subtopology euclidean t) s \<longleftrightarrow> s \<subseteq> t \<and> (\<forall>x. x islimpt s \<and> x \<in> t \<longrightarrow> x \<in> s)"
+   "closedin (subtopology euclidean T) S \<longleftrightarrow> S \<subseteq> T \<and> (\<forall>x. x islimpt S \<and> x \<in> T \<longrightarrow> x \<in> S)"
   apply (simp add: closedin_closed, safe)
   apply (simp add: closed_limpt islimpt_subset)
-  apply (rule_tac x="closure s" in exI)
+  apply (rule_tac x="closure S" in exI)
   apply simp
   apply (force simp: closure_def)
   done
 
 lemma closedin_closed_eq:
-    "closed s \<Longrightarrow> (closedin (subtopology euclidean s) t \<longleftrightarrow> closed t \<and> t \<subseteq> s)"
+    "closed S \<Longrightarrow> (closedin (subtopology euclidean S) T \<longleftrightarrow> closed T \<and> T \<subseteq> S)"
   by (meson closedin_limpt closed_subset closedin_closed_trans)
 
+lemma closedin_subset_trans:
+   "\<lbrakk>closedin (subtopology euclidean U) S; S \<subseteq> T; T \<subseteq> U\<rbrakk>
+    \<Longrightarrow> closedin (subtopology euclidean T) S"
+by (meson closedin_limpt subset_iff)
+
+lemma closedin_Times:
+   "\<lbrakk>closedin (subtopology euclidean S) S'; closedin (subtopology euclidean T) T'\<rbrakk>
+    \<Longrightarrow> closedin (subtopology euclidean (S \<times> T)) (S' \<times> T')"
+unfolding closedin_closed using closed_Times by blast
+
 lemma bdd_below_closure:
   fixes A :: "real set"
   assumes "bdd_below A"
@@ -2438,14 +2448,13 @@
   by (rule topological_tendstoI, auto elim: eventually_mono)
 
 lemma Lim_transform_within_set:
-  fixes a l :: "'a::real_normed_vector"
-  shows "\<lbrakk>(f \<longlongrightarrow> l) (at a within s); eventually (\<lambda>x. x \<in> s \<longleftrightarrow> x \<in> t) (at a)\<rbrakk>
-         \<Longrightarrow> (f \<longlongrightarrow> l) (at a within t)"
+  fixes a :: "'a::metric_space" and l :: "'b::metric_space"
+  shows "\<lbrakk>(f \<longlongrightarrow> l) (at a within S); eventually (\<lambda>x. x \<in> S \<longleftrightarrow> x \<in> T) (at a)\<rbrakk>
+         \<Longrightarrow> (f \<longlongrightarrow> l) (at a within T)"
 apply (clarsimp simp: eventually_at Lim_within)
 apply (drule_tac x=e in spec, clarify)
 apply (rename_tac k)
-apply (rule_tac x="min d k" in exI)
-apply (simp add:)
+apply (rule_tac x="min d k" in exI, simp)
 done
 
 lemma Lim_transform_within_set_eq:
@@ -2454,6 +2463,31 @@
          \<Longrightarrow> ((f \<longlongrightarrow> l) (at a within s) \<longleftrightarrow> (f \<longlongrightarrow> l) (at a within t))"
 by (force intro: Lim_transform_within_set elim: eventually_mono)
 
+lemma Lim_transform_within_openin:
+  fixes a :: "'a::metric_space"
+  assumes f: "(f \<longlongrightarrow> l) (at a within T)"
+      and "openin (subtopology euclidean T) S" "a \<in> S"
+      and eq: "\<And>x. \<lbrakk>x \<in> S; x \<noteq> a\<rbrakk> \<Longrightarrow> f x = g x"
+  shows "(g \<longlongrightarrow> l) (at a within T)"
+proof -
+  obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "ball a \<epsilon> \<inter> T \<subseteq> S"
+    using assms by (force simp: openin_contains_ball)
+  then have "a \<in> ball a \<epsilon>"
+    by force
+  show ?thesis
+    apply (rule Lim_transform_within [OF f \<open>0 < \<epsilon>\<close> eq])
+    using \<epsilon> apply (auto simp: dist_commute subset_iff)
+    done
+qed
+
+lemma continuous_transform_within_openin:
+  fixes a :: "'a::metric_space"
+  assumes "continuous (at a within T) f"
+      and "openin (subtopology euclidean T) S" "a \<in> S"
+      and eq: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
+  shows "continuous (at a within T) g"
+using assms by (simp add: Lim_transform_within_openin continuous_within)
+
 text\<open>The expected monotonicity property.\<close>
 
 lemma Lim_Un:
@@ -2544,6 +2578,72 @@
 
 text\<open>Another limit point characterization.\<close>
 
+lemma limpt_sequential_inj:
+  fixes x :: "'a::metric_space"
+  shows "x islimpt S \<longleftrightarrow>
+         (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> inj f \<and> (f \<longlongrightarrow> x) sequentially)"
+         (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then have "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e"
+    by (force simp: islimpt_approachable)
+  then obtain y where y: "\<And>e. e>0 \<Longrightarrow> y e \<in> S \<and> y e \<noteq> x \<and> dist (y e) x < e"
+    by metis
+  define f where "f \<equiv> rec_nat (y 1) (\<lambda>n fn. y (min (inverse(2 ^ (Suc n))) (dist fn x)))"
+  have [simp]: "f 0 = y 1"
+               "f(Suc n) = y (min (inverse(2 ^ (Suc n))) (dist (f n) x))" for n
+    by (simp_all add: f_def)
+  have f: "f n \<in> S \<and> (f n \<noteq> x) \<and> dist (f n) x < inverse(2 ^ n)" for n
+  proof (induction n)
+    case 0 show ?case
+      by (simp add: y)
+  next
+    case (Suc n) then show ?case
+      apply (auto simp: y)
+      by (metis half_gt_zero_iff inverse_positive_iff_positive less_divide_eq_numeral1(1) min_less_iff_conj y zero_less_dist_iff zero_less_numeral zero_less_power)
+  qed
+  show ?rhs
+  proof (rule_tac x=f in exI, intro conjI allI)
+    show "\<And>n. f n \<in> S - {x}"
+      using f by blast
+    have "dist (f n) x < dist (f m) x" if "m < n" for m n
+    using that
+    proof (induction n)
+      case 0 then show ?case by simp
+    next
+      case (Suc n)
+      then consider "m < n" | "m = n" using less_Suc_eq by blast
+      then show ?case
+      proof cases
+        assume "m < n"
+        have "dist (f(Suc n)) x = dist (y (min (inverse(2 ^ (Suc n))) (dist (f n) x))) x"
+          by simp
+        also have "... < dist (f n) x"
+          by (metis dist_pos_lt f min.strict_order_iff min_less_iff_conj y)
+        also have "... < dist (f m) x"
+          using Suc.IH \<open>m < n\<close> by blast
+        finally show ?thesis .
+      next
+        assume "m = n" then show ?case
+          by simp (metis dist_pos_lt f half_gt_zero_iff inverse_positive_iff_positive min_less_iff_conj y zero_less_numeral zero_less_power)
+      qed
+    qed
+    then show "inj f"
+      by (metis less_irrefl linorder_injI)
+    show "f \<longlonglongrightarrow> x"
+      apply (rule tendstoI)
+      apply (rule_tac c="nat (ceiling(1/e))" in eventually_sequentiallyI)
+      apply (rule less_trans [OF f [THEN conjunct2, THEN conjunct2]])
+      apply (simp add: field_simps)
+      by (meson le_less_trans mult_less_cancel_left not_le of_nat_less_two_power)
+  qed
+next
+  assume ?rhs
+  then show ?lhs
+    by (fastforce simp add: islimpt_approachable lim_sequentially)
+qed
+
+(*could prove directly from islimpt_sequential_inj, but only for metric spaces*)
 lemma islimpt_sequential:
   fixes x :: "'a::first_countable_topology"
   shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> (f \<longlongrightarrow> x) sequentially)"
@@ -5822,6 +5922,36 @@
   unfolding continuous_on_open_invariant openin_open Int_def vimage_def Int_commute
   by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
 
+lemma continuous_on_open_gen:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  assumes "f ` S \<subseteq> T"
+    shows "continuous_on S f \<longleftrightarrow>
+             (\<forall>U. openin (subtopology euclidean T) U
+                  \<longrightarrow> openin (subtopology euclidean S) {x \<in> S. f x \<in> U})"
+     (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    apply (auto simp: openin_euclidean_subtopology_iff continuous_on_iff)
+    by (metis assms image_subset_iff)
+next
+  have ope: "openin (subtopology euclidean T) (ball y e \<inter> T)" for y e
+    by (simp add: Int_commute openin_open_Int)
+  assume ?rhs
+  then show ?lhs
+    apply (clarsimp simp add: continuous_on_iff)
+    apply (drule_tac x = "ball (f x) e \<inter> T" in spec)
+    apply (clarsimp simp add: ope openin_euclidean_subtopology_iff [of S])
+    by (metis (no_types, hide_lams) assms dist_commute dist_self image_subset_iff)
+qed
+
+lemma continuous_openin_preimage:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  shows
+   "\<lbrakk>continuous_on S f; f ` S \<subseteq> T; openin (subtopology euclidean T) U\<rbrakk>
+        \<Longrightarrow> openin (subtopology euclidean S) {x \<in> S. f x \<in> U}"
+by (simp add: continuous_on_open_gen)
+
 text \<open>Similarly in terms of closed sets.\<close>
 
 lemma continuous_on_closed:
@@ -5831,9 +5961,37 @@
   unfolding continuous_on_closed_invariant closedin_closed Int_def vimage_def Int_commute
   by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
 
+lemma continuous_on_closed_gen:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  assumes "f ` S \<subseteq> T"
+    shows "continuous_on S f \<longleftrightarrow>
+             (\<forall>U. closedin (subtopology euclidean T) U
+                  \<longrightarrow> closedin (subtopology euclidean S) {x \<in> S. f x \<in> U})"
+proof -
+  have *: "U \<subseteq> T \<Longrightarrow> {x \<in> S. f x \<in> T \<and> f x \<notin> U} = S - {x \<in> S. f x \<in> U}" for U
+    using assms by blast
+  show ?thesis
+    apply (simp add: continuous_on_open_gen [OF assms], safe)
+    apply (drule_tac [!] x="T-U" in spec)
+    apply (force simp: closedin_def *)
+    apply (force simp: openin_closedin_eq *)
+    done
+qed
+
+lemma continuous_closedin_preimage_gen:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  assumes "continuous_on S f" "f ` S \<subseteq> T" "closedin (subtopology euclidean T) U"
+    shows "closedin (subtopology euclidean S) {x \<in> S. f x \<in> U}"
+using assms continuous_on_closed_gen by blast
+
+lemma continuous_on_imp_closedin:
+  assumes "continuous_on S f" "closedin (subtopology euclidean (f ` S)) T"
+    shows "closedin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> T}"
+using assms continuous_on_closed by blast
+
 subsection \<open>Half-global and completely global cases.\<close>
 
-lemma continuous_openin_preimage:
+lemma continuous_openin_preimage_gen:
   assumes "continuous_on s f"  "open t"
   shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
 proof -
@@ -5867,7 +6025,7 @@
   shows "open {x \<in> s. f x \<in> t}"
 proof-
   obtain T where T: "open T" "{x \<in> s. f x \<in> t} = s \<inter> T"
-    using continuous_openin_preimage[OF assms(1,3)] unfolding openin_open by auto
+    using continuous_openin_preimage_gen[OF assms(1,3)] unfolding openin_open by auto
   then show ?thesis
     using open_Int[of s T, OF assms(2)] by auto
 qed
@@ -6753,7 +6911,7 @@
   proof safe
     fix y
     assume "y \<in> s"
-    from continuous_openin_preimage[OF f open_ball]
+    from continuous_openin_preimage_gen[OF f open_ball]
     obtain T where "open T" and T: "{x \<in> s. f x \<in> ball (f y) (e/2)} = T \<inter> s"
       unfolding openin_subtopology open_openin by metis
     then obtain d where "ball y d \<subseteq> T" "0 < d"
@@ -9257,12 +9415,12 @@
   assumes "open S" "finite X" "p \<in> S"
   shows "\<exists>e>0. \<forall>w\<in>ball p e. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
 proof -
-  obtain e1 where "0 < e1" and e1_b:"ball p e1 \<subseteq> S" 
+  obtain e1 where "0 < e1" and e1_b:"ball p e1 \<subseteq> S"
     using open_contains_ball_eq[OF \<open>open S\<close>] assms by auto
-  obtain e2 where "0 < e2" and "\<forall>x\<in>X. x \<noteq> p \<longrightarrow> e2 \<le> dist p x" 
+  obtain e2 where "0 < e2" and "\<forall>x\<in>X. x \<noteq> p \<longrightarrow> e2 \<le> dist p x"
     using finite_set_avoid[OF \<open>finite X\<close>,of p] by auto
   hence "\<forall>w\<in>ball p (min e1 e2). w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)" using e1_b by auto
-  thus "\<exists>e>0. \<forall>w\<in>ball p e. w \<in> S \<and> (w \<noteq> p \<longrightarrow> w \<notin> X)" using \<open>e2>0\<close> \<open>e1>0\<close> 
+  thus "\<exists>e>0. \<forall>w\<in>ball p e. w \<in> S \<and> (w \<noteq> p \<longrightarrow> w \<notin> X)" using \<open>e2>0\<close> \<open>e1>0\<close>
     apply (rule_tac x="min e1 e2" in exI)
     by auto
 qed
@@ -9272,7 +9430,7 @@
   assumes "open S" "finite X" "p \<in> S"
   shows "\<exists>e>0. \<forall>w\<in>cball p e. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
 proof -
-  obtain e1 where "e1>0" and e1: "\<forall>w\<in>ball p e1. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)" 
+  obtain e1 where "e1>0" and e1: "\<forall>w\<in>ball p e1. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
     using finite_ball_avoid[OF assms] by auto
   define e2 where "e2 \<equiv> e1/2"
   have "e2>0" and "e2 < e1" unfolding e2_def using \<open>e1>0\<close> by auto
@@ -9280,6 +9438,180 @@
   then show "\<exists>e>0. \<forall>w\<in>cball p e. w \<in> S \<and> (w \<noteq> p \<longrightarrow> w \<notin> X)" using \<open>e2>0\<close> e1 by auto
 qed
 
+subsection\<open>Various separability-type properties\<close>
+
+lemma univ_second_countable:
+  obtains \<B> :: "'a::euclidean_space 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 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 op: "\<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> op)
+    done
+qed
+
+proposition Lindelof:
+  fixes \<F> :: "'a::euclidean_space 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 \<D> G"
+    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::euclidean_space 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 \<F> tf"
+    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::euclidean_space 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 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)
+
+subsection\<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)
+
 no_notation
   eucl_less (infix "<e" 50)
 
diff -r ce995deef4b0 -r d3c87eb0bad2 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Set.thy	Tue Jun 14 15:34:21 2016 +0100
@@ -1928,6 +1928,9 @@
 
 definition disjnt where "disjnt A B \<equiv> A \<inter> B = {}"
 
+lemma disjnt_iff: "disjnt A B \<longleftrightarrow> (\<forall>x. ~ (x \<in> A \<and> x \<in> B))"
+  by (force simp: disjnt_def)
+
 lemma pairwise_empty [simp]: "pairwise P {}"
   by (simp add: pairwise_def)
 
diff -r ce995deef4b0 -r d3c87eb0bad2 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Mon Jun 13 22:42:38 2016 +0200
+++ b/src/HOL/Topological_Spaces.thy	Tue Jun 14 15:34:21 2016 +0100
@@ -146,7 +146,7 @@
   shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U)"
   using t1_space[of x y] by blast
 
-lemma closed_singleton:
+lemma closed_singleton [iff]:
   fixes a :: "'a::t1_space"
   shows "closed {a}"
 proof -
@@ -1610,6 +1610,9 @@
 lemma continuous_on_id[continuous_intros]: "continuous_on s (\<lambda>x. x)"
   unfolding continuous_on_def by fast
 
+lemma continuous_on_id'[continuous_intros]: "continuous_on s id"
+  unfolding continuous_on_def id_def by fast
+
 lemma continuous_on_const[continuous_intros]: "continuous_on s (\<lambda>x. c)"
   unfolding continuous_on_def by auto
 
@@ -1841,6 +1844,8 @@
 lemma inj_setminus: "inj_on uminus (A::'a set set)"
   by (auto simp: inj_on_def)
 
+subsection\<open> Finite intersection property\<close>
+
 lemma compact_fip:
   "compact U \<longleftrightarrow>
     (\<forall>A. (\<forall>a\<in>A. closed a) \<longrightarrow> (\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}) \<longrightarrow> U \<inter> \<Inter>A \<noteq> {})"