# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1460388462 -3600
# Node ID 7700f467892b738938f6587694371653109b29d8
# Parent  3374f3ffb2ec77daf30e6e2f7e26460232583534
lots of new theorems for multivariate analysis

diff -r 3374f3ffb2ec -r 7700f467892b src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sun Apr 10 23:15:34 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Apr 11 16:27:42 2016 +0100
@@ -19,7 +19,7 @@
 section \<open>Results connected with topological dimension.\<close>
 
 theory Brouwer_Fixpoint
-imports Convex_Euclidean_Space
+imports Path_Connected
 begin
 
 lemma bij_betw_singleton_eq:
@@ -2010,4 +2010,186 @@
     using x assms by auto
 qed
 
+subsection\<open>Retractions\<close>
+
+lemma retraction:
+   "retraction s t r \<longleftrightarrow>
+    t \<subseteq> s \<and> continuous_on s r \<and> r ` s = t \<and> (\<forall>x \<in> t. r x = x)"
+by (force simp: retraction_def)
+
+lemma retract_of_imp_extensible:
+  assumes "s retract_of t" and "continuous_on s f" and "f ` s \<subseteq> u"
+  obtains g where "continuous_on t g" "g ` t \<subseteq> u" "\<And>x. x \<in> s \<Longrightarrow> g x = f x"
+using assms
+apply (clarsimp simp add: retract_of_def retraction)
+apply (rule_tac g = "f o r" in that)
+apply (auto simp: continuous_on_compose2)
+done
+
+lemma idempotent_imp_retraction:
+  assumes "continuous_on s f" and "f ` s \<subseteq> s" and "\<And>x. x \<in> s \<Longrightarrow> f(f x) = f x"
+    shows "retraction s (f ` s) f"
+by (simp add: assms retraction)
+
+lemma retraction_subset:
+  assumes "retraction s t r" and "t \<subseteq> s'" and "s' \<subseteq> s"
+    shows "retraction s' t r"
+apply (simp add: retraction_def)
+by (metis assms continuous_on_subset image_mono retraction)
+
+lemma retract_of_subset:
+  assumes "t retract_of s" and "t \<subseteq> s'" and "s' \<subseteq> s"
+    shows "t retract_of s'"
+by (meson assms retract_of_def retraction_subset)
+
+lemma retraction_refl [simp]: "retraction s s (\<lambda>x. x)"
+by (simp add: continuous_on_id retraction)
+
+lemma retract_of_refl [iff]: "s retract_of s"
+  using continuous_on_id retract_of_def retraction_def by fastforce
+
+lemma retract_of_imp_subset:
+   "s retract_of t \<Longrightarrow> s \<subseteq> t"
+by (simp add: retract_of_def retraction_def)
+
+lemma retract_of_empty [simp]:
+     "({} retract_of s) \<longleftrightarrow> s = {}"  "(s retract_of {}) \<longleftrightarrow> s = {}"
+by (auto simp: retract_of_def retraction_def)
+
+lemma retract_of_singleton [iff]: "({x} retract_of s) \<longleftrightarrow> x \<in> s"
+  using continuous_on_const
+  by (auto simp: retract_of_def retraction_def)
+
+lemma retraction_comp:
+   "\<lbrakk>retraction s t f; retraction t u g\<rbrakk>
+        \<Longrightarrow> retraction s u (g o f)"
+apply (auto simp: retraction_def intro: continuous_on_compose2)
+by blast
+
+lemma retract_of_trans:
+  assumes "s retract_of t" and "t retract_of u"
+    shows "s retract_of u"
+using assms by (auto simp: retract_of_def intro: retraction_comp)
+
+lemma closedin_retract:
+  fixes s :: "'a :: real_normed_vector set"
+  assumes "s retract_of t"
+    shows "closedin (subtopology euclidean t) s"
+proof -
+  obtain r where "s \<subseteq> t" "continuous_on t r" "r ` t \<subseteq> s" "\<And>x. x \<in> s \<Longrightarrow> r x = x"
+    using assms by (auto simp: retract_of_def retraction_def)
+  then have s: "s = {x \<in> t. (norm(r x - x)) = 0}" by auto
+  show ?thesis
+    apply (subst s)
+    apply (rule continuous_closedin_preimage_constant)
+    by (simp add: \<open>continuous_on t r\<close> continuous_on_diff continuous_on_id continuous_on_norm)
+qed
+
+lemma retract_of_contractible:
+  assumes "contractible t" "s retract_of t"
+    shows "contractible s"
+using assms
+apply (clarsimp simp add: retract_of_def contractible_def retraction_def homotopic_with)
+apply (rule_tac x="r a" in exI)
+apply (rule_tac x="r o h" in exI)
+apply (intro conjI continuous_intros continuous_on_compose)
+apply (erule continuous_on_subset | force)+
+done
+
+lemma retract_of_compact:
+     "\<lbrakk>compact t; s retract_of t\<rbrakk> \<Longrightarrow> compact s"
+  by (metis compact_continuous_image retract_of_def retraction)
+
+lemma retract_of_closed:
+    fixes s :: "'a :: real_normed_vector set"
+    shows "\<lbrakk>closed t; s retract_of t\<rbrakk> \<Longrightarrow> closed s"
+  by (metis closedin_retract closedin_closed_eq)
+
+lemma retract_of_connected:
+    "\<lbrakk>connected t; s retract_of t\<rbrakk> \<Longrightarrow> connected s"
+  by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction)
+
+lemma retract_of_path_connected:
+    "\<lbrakk>path_connected t; s retract_of t\<rbrakk> \<Longrightarrow> path_connected s"
+  by (metis path_connected_continuous_image retract_of_def retraction)
+
+lemma retract_of_simply_connected:
+    "\<lbrakk>simply_connected t; s retract_of t\<rbrakk> \<Longrightarrow> simply_connected s"
+apply (simp add: retract_of_def retraction_def, clarify)
+apply (rule simply_connected_retraction_gen)
+apply (force simp: continuous_on_id elim!: continuous_on_subset)+
+done
+
+lemma retract_of_homotopically_trivial:
+  assumes ts: "t retract_of s"
+      and hom: "\<And>f g. \<lbrakk>continuous_on u f; f ` u \<subseteq> s;
+                       continuous_on u g; g ` u \<subseteq> s\<rbrakk>
+                       \<Longrightarrow> homotopic_with (\<lambda>x. True) u s f g"
+      and "continuous_on u f" "f ` u \<subseteq> t"
+      and "continuous_on u g" "g ` u \<subseteq> t"
+    shows "homotopic_with (\<lambda>x. True) u t f g"
+proof -
+  obtain r where "r ` s \<subseteq> s" "continuous_on s r" "\<forall>x\<in>s. r (r x) = r x" "t = r ` s"
+    using ts by (auto simp: retract_of_def retraction)
+  then obtain k where "Retracts s r t k"
+    unfolding Retracts_def
+    by (metis continuous_on_subset dual_order.trans image_iff image_mono)
+  then show ?thesis
+    apply (rule Retracts.homotopically_trivial_retraction_gen)
+    using assms
+    apply (force simp: hom)+
+    done
+qed
+
+lemma retract_of_homotopically_trivial_null:
+  assumes ts: "t retract_of s"
+      and hom: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s\<rbrakk>
+                     \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) u s f (\<lambda>x. c)"
+      and "continuous_on u f" "f ` u \<subseteq> t"
+  obtains c where "homotopic_with (\<lambda>x. True) u t f (\<lambda>x. c)"
+proof -
+  obtain r where "r ` s \<subseteq> s" "continuous_on s r" "\<forall>x\<in>s. r (r x) = r x" "t = r ` s"
+    using ts by (auto simp: retract_of_def retraction)
+  then obtain k where "Retracts s r t k"
+    unfolding Retracts_def
+    by (metis continuous_on_subset dual_order.trans image_iff image_mono)
+  then show ?thesis
+    apply (rule Retracts.homotopically_trivial_retraction_null_gen)
+    apply (rule TrueI refl assms that | assumption)+
+    done
+qed
+
+lemma retraction_imp_quotient_map:
+   "retraction s t r
+    \<Longrightarrow> u \<subseteq> t
+            \<Longrightarrow> (openin (subtopology euclidean s) {x. x \<in> s \<and> r x \<in> u} \<longleftrightarrow>
+                 openin (subtopology euclidean t) u)"
+apply (clarsimp simp add: retraction)
+apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
+apply (auto simp: elim: continuous_on_subset)
+done
+
+lemma retract_of_locally_compact:
+    fixes s :: "'a :: {heine_borel,real_normed_vector} set"
+    shows  "\<lbrakk> locally compact s; t retract_of s\<rbrakk> \<Longrightarrow> locally compact t"
+  by (metis locally_compact_closedin closedin_retract)
+
+lemma retract_of_times:
+   "\<lbrakk>s retract_of s'; t retract_of t'\<rbrakk> \<Longrightarrow> (s \<times> t) retract_of (s' \<times> t')"
+apply (simp add: retract_of_def retraction_def Sigma_mono, clarify)
+apply (rename_tac f g)
+apply (rule_tac x="\<lambda>z. ((f o fst) z, (g o snd) z)" in exI)
+apply (rule conjI continuous_intros | erule continuous_on_subset | force)+
+done
+
+lemma homotopic_into_retract:
+   "\<lbrakk>f ` s \<subseteq> t; g ` s \<subseteq> t; t retract_of u;
+        homotopic_with (\<lambda>x. True) s u f g\<rbrakk>
+        \<Longrightarrow> homotopic_with (\<lambda>x. True) s t f g"
+apply (subst (asm) homotopic_with_def)
+apply (simp add: homotopic_with retract_of_def retraction_def, clarify)
+apply (rule_tac x="r o h" in exI)
+apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+
+done
+
 end
diff -r 3374f3ffb2ec -r 7700f467892b src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Apr 10 23:15:34 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Apr 11 16:27:42 2016 +0100
@@ -411,13 +411,13 @@
 lemma affine_alt: "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \<in> s)"
   unfolding affine_def by (metis eq_diff_eq')
 
-lemma affine_empty[intro]: "affine {}"
+lemma affine_empty [iff]: "affine {}"
   unfolding affine_def by auto
 
-lemma affine_sing[intro]: "affine {x}"
+lemma affine_sing [iff]: "affine {x}"
   unfolding affine_alt by (auto simp add: scaleR_left_distrib [symmetric])
 
-lemma affine_UNIV[intro]: "affine UNIV"
+lemma affine_UNIV [iff]: "affine UNIV"
   unfolding affine_def by auto
 
 lemma affine_Inter[intro]: "(\<forall>s\<in>f. affine s) \<Longrightarrow> affine (\<Inter>f)"
@@ -433,6 +433,9 @@
 lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s"
   by (metis affine_affine_hull hull_same)
 
+lemma affine_hyperplane: "affine {x. a \<bullet> x = b}"
+  by (simp add: affine_def algebra_simps) (metis distrib_right mult.left_neutral)
+
 
 subsubsection \<open>Some explicit formulations (from Lars Schewe)\<close>
 
@@ -1384,6 +1387,11 @@
   shows "compact s \<and> open s \<longleftrightarrow> s = {}"
   by (auto simp: compact_eq_bounded_closed clopen)
 
+corollary finite_imp_not_open:
+    fixes S :: "'a::{real_normed_vector, perfect_space} set"
+    shows "\<lbrakk>finite S; open S\<rbrakk> \<Longrightarrow> S={}"
+  using clopen [of S] finite_imp_closed not_bounded_UNIV by blast
+
 text \<open>Balls, being convex, are connected.\<close>
 
 lemma convex_prod:
@@ -2745,7 +2753,7 @@
   apply (simp add: aff_dim_affine_independent aff_independent_finite)
   by (metis affine_basis_exists [of s] aff_dim_unique card_subset_eq diff_add_cancel of_nat_eq_iff)
 
-lemma aff_dim_sing:
+lemma aff_dim_sing [simp]:
   fixes a :: "'n::euclidean_space"
   shows "aff_dim {a} = 0"
   using aff_dim_affine_independent[of "{a}"] affine_independent_sing by auto
@@ -3553,7 +3561,7 @@
   shows "closure S \<subseteq> affine hull S"
   by (intro closure_minimal hull_subset affine_closed affine_affine_hull)
 
-lemma closure_same_affine_hull:
+lemma closure_same_affine_hull [simp]:
   fixes S :: "'n::euclidean_space set"
   shows "affine hull (closure S) = affine hull S"
 proof -
@@ -4741,7 +4749,7 @@
 
 subsection \<open>More convexity generalities\<close>
 
-lemma convex_closure:
+lemma convex_closure [intro,simp]:
   fixes s :: "'a::real_normed_vector set"
   assumes "convex s"
   shows "convex (closure s)"
@@ -4753,7 +4761,7 @@
   apply (auto del: tendsto_const intro!: tendsto_intros)
   done
 
-lemma convex_interior:
+lemma convex_interior [intro,simp]:
   fixes s :: "'a::real_normed_vector set"
   assumes "convex s"
   shows "convex (interior s)"
@@ -6379,6 +6387,11 @@
 
 lemmas segment = open_segment_def closed_segment_def
 
+lemma in_segment:
+    "x \<in> closed_segment a b \<longleftrightarrow> (\<exists>u. 0 \<le> u \<and> u \<le> 1 \<and> x = (1 - u) *\<^sub>R a + u *\<^sub>R b)"
+    "x \<in> open_segment a b \<longleftrightarrow> a \<noteq> b \<and> (\<exists>u. 0 < u \<and> u < 1 \<and> x = (1 - u) *\<^sub>R a + u *\<^sub>R b)"
+  using less_eq_real_def by (auto simp: segment algebra_simps)
+
 definition "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
 
 definition "starlike s \<longleftrightarrow> (\<exists>a\<in>s. \<forall>x\<in>s. closed_segment a x \<subseteq> s)"
@@ -7819,9 +7832,9 @@
       have yball: "y \<in> cball z e"
         using mem_cball y_def dist_norm[of z y] e by auto
       have "x \<in> affine hull closure S"
-        using x rel_interior_subset_closure hull_inc[of x "closure S"] by auto
+        using x rel_interior_subset_closure hull_inc[of x "closure S"] by blast
       moreover have "z \<in> affine hull closure S"
-        using z rel_interior_subset hull_subset[of "closure S"] by auto
+        using z rel_interior_subset hull_subset[of "closure S"] by blast
       ultimately have "y \<in> affine hull closure S"
         using y_def affine_affine_hull[of "closure S"]
           mem_affine_3_minus [of "affine hull closure S" z z x "e/norm(z-x)"] by auto
@@ -7969,8 +7982,7 @@
   have "S1 \<subseteq> closure S2"
     using assms unfolding rel_frontier_def by auto
   then have *: "affine hull S1 \<subseteq> affine hull S2"
-    using hull_mono[of "S1" "closure S2"] closure_same_affine_hull[of S2]
-    by auto
+    using hull_mono[of "S1" "closure S2"] closure_same_affine_hull[of S2] by blast
   then have "aff_dim S1 \<le> aff_dim S2"
     using * aff_dim_affine_hull[of S1] aff_dim_affine_hull[of S2]
       aff_dim_subset[of "affine hull S1" "affine hull S2"]
@@ -8072,7 +8084,7 @@
         using \<open>m > 1\<close> by auto
     }
     ultimately have "\<exists>m. m > 1 \<and> (\<forall>e. e > 1 \<and> e \<le> m \<longrightarrow> (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> S )"
-      by auto
+      by blast
   }
   then show ?thesis by auto
 qed
diff -r 3374f3ffb2ec -r 7700f467892b src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sun Apr 10 23:15:34 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Apr 11 16:27:42 2016 +0100
@@ -784,7 +784,7 @@
   apply (auto simp add: subspace_def)
   done
 
-lemma (in real_vector) independent_empty[intro]: "independent {}"
+lemma (in real_vector) independent_empty [iff]: "independent {}"
   by (simp add: dependent_def)
 
 lemma dependent_single[simp]: "dependent {x} \<longleftrightarrow> x = 0"
diff -r 3374f3ffb2ec -r 7700f467892b src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Sun Apr 10 23:15:34 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Apr 11 16:27:42 2016 +0100
@@ -1388,8 +1388,6 @@
      "\<lbrakk>x \<in> t; path_connected t; t \<subseteq> s\<rbrakk> \<Longrightarrow> t \<subseteq> (path_component_set s x)"
   by (metis path_component_mono path_connected_component_set)
 
-subsection \<open>More about path-connectedness\<close>
-
 lemma convex_imp_path_connected:
   fixes s :: "'a::real_normed_vector set"
   assumes "convex s"
@@ -1773,6 +1771,60 @@
 using is_interval_connected_1 is_interval_path_connected path_connected_imp_connected by blast
 
 
+lemma Union_path_component [simp]:
+   "Union {path_component_set S x |x. x \<in> S} = S"
+apply (rule subset_antisym)
+using path_component_subset apply force
+using path_component_refl by auto
+
+lemma path_component_disjoint:
+   "disjnt (path_component_set S a) (path_component_set S b) \<longleftrightarrow>
+    (a \<notin> path_component_set S b)"
+apply (auto simp: disjnt_def)
+using path_component_eq apply fastforce
+using path_component_sym path_component_trans by blast
+
+lemma path_component_eq_eq:
+   "path_component S x = path_component S y \<longleftrightarrow>
+        (x \<notin> S) \<and> (y \<notin> S) \<or> x \<in> S \<and> y \<in> S \<and> path_component S x y"
+apply (rule iffI, metis (no_types) path_component_mem(1) path_component_refl)
+apply (erule disjE, metis Collect_empty_eq_bot path_component_eq_empty)
+apply (rule ext)
+apply (metis path_component_trans path_component_sym)
+done
+
+lemma path_component_unique:
+  assumes "x \<in> c" "c \<subseteq> S" "path_connected c"
+          "\<And>c'. \<lbrakk>x \<in> c'; c' \<subseteq> S; path_connected c'\<rbrakk> \<Longrightarrow> c' \<subseteq> c"
+   shows "path_component_set S x = c"
+apply (rule subset_antisym)
+using assms
+apply (metis mem_Collect_eq subsetCE path_component_eq_eq path_component_subset path_connected_path_component)
+by (simp add: assms path_component_maximal)
+
+lemma path_component_intermediate_subset:
+   "path_component_set u a \<subseteq> t \<and> t \<subseteq> u
+        \<Longrightarrow> path_component_set t a = path_component_set u a"
+by (metis (no_types) path_component_mono path_component_path_component subset_antisym)
+
+lemma complement_path_component_Union:
+  fixes x :: "'a :: topological_space"
+  shows "S - path_component_set S x =
+         \<Union>({path_component_set S y| y. y \<in> S} - {path_component_set S x})"
+proof -
+  have *: "(\<And>x. x \<in> S - {a} \<Longrightarrow> disjnt a x) \<Longrightarrow> \<Union>S - a = \<Union>(S - {a})"
+    for a::"'a set" and S
+    by (auto simp: disjnt_def)
+  have "\<And>y. y \<in> {path_component_set S x |x. x \<in> S} - {path_component_set S x}
+            \<Longrightarrow> disjnt (path_component_set S x) y"
+    using path_component_disjoint path_component_eq by fastforce
+  then have "\<Union>{path_component_set S x |x. x \<in> S} - path_component_set S x =
+             \<Union>({path_component_set S y |y. y \<in> S} - {path_component_set S x})"
+    by (meson *)
+  then show ?thesis by simp
+qed
+
+
 subsection \<open>Sphere is path-connected\<close>
 
 lemma path_connected_punctured_universe:
@@ -3697,11 +3749,10 @@
     shows "homotopic_paths s g h"
   using assms
   unfolding path_def
-  apply (simp add: pathstart_def pathfinish_def homotopic_paths_def homotopic_with_def)
+  apply (simp add: closed_segment_def pathstart_def pathfinish_def homotopic_paths_def homotopic_with_def)
   apply (rule_tac x="\<lambda>y. ((1 - (fst y)) *\<^sub>R g(snd y) + (fst y) *\<^sub>R h(snd y))" in exI)
-  apply (auto intro!: continuous_intros intro: continuous_on_compose2 [where g=g] continuous_on_compose2 [where g=h] )
-  apply (force simp: closed_segment_def)
-  apply (simp_all add: algebra_simps)
+  apply (intro conjI subsetI continuous_intros)
+  apply (fastforce intro: continuous_intros continuous_on_compose2 [where g=g] continuous_on_compose2 [where g=h])+
   done
 
 lemma homotopic_loops_linear:
@@ -4322,4 +4373,852 @@
     done
 qed
 
+subsection\<open>Local versions of topological properties in general\<close>
+
+definition locally :: "('a::topological_space set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
+where
+ "locally P S \<equiv>
+        \<forall>w x. openin (subtopology euclidean S) w \<and> x \<in> w
+              \<longrightarrow> (\<exists>u v. openin (subtopology euclidean S) u \<and> P v \<and>
+                        x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w)"
+
+lemma locallyI:
+  assumes "\<And>w x. \<lbrakk>openin (subtopology euclidean S) w; x \<in> w\<rbrakk>
+                  \<Longrightarrow> \<exists>u v. openin (subtopology euclidean S) u \<and> P v \<and>
+                        x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w"
+    shows "locally P S"
+using assms by (force simp: locally_def)
+
+lemma locallyE:
+  assumes "locally P S" "openin (subtopology euclidean S) w" "x \<in> w"
+  obtains u v where "openin (subtopology euclidean S) u"
+                    "P v" "x \<in> u" "u \<subseteq> v" "v \<subseteq> w"
+using assms by (force simp: locally_def)
+
+lemma locally_mono:
+  assumes "locally P S" "\<And>t. P t \<Longrightarrow> Q t"
+    shows "locally Q S"
+by (metis assms locally_def)
+
+lemma locally_open_subset:
+  assumes "locally P S" "openin (subtopology euclidean S) t"
+    shows "locally P t"
+using assms
+apply (simp add: locally_def)
+apply (erule all_forward)+
+apply (rule impI)
+apply (erule impCE)
+ using openin_trans apply blast
+apply (erule ex_forward)
+by (metis (no_types, hide_lams) Int_absorb1 Int_lower1 Int_subset_iff openin_open openin_subtopology_Int_subset)
+
+lemma locally_diff_closed:
+    "\<lbrakk>locally P S; closedin (subtopology euclidean S) t\<rbrakk> \<Longrightarrow> locally P (S - t)"
+  using locally_open_subset closedin_def by fastforce
+
+lemma locally_empty [iff]: "locally P {}"
+  by (simp add: locally_def openin_subtopology)
+
+lemma locally_singleton [iff]:
+  fixes a :: "'a::metric_space"
+  shows "locally P {a} \<longleftrightarrow> P {a}"
+apply (simp add: locally_def openin_euclidean_subtopology_iff subset_singleton_iff conj_disj_distribR cong: conj_cong)
+using zero_less_one by blast
+
+lemma locally_iff:
+    "locally P S \<longleftrightarrow>
+     (\<forall>T x. open T \<and> x \<in> S \<inter> T \<longrightarrow> (\<exists>U. open U \<and> (\<exists>v. P v \<and> x \<in> S \<inter> U \<and> S \<inter> U \<subseteq> v \<and> v \<subseteq> S \<inter> T)))"
+apply (simp add: le_inf_iff locally_def openin_open, safe)
+apply (metis IntE IntI le_inf_iff)
+apply (metis IntI Int_subset_iff)
+done
+
+lemma locally_Int:
+  assumes S: "locally P S" and t: "locally P t"
+      and P: "\<And>S t. P S \<and> P t \<Longrightarrow> P(S \<inter> t)"
+    shows "locally P (S \<inter> t)"
+using S t unfolding locally_iff
+apply clarify
+apply (drule_tac x=T in spec)+
+apply (drule_tac x=x in spec)+
+apply clarsimp
+apply (rename_tac U1 U2 V1 V2)
+apply (rule_tac x="U1 \<inter> U2" in exI)
+apply (simp add: open_Int)
+apply (rule_tac x="V1 \<inter> V2" in exI)
+apply (auto intro: P)
+done
+
+
+proposition homeomorphism_locally_imp:
+  fixes S :: "'a::metric_space set" and t :: "'b::t2_space set"
+  assumes S: "locally P S" and hom: "homeomorphism S t f g"
+      and Q: "\<And>S t. \<lbrakk>P S; homeomorphism S t f g\<rbrakk> \<Longrightarrow> Q t"
+    shows "locally Q t"
+proof (clarsimp simp: locally_def)
+  fix w y
+  assume "y \<in> w" and "openin (subtopology euclidean t) w"
+  then obtain T where T: "open T" "w = t \<inter> T"
+    by (force simp: openin_open)
+  then have "w \<subseteq> t" by auto
+  have f: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x" "f ` S = t" "continuous_on S f"
+   and g: "\<And>y. y \<in> t \<Longrightarrow> f(g y) = y" "g ` t = S" "continuous_on t g"
+    using hom by (auto simp: homeomorphism_def)
+  have gw: "g ` w = S \<inter> {x. f x \<in> w}"
+    using \<open>w \<subseteq> t\<close>
+    apply auto
+    using \<open>g ` t = S\<close> \<open>w \<subseteq> t\<close> apply blast
+    using g \<open>w \<subseteq> t\<close> apply auto[1]
+    by (simp add: f rev_image_eqI)
+  have o: "openin (subtopology euclidean S) (g ` w)"
+  proof -
+    have "continuous_on S f"
+      using f(3) by blast
+    then show "openin (subtopology euclidean S) (g ` w)"
+      by (simp add: gw Collect_conj_eq \<open>openin (subtopology euclidean t) w\<close> continuous_on_open f(2))
+  qed
+  then obtain u v
+    where osu: "openin (subtopology euclidean S) u" and uv: "P v" "g y \<in> u" "u \<subseteq> v" "v \<subseteq> g ` w"
+    using S [unfolded locally_def, rule_format, of "g ` w" "g y"] \<open>y \<in> w\<close> by force
+  have "v \<subseteq> S" using uv by (simp add: gw)
+  have fv: "f ` v = t \<inter> {x. g x \<in> v}"
+    using \<open>f ` S = t\<close> f \<open>v \<subseteq> S\<close> by auto
+  have "f ` v \<subseteq> w"
+    using uv using Int_lower2 gw image_subsetI mem_Collect_eq subset_iff by auto
+  have contvf: "continuous_on v f"
+    using \<open>v \<subseteq> S\<close> continuous_on_subset f(3) by blast
+  have contvg: "continuous_on (f ` v) g"
+    using \<open>f ` v \<subseteq> w\<close> \<open>w \<subseteq> t\<close> continuous_on_subset g(3) by blast
+  have homv: "homeomorphism v (f ` v) f g"
+    using \<open>v \<subseteq> S\<close> \<open>w \<subseteq> t\<close> f
+    apply (simp add: homeomorphism_def contvf contvg, auto)
+    by (metis f(1) rev_image_eqI rev_subsetD)
+  have 1: "openin (subtopology euclidean t) {x \<in> t. g x \<in> u}"
+    apply (rule continuous_on_open [THEN iffD1, rule_format])
+    apply (rule \<open>continuous_on t g\<close>)
+    using \<open>g ` t = S\<close> apply (simp add: osu)
+    done
+  have 2: "\<exists>v. Q v \<and> y \<in> {x \<in> t. g x \<in> u} \<and> {x \<in> t. g x \<in> u} \<subseteq> v \<and> v \<subseteq> w"
+    apply (rule_tac x="f ` v" in exI)
+    apply (intro conjI Q [OF \<open>P v\<close> homv])
+    using \<open>w \<subseteq> t\<close> \<open>y \<in> w\<close>  \<open>f ` v \<subseteq> w\<close>  uv  apply (auto simp: fv)
+    done
+  show "\<exists>u. openin (subtopology euclidean t) u \<and>
+            (\<exists>v. Q v \<and> y \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w)"
+    by (meson 1 2)
+qed
+
+lemma homeomorphism_locally:
+  fixes f:: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  assumes hom: "homeomorphism S t f g"
+      and eq: "\<And>S t. homeomorphism S t f g \<Longrightarrow> (P S \<longleftrightarrow> Q t)"
+    shows "locally P S \<longleftrightarrow> locally Q t"
+apply (rule iffI)
+apply (erule homeomorphism_locally_imp [OF _ hom])
+apply (simp add: eq)
+apply (erule homeomorphism_locally_imp)
+using eq homeomorphism_sym homeomorphism_symD [OF hom] apply blast+
+done
+
+lemma locally_translation:
+  fixes P :: "'a :: real_normed_vector set \<Rightarrow> bool"
+  shows
+   "(\<And>S. P (image (\<lambda>x. a + x) S) \<longleftrightarrow> P S)
+        \<Longrightarrow> locally P (image (\<lambda>x. a + x) S) \<longleftrightarrow> locally P S"
+apply (rule homeomorphism_locally [OF homeomorphism_translation])
+apply (simp add: homeomorphism_def)
+by metis
+
+lemma locally_injective_linear_image:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes f: "linear f" "inj f" and iff: "\<And>S. P (f ` S) \<longleftrightarrow> Q S"
+    shows "locally P (f ` S) \<longleftrightarrow> locally Q S"
+apply (rule linear_homeomorphism_image [OF f])
+apply (rule_tac f=g and g = f in homeomorphism_locally, assumption)
+by (metis iff homeomorphism_def)
+
+lemma locally_open_map_image:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+  assumes P: "locally P S"
+      and f: "continuous_on S f"
+      and oo: "\<And>t. openin (subtopology euclidean S) t
+                   \<Longrightarrow> openin (subtopology euclidean (f ` S)) (f ` t)"
+      and Q: "\<And>t. \<lbrakk>t \<subseteq> S; P t\<rbrakk> \<Longrightarrow> Q(f ` t)"
+    shows "locally Q (f ` S)"
+proof (clarsimp simp add: locally_def)
+  fix w y
+  assume oiw: "openin (subtopology euclidean (f ` S)) w" and "y \<in> w"
+  then have "w \<subseteq> f ` S" by (simp add: openin_euclidean_subtopology_iff)
+  have oivf: "openin (subtopology euclidean S) {x \<in> S. f x \<in> w}"
+    by (rule continuous_on_open [THEN iffD1, rule_format, OF f oiw])
+  then obtain x where "x \<in> S" "f x = y"
+    using \<open>w \<subseteq> f ` S\<close> \<open>y \<in> w\<close> by blast
+  then obtain u v
+    where "openin (subtopology euclidean S) u" "P v" "x \<in> u" "u \<subseteq> v" "v \<subseteq> {x \<in> S. f x \<in> w}"
+    using P [unfolded locally_def, rule_format, of "{x. x \<in> S \<and> f x \<in> w}" x] oivf \<open>y \<in> w\<close>
+    by auto
+  then show "\<exists>u. openin (subtopology euclidean (f ` S)) u \<and>
+            (\<exists>v. Q v \<and> y \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w)"
+    apply (rule_tac x="f ` u" in exI)
+    apply (rule conjI, blast intro!: oo)
+    apply (rule_tac x="f ` v" in exI)
+    apply (force simp: \<open>f x = y\<close> rev_image_eqI intro: Q)
+    done
+qed
+
+subsection\<open>Basic properties of local compactness\<close>
+
+lemma locally_compact:
+  fixes s :: "'a :: metric_space set"
+  shows
+    "locally compact s \<longleftrightarrow>
+     (\<forall>x \<in> s. \<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and>
+                    openin (subtopology euclidean s) u \<and> compact v)"
+     (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    apply clarify
+    apply (erule_tac w = "s \<inter> ball x 1" in locallyE)
+    by auto
+next
+  assume r [rule_format]: ?rhs
+  have *: "\<exists>u v.
+              openin (subtopology euclidean s) u \<and>
+              compact v \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<inter> T"
+          if "open T" "x \<in> s" "x \<in> T" for x T
+  proof -
+    obtain u v where uv: "x \<in> u" "u \<subseteq> v" "v \<subseteq> s" "compact v" "openin (subtopology euclidean s) u"
+      using r [OF \<open>x \<in> s\<close>] by auto
+    obtain e where "e>0" and e: "cball x e \<subseteq> T"
+      using open_contains_cball \<open>open T\<close> \<open>x \<in> T\<close> by blast
+    show ?thesis
+      apply (rule_tac x="(s \<inter> ball x e) \<inter> u" in exI)
+      apply (rule_tac x="cball x e \<inter> v" in exI)
+      using that \<open>e > 0\<close> e uv
+      apply auto
+      done
+  qed
+  show ?lhs
+    apply (rule locallyI)
+    apply (subst (asm) openin_open)
+    apply (blast intro: *)
+    done
+qed
+
+lemma locally_compactE:
+  fixes s :: "'a :: metric_space set"
+  assumes "locally compact s"
+  obtains u v where "\<And>x. x \<in> s \<Longrightarrow> x \<in> u x \<and> u x \<subseteq> v x \<and> v x \<subseteq> s \<and>
+                             openin (subtopology euclidean s) (u x) \<and> compact (v x)"
+using assms
+unfolding locally_compact by metis
+
+lemma locally_compact_alt:
+  fixes s :: "'a :: heine_borel set"
+  shows "locally compact s \<longleftrightarrow>
+         (\<forall>x \<in> s. \<exists>u. x \<in> u \<and>
+                    openin (subtopology euclidean s) u \<and> compact(closure u) \<and> closure u \<subseteq> s)"
+apply (simp add: locally_compact)
+apply (intro ball_cong ex_cong refl iffI)
+apply (metis bounded_subset closure_eq closure_mono compact_eq_bounded_closed dual_order.trans)
+by (meson closure_subset compact_closure)
+
+lemma locally_compact_Int_cball:
+  fixes s :: "'a :: heine_borel set"
+  shows "locally compact s \<longleftrightarrow> (\<forall>x \<in> s. \<exists>e. 0 < e \<and> closed(cball x e \<inter> s))"
+        (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    apply (simp add: locally_compact openin_contains_cball)
+    apply (clarify | assumption | drule bspec)+
+    by (metis (no_types, lifting)  compact_cball compact_imp_closed compact_Int inf.absorb_iff2 inf.orderE inf_sup_aci(2))
+next
+  assume ?rhs
+  then show ?lhs
+    apply (simp add: locally_compact openin_contains_cball)
+    apply (clarify | assumption | drule bspec)+
+    apply (rule_tac x="ball x e \<inter> s" in exI, simp)
+    apply (rule_tac x="cball x e \<inter> s" in exI)
+    using compact_eq_bounded_closed
+    apply auto
+    apply (metis open_ball le_infI1 mem_ball open_contains_cball_eq)
+    done
+qed
+
+lemma locally_compact_compact:
+  fixes s :: "'a :: heine_borel set"
+  shows "locally compact s \<longleftrightarrow>
+         (\<forall>k. k \<subseteq> s \<and> compact k
+              \<longrightarrow> (\<exists>u v. k \<subseteq> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and>
+                         openin (subtopology euclidean s) u \<and> compact v))"
+        (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then obtain u v where
+    uv: "\<And>x. x \<in> s \<Longrightarrow> x \<in> u x \<and> u x \<subseteq> v x \<and> v x \<subseteq> s \<and>
+                             openin (subtopology euclidean s) (u x) \<and> compact (v x)"
+    by (metis locally_compactE)
+  have *: "\<exists>u v. k \<subseteq> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and> openin (subtopology euclidean s) u \<and> compact v"
+          if "k \<subseteq> s" "compact k" for k
+  proof -
+    have "\<And>C. (\<forall>c\<in>C. openin (subtopology euclidean k) c) \<and> k \<subseteq> \<Union>C \<Longrightarrow>
+                    \<exists>D\<subseteq>C. finite D \<and> k \<subseteq> \<Union>D"
+      using that by (simp add: compact_eq_openin_cover)
+    moreover have "\<forall>c \<in> (\<lambda>x. k \<inter> u x) ` k. openin (subtopology euclidean k) c"
+      using that by clarify (metis subsetD inf.absorb_iff2 openin_subset openin_subtopology_Int_subset topspace_euclidean_subtopology uv)
+    moreover have "k \<subseteq> \<Union>((\<lambda>x. k \<inter> u x) ` k)"
+      using that by clarsimp (meson subsetCE uv)
+    ultimately obtain D where "D \<subseteq> (\<lambda>x. k \<inter> u x) ` k" "finite D" "k \<subseteq> \<Union>D"
+      by metis
+    then obtain T where T: "T \<subseteq> k" "finite T" "k \<subseteq> \<Union>((\<lambda>x. k \<inter> u x) ` T)"
+      by (metis finite_subset_image)
+    have Tuv: "UNION T u \<subseteq> UNION T v"
+      using T that by (force simp: dest!: uv)
+    show ?thesis
+      apply (rule_tac x="\<Union>(u ` T)" in exI)
+      apply (rule_tac x="\<Union>(v ` T)" in exI)
+      apply (simp add: Tuv)
+      using T that
+      apply (auto simp: dest!: uv)
+      done
+  qed
+  show ?rhs
+    by (blast intro: *)
+next
+  assume ?rhs
+  then show ?lhs
+    apply (clarsimp simp add: locally_compact)
+    apply (drule_tac x="{x}" in spec, simp)
+    done
+qed
+
+lemma open_imp_locally_compact:
+  fixes s :: "'a :: heine_borel set"
+  assumes "open s"
+    shows "locally compact s"
+proof -
+  have *: "\<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and> openin (subtopology euclidean s) u \<and> compact v"
+          if "x \<in> s" for x
+  proof -
+    obtain e where "e>0" and e: "cball x e \<subseteq> s"
+      using open_contains_cball assms \<open>x \<in> s\<close> by blast
+    have ope: "openin (subtopology euclidean s) (ball x e)"
+      by (meson e open_ball ball_subset_cball dual_order.trans open_subset)
+    show ?thesis
+      apply (rule_tac x="ball x e" in exI)
+      apply (rule_tac x="cball x e" in exI)
+      using \<open>e > 0\<close> e apply (auto simp: ope)
+      done
+  qed
+  show ?thesis
+    unfolding locally_compact
+    by (blast intro: *)
+qed
+
+lemma closed_imp_locally_compact:
+  fixes s :: "'a :: heine_borel set"
+  assumes "closed s"
+    shows "locally compact s"
+proof -
+  have *: "\<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and>
+                 openin (subtopology euclidean s) u \<and> compact v"
+          if "x \<in> s" for x
+  proof -
+    show ?thesis
+      apply (rule_tac x = "s \<inter> ball x 1" in exI)
+      apply (rule_tac x = "s \<inter> cball x 1" in exI)
+      using \<open>x \<in> s\<close> assms apply auto
+      done
+  qed
+  show ?thesis
+    unfolding locally_compact
+    by (blast intro: *)
+qed
+
+lemma locally_compact_UNIV: "locally compact (UNIV :: 'a :: heine_borel set)"
+  by (simp add: closed_imp_locally_compact)
+
+lemma locally_compact_Int:
+  fixes s :: "'a :: t2_space set"
+  shows "\<lbrakk>locally compact s; locally compact t\<rbrakk> \<Longrightarrow> locally compact (s \<inter> t)"
+by (simp add: compact_Int locally_Int)
+
+lemma locally_compact_closedin:
+  fixes s :: "'a :: heine_borel set"
+  shows "\<lbrakk>closedin (subtopology euclidean s) t; locally compact s\<rbrakk>
+        \<Longrightarrow> locally compact t"
+unfolding closedin_closed
+using closed_imp_locally_compact locally_compact_Int by blast
+
+lemma locally_compact_delete:
+     fixes s :: "'a :: t1_space set"
+     shows "locally compact s \<Longrightarrow> locally compact (s - {a})"
+  by (auto simp: openin_delete locally_open_subset)
+
+lemma locally_closed:
+  fixes s :: "'a :: heine_borel set"
+  shows "locally closed s \<longleftrightarrow> locally compact s"
+        (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    apply (simp only: locally_def)
+    apply (erule all_forward imp_forward asm_rl exE)+
+    apply (rule_tac x = "u \<inter> ball x 1" in exI)
+    apply (rule_tac x = "v \<inter> cball x 1" in exI)
+    apply (force intro: openin_trans)
+    done
+next
+  assume ?rhs then show ?lhs
+    using compact_eq_bounded_closed locally_mono by blast
+qed
+
+subsection\<open>Important special cases of local connectedness and path connectedness\<close>
+
+lemma locally_connected_1:
+  assumes
+    "\<And>v x. \<lbrakk>openin (subtopology euclidean S) v; x \<in> v\<rbrakk>
+              \<Longrightarrow> \<exists>u. openin (subtopology euclidean S) u \<and>
+                      connected u \<and> x \<in> u \<and> u \<subseteq> v"
+   shows "locally connected S"
+apply (clarsimp simp add: locally_def)
+apply (drule assms; blast)
+done
+
+lemma locally_connected_2:
+  assumes "locally connected S"
+          "openin (subtopology euclidean S) t"
+          "x \<in> t"
+   shows "openin (subtopology euclidean S) (connected_component_set t x)"
+proof -
+  { fix y :: 'a
+    let ?SS = "subtopology euclidean S"
+    assume 1: "openin ?SS t"
+              "\<forall>w x. openin ?SS w \<and> x \<in> w \<longrightarrow> (\<exists>u. openin ?SS u \<and> (\<exists>v. connected v \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w))"
+    and "connected_component t x y"
+    then have "y \<in> t" and y: "y \<in> connected_component_set t x"
+      using connected_component_subset by blast+
+    obtain F where
+      "\<forall>x y. (\<exists>w. openin ?SS w \<and> (\<exists>u. connected u \<and> x \<in> w \<and> w \<subseteq> u \<and> u \<subseteq> y)) = (openin ?SS (F x y) \<and> (\<exists>u. connected u \<and> x \<in> F x y \<and> F x y \<subseteq> u \<and> u \<subseteq> y))"
+      by moura
+    then obtain G where
+       "\<forall>a A. (\<exists>U. openin ?SS U \<and> (\<exists>V. connected V \<and> a \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> A)) = (openin ?SS (F a A) \<and> connected (G a A) \<and> a \<in> F a A \<and> F a A \<subseteq> G a A \<and> G a A \<subseteq> A)"
+      by moura
+    then have *: "openin ?SS (F y t) \<and> connected (G y t) \<and> y \<in> F y t \<and> F y t \<subseteq> G y t \<and> G y t \<subseteq> t"
+      using 1 \<open>y \<in> t\<close> by presburger
+    have "G y t \<subseteq> connected_component_set t y"
+      by (metis (no_types) * connected_component_eq_self connected_component_mono contra_subsetD)
+    then have "\<exists>A. openin ?SS A \<and> y \<in> A \<and> A \<subseteq> connected_component_set t x"
+      by (metis (no_types) * connected_component_eq dual_order.trans y)
+  }
+  then show ?thesis
+    using assms openin_subopen by (force simp: locally_def)
+qed
+
+lemma locally_connected_3:
+  assumes "\<And>t x. \<lbrakk>openin (subtopology euclidean S) t; x \<in> t\<rbrakk>
+              \<Longrightarrow> openin (subtopology euclidean S)
+                          (connected_component_set t x)"
+          "openin (subtopology euclidean S) v" "x \<in> v"
+   shows  "\<exists>u. openin (subtopology euclidean S) u \<and> connected u \<and> x \<in> u \<and> u \<subseteq> v"
+using assms connected_component_subset by fastforce
+
+lemma locally_connected:
+  "locally connected S \<longleftrightarrow>
+   (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
+          \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and> connected u \<and> x \<in> u \<and> u \<subseteq> v))"
+by (metis locally_connected_1 locally_connected_2 locally_connected_3)
+
+lemma locally_connected_open_connected_component:
+  "locally connected S \<longleftrightarrow>
+   (\<forall>t x. openin (subtopology euclidean S) t \<and> x \<in> t
+          \<longrightarrow> openin (subtopology euclidean S) (connected_component_set t x))"
+by (metis locally_connected_1 locally_connected_2 locally_connected_3)
+
+lemma locally_path_connected_1:
+  assumes
+    "\<And>v x. \<lbrakk>openin (subtopology euclidean S) v; x \<in> v\<rbrakk>
+              \<Longrightarrow> \<exists>u. openin (subtopology euclidean S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> v"
+   shows "locally path_connected S"
+apply (clarsimp simp add: locally_def)
+apply (drule assms; blast)
+done
+
+lemma locally_path_connected_2:
+  assumes "locally path_connected S"
+          "openin (subtopology euclidean S) t"
+          "x \<in> t"
+   shows "openin (subtopology euclidean S) (path_component_set t x)"
+proof -
+  { fix y :: 'a
+    let ?SS = "subtopology euclidean S"
+    assume 1: "openin ?SS t"
+              "\<forall>w x. openin ?SS w \<and> x \<in> w \<longrightarrow> (\<exists>u. openin ?SS u \<and> (\<exists>v. path_connected v \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w))"
+    and "path_component t x y"
+    then have "y \<in> t" and y: "y \<in> path_component_set t x"
+      using path_component_mem(2) by blast+
+    obtain F where
+      "\<forall>x y. (\<exists>w. openin ?SS w \<and> (\<exists>u. path_connected u \<and> x \<in> w \<and> w \<subseteq> u \<and> u \<subseteq> y)) = (openin ?SS (F x y) \<and> (\<exists>u. path_connected u \<and> x \<in> F x y \<and> F x y \<subseteq> u \<and> u \<subseteq> y))"
+      by moura
+    then obtain G where
+       "\<forall>a A. (\<exists>U. openin ?SS U \<and> (\<exists>V. path_connected V \<and> a \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> A)) = (openin ?SS (F a A) \<and> path_connected (G a A) \<and> a \<in> F a A \<and> F a A \<subseteq> G a A \<and> G a A \<subseteq> A)"
+      by moura
+    then have *: "openin ?SS (F y t) \<and> path_connected (G y t) \<and> y \<in> F y t \<and> F y t \<subseteq> G y t \<and> G y t \<subseteq> t"
+      using 1 \<open>y \<in> t\<close> by presburger
+    have "G y t \<subseteq> path_component_set t y"
+      using * path_component_maximal set_rev_mp by blast
+    then have "\<exists>A. openin ?SS A \<and> y \<in> A \<and> A \<subseteq> path_component_set t x"
+      by (metis "*" \<open>G y t \<subseteq> path_component_set t y\<close> dual_order.trans path_component_eq y)
+  }
+  then show ?thesis
+    using assms openin_subopen by (force simp: locally_def)
+qed
+
+lemma locally_path_connected_3:
+  assumes "\<And>t x. \<lbrakk>openin (subtopology euclidean S) t; x \<in> t\<rbrakk>
+              \<Longrightarrow> openin (subtopology euclidean S) (path_component_set t x)"
+          "openin (subtopology euclidean S) v" "x \<in> v"
+   shows  "\<exists>u. openin (subtopology euclidean S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> v"
+proof -
+  have "path_component v x x"
+    by (meson assms(3) path_component_refl)
+  then show ?thesis
+    by (metis assms(1) assms(2) assms(3) mem_Collect_eq path_component_subset path_connected_path_component)
+qed
+
+proposition locally_path_connected:
+  "locally path_connected S \<longleftrightarrow>
+   (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
+          \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> v))"
+by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
+
+proposition locally_path_connected_open_path_connected_component:
+  "locally path_connected S \<longleftrightarrow>
+   (\<forall>t x. openin (subtopology euclidean S) t \<and> x \<in> t
+          \<longrightarrow> openin (subtopology euclidean S) (path_component_set t x))"
+by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
+
+lemma locally_connected_open_component:
+  "locally connected S \<longleftrightarrow>
+   (\<forall>t c. openin (subtopology euclidean S) t \<and> c \<in> components t
+          \<longrightarrow> openin (subtopology euclidean S) c)"
+by (metis components_iff locally_connected_open_connected_component)
+
+proposition locally_connected_im_kleinen:
+  "locally connected S \<longleftrightarrow>
+   (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
+       \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and>
+                x \<in> u \<and> u \<subseteq> v \<and>
+                (\<forall>y. y \<in> u \<longrightarrow> (\<exists>c. connected c \<and> c \<subseteq> v \<and> x \<in> c \<and> y \<in> c))))"
+   (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    by (fastforce simp add: locally_connected)
+next
+  assume ?rhs
+  have *: "\<exists>T. openin (subtopology euclidean S) T \<and> x \<in> T \<and> T \<subseteq> c"
+       if "openin (subtopology euclidean S) t" and c: "c \<in> components t" and "x \<in> c" for t c x
+  proof -
+    from that \<open>?rhs\<close> [rule_format, of t x]
+    obtain u where u:
+      "openin (subtopology euclidean S) u \<and> x \<in> u \<and> u \<subseteq> t \<and>
+       (\<forall>y. y \<in> u \<longrightarrow> (\<exists>c. connected c \<and> c \<subseteq> t \<and> x \<in> c \<and> y \<in> c))"
+      by auto (meson subsetD in_components_subset)
+    obtain F :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a" where
+      "\<forall>x y. (\<exists>z. z \<in> x \<and> y = connected_component_set x z) = (F x y \<in> x \<and> y = connected_component_set x (F x y))"
+      by moura
+    then have F: "F t c \<in> t \<and> c = connected_component_set t (F t c)"
+      by (meson components_iff c)
+    obtain G :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a" where
+        G: "\<forall>x y. (\<exists>z. z \<in> y \<and> z \<notin> x) = (G x y \<in> y \<and> G x y \<notin> x)"
+      by moura
+     have "G c u \<notin> u \<or> G c u \<in> c"
+      using F by (metis (full_types) u connected_componentI connected_component_eq mem_Collect_eq that(3))
+    then show ?thesis
+      using G u by auto
+  qed
+  show ?lhs
+    apply (clarsimp simp add: locally_connected_open_component)
+    apply (subst openin_subopen)
+    apply (blast intro: *)
+    done
+qed
+
+proposition locally_path_connected_im_kleinen:
+  "locally path_connected S \<longleftrightarrow>
+   (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
+       \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and>
+                x \<in> u \<and> u \<subseteq> v \<and>
+                (\<forall>y. y \<in> u \<longrightarrow> (\<exists>p. path p \<and> path_image p \<subseteq> v \<and>
+                                pathstart p = x \<and> pathfinish p = y))))"
+   (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    apply (simp add: locally_path_connected path_connected_def)
+    apply (erule all_forward ex_forward imp_forward conjE | simp)+
+    by (meson dual_order.trans)
+next
+  assume ?rhs
+  have *: "\<exists>T. openin (subtopology euclidean S) T \<and>
+               x \<in> T \<and> T \<subseteq> path_component_set u z"
+       if "openin (subtopology euclidean S) u" and "z \<in> u" and c: "path_component u z x" for u z x
+  proof -
+    have "x \<in> u"
+      by (meson c path_component_mem(2))
+    with that \<open>?rhs\<close> [rule_format, of u x]
+    obtain U where U:
+      "openin (subtopology euclidean S) U \<and> x \<in> U \<and> U \<subseteq> u \<and>
+       (\<forall>y. y \<in> U \<longrightarrow> (\<exists>p. path p \<and> path_image p \<subseteq> u \<and> pathstart p = x \<and> pathfinish p = y))"
+       by blast
+    show ?thesis
+      apply (rule_tac x=U in exI)
+      apply (auto simp: U)
+      apply (metis U c path_component_trans path_component_def)
+      done
+  qed
+  show ?lhs
+    apply (clarsimp simp add: locally_path_connected_open_path_connected_component)
+    apply (subst openin_subopen)
+    apply (blast intro: *)
+    done
+qed
+
+lemma locally_path_connected_imp_locally_connected:
+  "locally path_connected S \<Longrightarrow> locally connected S"
+using locally_mono path_connected_imp_connected by blast
+
+lemma locally_connected_components:
+  "\<lbrakk>locally connected S; c \<in> components S\<rbrakk> \<Longrightarrow> locally connected c"
+by (meson locally_connected_open_component locally_open_subset openin_subtopology_self)
+
+lemma locally_path_connected_components:
+  "\<lbrakk>locally path_connected S; c \<in> components S\<rbrakk> \<Longrightarrow> locally path_connected c"
+by (meson locally_connected_open_component locally_open_subset locally_path_connected_imp_locally_connected openin_subtopology_self)
+
+lemma locally_path_connected_connected_component:
+  "locally path_connected S \<Longrightarrow> locally path_connected (connected_component_set S x)"
+by (metis components_iff connected_component_eq_empty locally_empty locally_path_connected_components)
+
+lemma open_imp_locally_path_connected:
+  fixes S :: "'a :: real_normed_vector set"
+  shows "open S \<Longrightarrow> locally path_connected S"
+apply (rule locally_mono [of convex])
+apply (simp_all add: locally_def openin_open_eq convex_imp_path_connected)
+apply (meson Topology_Euclidean_Space.open_ball centre_in_ball convex_ball openE order_trans)
+done
+
+lemma open_imp_locally_connected:
+  fixes S :: "'a :: real_normed_vector set"
+  shows "open S \<Longrightarrow> locally connected S"
+by (simp add: locally_path_connected_imp_locally_connected open_imp_locally_path_connected)
+
+lemma locally_path_connected_UNIV: "locally path_connected (UNIV::'a :: real_normed_vector set)"
+  by (simp add: open_imp_locally_path_connected)
+
+lemma locally_connected_UNIV: "locally connected (UNIV::'a :: real_normed_vector set)"
+  by (simp add: open_imp_locally_connected)
+
+lemma openin_connected_component_locally_connected:
+    "locally connected S
+     \<Longrightarrow> openin (subtopology euclidean S) (connected_component_set S x)"
+apply (simp add: locally_connected_open_connected_component)
+by (metis connected_component_eq_empty connected_component_subset open_empty open_subset openin_subtopology_self)
+
+lemma openin_components_locally_connected:
+    "\<lbrakk>locally connected S; c \<in> components S\<rbrakk> \<Longrightarrow> openin (subtopology euclidean S) c"
+  using locally_connected_open_component openin_subtopology_self by blast
+
+lemma openin_path_component_locally_path_connected:
+  "locally path_connected S
+        \<Longrightarrow> openin (subtopology euclidean S) (path_component_set S x)"
+by (metis (no_types) empty_iff locally_path_connected_2 openin_subopen openin_subtopology_self path_component_eq_empty)
+
+lemma closedin_path_component_locally_path_connected:
+    "locally path_connected S
+        \<Longrightarrow> closedin (subtopology euclidean S) (path_component_set S x)"
+apply  (simp add: closedin_def path_component_subset complement_path_component_Union)
+apply (rule openin_Union)
+using openin_path_component_locally_path_connected by auto
+
+lemma convex_imp_locally_path_connected:
+  fixes S :: "'a:: real_normed_vector set"
+  shows "convex S \<Longrightarrow> locally path_connected S"
+apply (clarsimp simp add: locally_path_connected)
+apply (subst (asm) openin_open)
+apply clarify
+apply (erule (1) Topology_Euclidean_Space.openE)
+apply (rule_tac x = "S \<inter> ball x e" in exI)
+apply (force simp: convex_Int convex_imp_path_connected)
+done
+
+subsection\<open>Retracts, in a general sense, preserve (co)homotopic triviality)\<close>
+
+locale Retracts =
+  fixes s h t k
+  assumes conth: "continuous_on s h"
+      and imh: "h ` s = t"
+      and contk: "continuous_on t k"
+      and imk: "k ` t \<subseteq> s"
+      and idhk: "\<And>y. y \<in> t \<Longrightarrow> h(k y) = y"
+
+begin
+
+lemma homotopically_trivial_retraction_gen:
+  assumes P: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> t; Q f\<rbrakk> \<Longrightarrow> P(k o f)"
+      and Q: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk> \<Longrightarrow> Q(h o f)"
+      and Qeq: "\<And>h k. (\<And>x. x \<in> u \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
+      and hom: "\<And>f g. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f;
+                       continuous_on u g; g ` u \<subseteq> s; P g\<rbrakk>
+                       \<Longrightarrow> homotopic_with P u s f g"
+      and contf: "continuous_on u f" and imf: "f ` u \<subseteq> t" and Qf: "Q f"
+      and contg: "continuous_on u g" and img: "g ` u \<subseteq> t" and Qg: "Q g"
+    shows "homotopic_with Q u t f g"
+proof -
+  have feq: "\<And>x. x \<in> u \<Longrightarrow> (h \<circ> (k \<circ> f)) x = f x" using idhk imf by auto
+  have geq: "\<And>x. x \<in> u \<Longrightarrow> (h \<circ> (k \<circ> g)) x = g x" using idhk img by auto
+  have "continuous_on u (k \<circ> f)"
+    using contf continuous_on_compose continuous_on_subset contk imf by blast
+  moreover have "(k \<circ> f) ` u \<subseteq> s"
+    using imf imk by fastforce
+  moreover have "P (k \<circ> f)"
+    by (simp add: P Qf contf imf)
+  moreover have "continuous_on u (k \<circ> g)"
+    using contg continuous_on_compose continuous_on_subset contk img by blast
+  moreover have "(k \<circ> g) ` u \<subseteq> s"
+    using img imk by fastforce
+  moreover have "P (k \<circ> g)"
+    by (simp add: P Qg contg img)
+  ultimately have "homotopic_with P u s (k \<circ> f) (k \<circ> g)"
+    by (rule hom)
+  then have "homotopic_with Q u t (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
+    apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono])
+    using Q by (auto simp: conth imh)
+  then show ?thesis
+    apply (rule homotopic_with_eq)
+    apply (metis feq)
+    apply (metis geq)
+    apply (metis Qeq)
+    done
+qed
+
+lemma homotopically_trivial_retraction_null_gen:
+  assumes P: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> t; Q f\<rbrakk> \<Longrightarrow> P(k o f)"
+      and Q: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk> \<Longrightarrow> Q(h o f)"
+      and Qeq: "\<And>h k. (\<And>x. x \<in> u \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
+      and hom: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk>
+                     \<Longrightarrow> \<exists>c. homotopic_with P u s f (\<lambda>x. c)"
+      and contf: "continuous_on u f" and imf:"f ` u \<subseteq> t" and Qf: "Q f"
+  obtains c where "homotopic_with Q u t f (\<lambda>x. c)"
+proof -
+  have feq: "\<And>x. x \<in> u \<Longrightarrow> (h \<circ> (k \<circ> f)) x = f x" using idhk imf by auto
+  have "continuous_on u (k \<circ> f)"
+    using contf continuous_on_compose continuous_on_subset contk imf by blast
+  moreover have "(k \<circ> f) ` u \<subseteq> s"
+    using imf imk by fastforce
+  moreover have "P (k \<circ> f)"
+    by (simp add: P Qf contf imf)
+  ultimately obtain c where "homotopic_with P u s (k \<circ> f) (\<lambda>x. c)"
+    by (metis hom)
+  then have "homotopic_with Q u t (h \<circ> (k \<circ> f)) (h o (\<lambda>x. c))"
+    apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono])
+    using Q by (auto simp: conth imh)
+  then show ?thesis
+    apply (rule_tac c = "h c" in that)
+    apply (erule homotopic_with_eq)
+    apply (metis feq, simp)
+    apply (metis Qeq)
+    done
+qed
+
+lemma cohomotopically_trivial_retraction_gen:
+  assumes P: "\<And>f. \<lbrakk>continuous_on t f; f ` t \<subseteq> u; Q f\<rbrakk> \<Longrightarrow> P(f o h)"
+      and Q: "\<And>f. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk> \<Longrightarrow> Q(f o k)"
+      and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
+      and hom: "\<And>f g. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f;
+                       continuous_on s g; g ` s \<subseteq> u; P g\<rbrakk>
+                       \<Longrightarrow> homotopic_with P s u f g"
+      and contf: "continuous_on t f" and imf: "f ` t \<subseteq> u" and Qf: "Q f"
+      and contg: "continuous_on t g" and img: "g ` t \<subseteq> u" and Qg: "Q g"
+    shows "homotopic_with Q t u f g"
+proof -
+  have feq: "\<And>x. x \<in> t \<Longrightarrow> (f \<circ> h \<circ> k) x = f x" using idhk imf by auto
+  have geq: "\<And>x. x \<in> t \<Longrightarrow> (g \<circ> h \<circ> k) x = g x" using idhk img by auto
+  have "continuous_on s (f \<circ> h)"
+    using contf conth continuous_on_compose imh by blast
+  moreover have "(f \<circ> h) ` s \<subseteq> u"
+    using imf imh by fastforce
+  moreover have "P (f \<circ> h)"
+    by (simp add: P Qf contf imf)
+  moreover have "continuous_on s (g o h)"
+    using contg continuous_on_compose continuous_on_subset conth imh by blast
+  moreover have "(g \<circ> h) ` s \<subseteq> u"
+    using img imh by fastforce
+  moreover have "P (g \<circ> h)"
+    by (simp add: P Qg contg img)
+  ultimately have "homotopic_with P s u (f o h) (g \<circ> h)"
+    by (rule hom)
+  then have "homotopic_with Q t u (f o h o k) (g \<circ> h o k)"
+    apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
+    using Q by (auto simp: contk imk)
+  then show ?thesis
+    apply (rule homotopic_with_eq)
+    apply (metis feq)
+    apply (metis geq)
+    apply (metis Qeq)
+    done
+qed
+
+lemma cohomotopically_trivial_retraction_null_gen:
+  assumes P: "\<And>f. \<lbrakk>continuous_on t f; f ` t \<subseteq> u; Q f\<rbrakk> \<Longrightarrow> P(f o h)"
+      and Q: "\<And>f. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk> \<Longrightarrow> Q(f o k)"
+      and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
+      and hom: "\<And>f g. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk>
+                       \<Longrightarrow> \<exists>c. homotopic_with P s u f (\<lambda>x. c)"
+      and contf: "continuous_on t f" and imf: "f ` t \<subseteq> u" and Qf: "Q f"
+  obtains c where "homotopic_with Q t u f (\<lambda>x. c)"
+proof -
+  have feq: "\<And>x. x \<in> t \<Longrightarrow> (f \<circ> h \<circ> k) x = f x" using idhk imf by auto
+  have "continuous_on s (f \<circ> h)"
+    using contf conth continuous_on_compose imh by blast
+  moreover have "(f \<circ> h) ` s \<subseteq> u"
+    using imf imh by fastforce
+  moreover have "P (f \<circ> h)"
+    by (simp add: P Qf contf imf)
+  ultimately obtain c where "homotopic_with P s u (f o h) (\<lambda>x. c)"
+    by (metis hom)
+  then have "homotopic_with Q t u (f o h o k) ((\<lambda>x. c) o k)"
+    apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
+    using Q by (auto simp: contk imk)
+  then show ?thesis
+    apply (rule_tac c = c in that)
+    apply (erule homotopic_with_eq)
+    apply (metis feq, simp)
+    apply (metis Qeq)
+    done
+qed
+
 end
+
+lemma simply_connected_retraction_gen:
+  shows "\<lbrakk>simply_connected S; continuous_on S h; h ` S = T;
+          continuous_on T k; k ` T \<subseteq> S; \<And>y. y \<in> T \<Longrightarrow> h(k y) = y\<rbrakk>
+        \<Longrightarrow> simply_connected T"
+apply (simp add: simply_connected_def path_def path_image_def homotopic_loops_def, clarify)
+apply (rule Retracts.homotopically_trivial_retraction_gen
+        [of S h _ k _ "\<lambda>p. pathfinish p = pathstart p"  "\<lambda>p. pathfinish p = pathstart p"])
+apply (simp_all add: Retracts_def pathfinish_def pathstart_def)
+done
+
+lemma homeomorphic_simply_connected:
+    "\<lbrakk>S homeomorphic T; simply_connected S\<rbrakk> \<Longrightarrow> simply_connected T"
+  by (auto simp: homeomorphic_def homeomorphism_def intro: simply_connected_retraction_gen)
+
+lemma homeomorphic_simply_connected_eq:
+    "S homeomorphic T \<Longrightarrow> (simply_connected S \<longleftrightarrow> simply_connected T)"
+  by (metis homeomorphic_simply_connected homeomorphic_sym)
+
+end
diff -r 3374f3ffb2ec -r 7700f467892b src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Apr 10 23:15:34 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 11 16:27:42 2016 +0100
@@ -629,6 +629,31 @@
 lemma subtopology_UNIV[simp]: "subtopology U UNIV = U"
   by (simp add: subtopology_superset)
 
+lemma openin_subtopology_empty:
+   "openin (subtopology U {}) s \<longleftrightarrow> s = {}"
+by (metis Int_empty_right openin_empty openin_subtopology)
+
+lemma closedin_subtopology_empty:
+   "closedin (subtopology U {}) s \<longleftrightarrow> s = {}"
+by (metis Int_empty_right closedin_empty closedin_subtopology)
+
+lemma closedin_subtopology_refl:
+   "closedin (subtopology U u) u \<longleftrightarrow> u \<subseteq> topspace U"
+by (metis closedin_def closedin_topspace inf.absorb_iff2 le_inf_iff topspace_subtopology)
+
+lemma openin_imp_subset:
+   "openin (subtopology U s) t \<Longrightarrow> t \<subseteq> s"
+by (metis Int_iff openin_subtopology subsetI)
+
+lemma closedin_imp_subset:
+   "closedin (subtopology U s) t \<Longrightarrow> t \<subseteq> s"
+by (simp add: closedin_def topspace_subtopology)
+
+lemma openin_subtopology_Un:
+    "openin (subtopology U t) s \<and> openin (subtopology U u) s
+     \<Longrightarrow> openin (subtopology U (t \<union> u)) s"
+by (simp add: openin_subtopology) blast
+
 
 subsubsection \<open>The standard Euclidean topology\<close>
 
@@ -657,6 +682,9 @@
 lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
   by (simp add: open_openin openin_subopen[symmetric])
 
+lemma openin_subtopology_self [simp]: "openin (subtopology euclidean S) S"
+  by (metis openin_topspace topspace_euclidean_subtopology)
+
 text \<open>Basic "localization" results are handy for connectedness.\<close>
 
 lemma openin_open: "openin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))"
@@ -3483,12 +3511,16 @@
     by (auto intro!: exI[of _ "b + norm a"])
 qed
 
+lemma bounded_translation_minus:
+  fixes S :: "'a::real_normed_vector set"
+  shows "bounded S \<Longrightarrow> bounded ((\<lambda>x. x - a) ` S)"
+using bounded_translation [of S "-a"] by simp
+
 lemma bounded_uminus [simp]:
   fixes X :: "'a::real_normed_vector set"
   shows "bounded (uminus ` X) \<longleftrightarrow> bounded X"
 by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp add: add.commute norm_minus_commute)
 
-
 text\<open>Some theorems on sups and infs using the notion "bounded".\<close>
 
 lemma bounded_real: "bounded (S::real set) \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. \<bar>x\<bar> \<le> a)"
@@ -3908,6 +3940,12 @@
   shows "open s \<Longrightarrow> open (s - {x})"
   by (simp add: open_Diff)
 
+lemma openin_delete:
+  fixes a :: "'a :: t1_space"
+  shows "openin (subtopology euclidean u) s
+         \<Longrightarrow> openin (subtopology euclidean u) (s - {a})"
+by (metis Int_Diff open_delete openin_open)
+
 text\<open>Compactness expressed with filters\<close>
 
 lemma closure_iff_nhds_not_empty:
@@ -6043,6 +6081,118 @@
   qed
 qed
 
+subsection\<open>Quotient maps\<close>
+
+lemma quotient_map_imp_continuous_open:
+  assumes t: "f ` s \<subseteq> t"
+      and ope: "\<And>u. u \<subseteq> t
+              \<Longrightarrow> (openin (subtopology euclidean s) {x. x \<in> s \<and> f x \<in> u} \<longleftrightarrow>
+                   openin (subtopology euclidean t) u)"
+    shows "continuous_on s f"
+proof -
+  have [simp]: "{x \<in> s. f x \<in> f ` s} = s" by auto
+  show ?thesis
+    using ope [OF t]
+    apply (simp add: continuous_on_open)
+    by (metis (no_types, lifting) "ope"  openin_imp_subset openin_trans)
+qed
+
+lemma quotient_map_imp_continuous_closed:
+  assumes t: "f ` s \<subseteq> t"
+      and ope: "\<And>u. u \<subseteq> t
+                  \<Longrightarrow> (closedin (subtopology euclidean s) {x. x \<in> s \<and> f x \<in> u} \<longleftrightarrow>
+                       closedin (subtopology euclidean t) u)"
+    shows "continuous_on s f"
+proof -
+  have [simp]: "{x \<in> s. f x \<in> f ` s} = s" by auto
+  show ?thesis
+    using ope [OF t]
+    apply (simp add: continuous_on_closed)
+    by (metis (no_types, lifting) "ope" closedin_imp_subset closedin_subtopology_refl closedin_trans openin_subtopology_refl openin_subtopology_self)
+qed
+
+lemma open_map_imp_quotient_map:
+  assumes contf: "continuous_on s f"
+      and t: "t \<subseteq> f ` s"
+      and ope: "\<And>t. openin (subtopology euclidean s) t
+                   \<Longrightarrow> openin (subtopology euclidean (f ` s)) (f ` t)"
+    shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t} =
+           openin (subtopology euclidean (f ` s)) t"
+proof -
+  have "t = image f {x. x \<in> s \<and> f x \<in> t}"
+    using t by blast
+  then show ?thesis
+    using "ope" contf continuous_on_open by fastforce
+qed
+
+lemma closed_map_imp_quotient_map:
+  assumes contf: "continuous_on s f"
+      and t: "t \<subseteq> f ` s"
+      and ope: "\<And>t. closedin (subtopology euclidean s) t
+              \<Longrightarrow> closedin (subtopology euclidean (f ` s)) (f ` t)"
+    shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t} \<longleftrightarrow>
+           openin (subtopology euclidean (f ` s)) t"
+          (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then have *: "closedin (subtopology euclidean s) (s - {x \<in> s. f x \<in> t})"
+    using closedin_diff by fastforce
+  have [simp]: "(f ` s - f ` (s - {x \<in> s. f x \<in> t})) = t"
+    using t by blast
+  show ?rhs
+    using ope [OF *, unfolded closedin_def] by auto
+next
+  assume ?rhs
+  with contf show ?lhs
+    by (auto simp: continuous_on_open)
+qed
+
+lemma continuous_right_inverse_imp_quotient_map:
+  assumes contf: "continuous_on s f" and imf: "f ` s \<subseteq> t"
+      and contg: "continuous_on t g" and img: "g ` t \<subseteq> s"
+      and fg [simp]: "\<And>y. y \<in> t \<Longrightarrow> f(g y) = y"
+      and u: "u \<subseteq> t"
+    shows "openin (subtopology euclidean s) {x. x \<in> s \<and> f x \<in> u} \<longleftrightarrow>
+           openin (subtopology euclidean t) u"
+          (is "?lhs = ?rhs")
+proof -
+  have f: "\<And>z. openin (subtopology euclidean (f ` s)) z \<Longrightarrow>
+                openin (subtopology euclidean s) {x \<in> s. f x \<in> z}"
+  and  g: "\<And>z. openin (subtopology euclidean (g ` t)) z \<Longrightarrow>
+                openin (subtopology euclidean t) {x \<in> t. g x \<in> z}"
+    using contf contg by (auto simp: continuous_on_open)
+  show ?thesis
+  proof
+    have "{x \<in> t. g x \<in> g ` t \<and> g x \<in> s \<and> f (g x) \<in> u} = {x \<in> t. f (g x) \<in> u}"
+      using imf img by blast
+    also have "... = u"
+      using u by auto
+    finally have [simp]: "{x \<in> t. g x \<in> g ` t \<and> g x \<in> s \<and> f (g x) \<in> u} = u" .
+    assume ?lhs
+    then have *: "openin (subtopology euclidean (g ` t)) (g ` t \<inter> {x \<in> s. f x \<in> u})"
+      by (meson img openin_Int openin_subtopology_Int_subset openin_subtopology_self)
+    show ?rhs
+      using g [OF *] by simp
+  next
+    assume rhs: ?rhs
+    show ?lhs
+      apply (rule f)
+      by (metis fg image_eqI image_subset_iff imf img openin_subopen openin_subtopology_self openin_trans rhs)
+  qed
+qed
+
+lemma continuous_left_inverse_imp_quotient_map:
+  assumes "continuous_on s f"
+      and "continuous_on (f ` s) g"
+      and  "\<And>x. x \<in> s \<Longrightarrow> g(f x) = x"
+      and "u \<subseteq> f ` s"
+    shows "openin (subtopology euclidean s) {x. x \<in> s \<and> f x \<in> u} \<longleftrightarrow>
+           openin (subtopology euclidean (f ` s)) u"
+apply (rule continuous_right_inverse_imp_quotient_map)
+using assms
+apply force+
+done
+
 subsection \<open>A function constant on a set\<close>
 
 definition constant_on  (infixl "(constant'_on)" 50)
@@ -7803,13 +7953,23 @@
   (\<forall>x\<in>s. (g(f x) = x)) \<and> (f ` s = t) \<and> continuous_on s f \<and>
   (\<forall>y\<in>t. (f(g y) = y)) \<and> (g ` t = s) \<and> continuous_on t g"
 
+lemma homeomorphism_translation:
+  fixes a :: "'a :: real_normed_vector"
+  shows "homeomorphism (op + a ` S) S (op + (- a)) (op + a)"
+unfolding homeomorphism_def by (auto simp: algebra_simps continuous_intros)
+
+lemma homeomorphism_symD: "homeomorphism S t f g \<Longrightarrow> homeomorphism t S g f"
+  by (simp add: homeomorphism_def)
+
+lemma homeomorphism_sym: "homeomorphism S t f g = homeomorphism t S g f"
+  by (force simp: homeomorphism_def)
+
 definition homeomorphic :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
     (infixr "homeomorphic" 60)
   where "s homeomorphic t \<equiv> (\<exists>f g. homeomorphism s t f g)"
 
 lemma homeomorphic_refl: "s homeomorphic s"
-  unfolding homeomorphic_def
-  unfolding homeomorphism_def
+  unfolding homeomorphic_def homeomorphism_def
   using continuous_on_id
   apply (rule_tac x = "(\<lambda>x. x)" in exI)
   apply (rule_tac x = "(\<lambda>x. x)" in exI)
@@ -7817,8 +7977,7 @@
   done
 
 lemma homeomorphic_sym: "s homeomorphic t \<longleftrightarrow> t homeomorphic s"
-  unfolding homeomorphic_def
-  unfolding homeomorphism_def
+  unfolding homeomorphic_def homeomorphism_def
   by blast
 
 lemma homeomorphic_trans [trans]:
diff -r 3374f3ffb2ec -r 7700f467892b src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Sun Apr 10 23:15:34 2016 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Apr 11 16:27:42 2016 +0100
@@ -259,6 +259,27 @@
   using real_vector_affinity_eq[where m=m and x=x and y=y and c=c]
   by metis
 
+lemma scaleR_eq_iff [simp]:
+  fixes a :: "'a :: real_vector"
+  shows "b + u *\<^sub>R a = a + u *\<^sub>R b \<longleftrightarrow> a=b \<or> u=1"
+proof (cases "u=1")
+  case True then show ?thesis by auto
+next
+  case False
+  { assume "b + u *\<^sub>R a = a + u *\<^sub>R b"
+    then have "(u - 1) *\<^sub>R a = (u - 1) *\<^sub>R b"
+      by (simp add: algebra_simps)
+    with False have "a=b"
+      by auto
+  }
+  then show ?thesis by auto
+qed
+
+lemma scaleR_collapse [simp]:
+  fixes a :: "'a :: real_vector"
+  shows "(1 - u) *\<^sub>R a + u *\<^sub>R a = a"
+by (simp add: algebra_simps)
+
 
 subsection \<open>Embedding of the Reals into any \<open>real_algebra_1\<close>:
 @{term of_real}\<close>
@@ -920,10 +941,21 @@
 qed
 
 lemma norm_power:
-  fixes x :: "'a::{real_normed_div_algebra}"
+  fixes x :: "'a::real_normed_div_algebra"
   shows "norm (x ^ n) = norm x ^ n"
 by (induct n) (simp_all add: norm_mult)
 
+lemma power_eq_imp_eq_norm:
+  fixes w :: "'a::real_normed_div_algebra"
+  assumes eq: "w ^ n = z ^ n" and "n > 0"
+    shows "norm w = norm z"
+proof -
+  have "norm w ^ n = norm z ^ n"
+    by (metis (no_types) eq norm_power)
+  then show ?thesis
+    using assms by (force intro: power_eq_imp_eq_base)
+qed
+
 lemma norm_mult_numeral1 [simp]:
   fixes a b :: "'a::{real_normed_field, field}"
   shows "norm (numeral w * a) = numeral w * norm a"
@@ -1077,6 +1109,10 @@
   shows "dist x z + dist y z < e ==> dist x y < e"
 by (rule le_less_trans [OF dist_triangle2])
 
+lemma dist_triangle_less_add:
+   "\<lbrakk>dist x1 y < e1; dist x2 y < e2\<rbrakk> \<Longrightarrow> dist x1 x2 < e1 + e2"
+by (rule dist_triangle_lt [where z=y], simp)
+
 lemma dist_triangle_half_l:
   shows "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 \<Longrightarrow> dist x1 x2 < e"
 by (rule dist_triangle_lt [where z=y], simp)
diff -r 3374f3ffb2ec -r 7700f467892b src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Apr 10 23:15:34 2016 +0200
+++ b/src/HOL/Transcendental.thy	Mon Apr 11 16:27:42 2016 +0100
@@ -3569,6 +3569,20 @@
   using sin_ge_zero [of "x-pi"]
   by (simp add: sin_diff)
 
+lemma sin_pi_divide_n_ge_0 [simp]:
+  assumes "n \<noteq> 0" shows "0 \<le> sin (pi / real n)"
+apply (rule sin_ge_zero)
+using assms
+apply (simp_all add: divide_simps)
+done
+
+lemma sin_pi_divide_n_gt_0:
+  assumes "2 \<le> n" shows "0 < sin (pi / real n)"
+apply (rule sin_gt_zero)
+using assms
+apply (simp_all add: divide_simps)
+done
+
 text \<open>FIXME: This proof is almost identical to lemma \<open>cos_is_zero\<close>.
   It should be possible to factor out some of the common parts.\<close>