# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1476110741 -3600
# Node ID 74fde524799e46d6eeb0df6eac002ea41d6bb74c
# Parent  f2c8f6b11dcf74c7d48efb60555ffe48f3851907
invariance of domain

diff -r f2c8f6b11dcf -r 74fde524799e NEWS
--- a/NEWS	Sun Oct 09 16:27:01 2016 +0200
+++ b/NEWS	Mon Oct 10 15:45:41 2016 +0100
@@ -432,7 +432,7 @@
 "~~/src/HOL/Library/FinFun_Syntax".
 
 * HOL-Library: theory Multiset_Permutations (executably) defines the set of
-permutations of a given set or multiset, i.e. the set of all lists that 
+permutations of a given set or multiset, i.e. the set of all lists that
 contain every element of the carrier (multi-)set exactly once.
 
 * HOL-Library: multiset membership is now expressed using set_mset
@@ -485,8 +485,7 @@
 and the Krein–Milman Minkowski theorem.
 
 * HOL-Analysis: Numerous results ported from the HOL Light libraries:
-homeomorphisms, continuous function extensions and other advanced topics
-in topology
+homeomorphisms, continuous function extensions, invariance of domain.
 
 * HOL-Probability: the type of emeasure and nn_integral was changed from
 ereal to ennreal, INCOMPATIBILITY.
diff -r f2c8f6b11dcf -r 74fde524799e src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Oct 09 16:27:01 2016 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Mon Oct 10 15:45:41 2016 +0100
@@ -2021,6 +2021,58 @@
     done
 qed
 
+proposition frontier_subset_retraction:
+  fixes S :: "'a::euclidean_space set"
+  assumes "bounded S" and fros: "frontier S \<subseteq> T"
+      and contf: "continuous_on (closure S) f"
+      and fim: "f ` S \<subseteq> T"
+      and fid: "\<And>x. x \<in> T \<Longrightarrow> f x = x"
+    shows "S \<subseteq> T"
+proof (rule ccontr)
+  assume "\<not> S \<subseteq> T"
+  then obtain a where "a \<in> S" "a \<notin> T" by blast
+  define g where "g \<equiv> \<lambda>z. if z \<in> closure S then f z else z"
+  have "continuous_on (closure S \<union> closure(-S)) g"
+    unfolding g_def
+    apply (rule continuous_on_cases)
+    using fros fid frontier_closures
+        apply (auto simp: contf continuous_on_id)
+    done
+  moreover have "closure S \<union> closure(- S) = UNIV"
+    using closure_Un by fastforce
+  ultimately have contg: "continuous_on UNIV g" by metis
+  obtain B where "0 < B" and B: "closure S \<subseteq> ball a B"
+    using \<open>bounded S\<close> bounded_subset_ballD by blast
+  have notga: "g x \<noteq> a" for x
+    unfolding g_def using fros fim \<open>a \<notin> T\<close>
+    apply (auto simp: frontier_def)
+    using fid interior_subset apply fastforce
+    by (simp add: \<open>a \<in> S\<close> closure_def)
+  define h where "h \<equiv> (\<lambda>y. a + (B / norm(y - a)) *\<^sub>R (y - a)) \<circ> g"
+  have "\<not> (frontier (cball a B) retract_of (cball a B))"
+    by (metis no_retraction_cball \<open>0 < B\<close>)
+  then have "\<And>k. \<not> retraction (cball a B) (frontier (cball a B)) k"
+    by (simp add: retract_of_def)
+  moreover have "retraction (cball a B) (frontier (cball a B)) h"
+    unfolding retraction_def
+  proof (intro conjI ballI)
+    show "frontier (cball a B) \<subseteq> cball a B"
+      by (force simp:)
+    show "continuous_on (cball a B) h"
+      unfolding h_def
+      apply (intro continuous_intros)
+      using contg continuous_on_subset notga apply auto
+      done
+    show "h ` cball a B \<subseteq> frontier (cball a B)"
+      using \<open>0 < B\<close> by (auto simp: h_def notga dist_norm)
+    show "\<And>x. x \<in> frontier (cball a B) \<Longrightarrow> h x = x"
+      apply (auto simp: h_def algebra_simps)
+      apply (simp add: vector_add_divide_simps  notga)
+      by (metis (no_types, hide_lams) B add.commute dist_commute  dist_norm g_def mem_ball not_less_iff_gr_or_eq  subset_eq)
+  qed
+  ultimately show False by simp
+qed
+
 subsection\<open>Retractions\<close>
 
 lemma retraction:
@@ -3192,7 +3244,7 @@
   shows "S retract_of UNIV \<longleftrightarrow> AR S \<and> closed S"
 by (metis AR_ANR AR_imp_retract ENR_def ENR_imp_ANR closed_UNIV closed_closedin contractible_UNIV empty_not_UNIV open_UNIV retract_of_closed retract_of_contractible retract_of_empty(1) subtopology_UNIV)
 
-lemma compact_AR [simp]:
+lemma compact_AR:
   fixes S :: "'a::euclidean_space set"
   shows "compact S \<and> AR S \<longleftrightarrow> compact S \<and> S retract_of UNIV"
 using compact_imp_closed retract_of_UNIV by blast
@@ -3893,7 +3945,7 @@
     apply (simp add: ENR_def)
     apply (rule_tac x = "{x. x \<in> UNIV \<and>
                              closest_point (affine hull S) x \<in> (- {a})}" in exI)
-    apply (simp add: open_openin)
+    apply simp
     done
 qed
 
@@ -4189,5 +4241,89 @@
   then show ?thesis by blast
 qed
 
+subsection\<open>The complement of a set and path-connectedness\<close>
+
+text\<open>Complement in dimension N > 1 of set homeomorphic to any interval in
+ any dimension is (path-)connected. This naively generalizes the argument
+ in Ryuji Maehara's paper "The Jordan curve theorem via the Brouwer fixed point theorem",
+American Mathematical Monthly 1984.\<close>
+
+lemma unbounded_components_complement_absolute_retract:
+  fixes S :: "'a::euclidean_space set"
+  assumes C: "C \<in> components(- S)" and S: "compact S" "AR S"
+    shows "\<not> bounded C"
+proof -
+  obtain y where y: "C = connected_component_set (- S) y" and "y \<notin> S"
+    using C by (auto simp: components_def)
+  have "open(- S)"
+    using S by (simp add: closed_open compact_eq_bounded_closed)
+  have "S retract_of UNIV"
+    using S compact_AR by blast
+  then obtain r where contr: "continuous_on UNIV r" and ontor: "range r \<subseteq> S"
+                  and r: "\<And>x. x \<in> S \<Longrightarrow> r x = x"
+    by (auto simp: retract_of_def retraction_def)
+  show ?thesis
+  proof
+    assume "bounded C"
+    have "connected_component_set (- S) y \<subseteq> S"
+    proof (rule frontier_subset_retraction)
+      show "bounded (connected_component_set (- S) y)"
+        using \<open>bounded C\<close> y by blast
+      show "frontier (connected_component_set (- S) y) \<subseteq> S"
+        using C \<open>compact S\<close> compact_eq_bounded_closed frontier_of_components_closed_complement y by blast
+      show "continuous_on (closure (connected_component_set (- S) y)) r"
+        by (blast intro: continuous_on_subset [OF contr])
+    qed (use ontor r in auto)
+    with \<open>y \<notin> S\<close> show False by force
+  qed
+qed
+
+lemma connected_complement_absolute_retract:
+  fixes S :: "'a::euclidean_space set"
+  assumes S: "compact S" "AR S" and 2: "2 \<le> DIM('a)"
+    shows "connected(- S)"
+proof -
+  have "S retract_of UNIV"
+    using S compact_AR by blast
+  show ?thesis
+    apply (clarsimp simp: connected_iff_connected_component_eq)
+    apply (rule cobounded_unique_unbounded_component [OF _ 2])
+      apply (simp add: \<open>compact S\<close> compact_imp_bounded)
+     apply (meson ComplI S componentsI unbounded_components_complement_absolute_retract)+
+    done
+qed
+
+lemma path_connected_complement_absolute_retract:
+  fixes S :: "'a::euclidean_space set"
+  assumes "compact S" "AR S" "2 \<le> DIM('a)"
+    shows "path_connected(- S)"
+  using connected_complement_absolute_retract [OF assms]
+  using \<open>compact S\<close> compact_eq_bounded_closed connected_open_path_connected by blast
+
+theorem connected_complement_homeomorphic_convex_compact:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes hom: "S homeomorphic T" and T: "convex T" "compact T" and 2: "2 \<le> DIM('a)"
+    shows "connected(- S)"
+proof (cases "S = {}")
+  case True
+  then show ?thesis
+    by (simp add: connected_UNIV)
+next
+  case False
+  show ?thesis
+  proof (rule connected_complement_absolute_retract)
+    show "compact S"
+      using \<open>compact T\<close> hom homeomorphic_compactness by auto
+    show "AR S"
+      by (meson AR_ANR False \<open>convex T\<close> convex_imp_ANR convex_imp_contractible hom homeomorphic_ANR_iff_ANR homeomorphic_contractible_eq)
+  qed (rule 2)
+qed
+
+corollary path_connected_complement_homeomorphic_convex_compact:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes hom: "S homeomorphic T" "convex T" "compact T" "2 \<le> DIM('a)"
+    shows "path_connected(- S)"
+  using connected_complement_homeomorphic_convex_compact [OF assms]
+  using \<open>compact T\<close> compact_eq_bounded_closed connected_open_path_connected hom homeomorphic_compactness by blast
 
 end
diff -r f2c8f6b11dcf -r 74fde524799e src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sun Oct 09 16:27:01 2016 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Oct 10 15:45:41 2016 +0100
@@ -2384,7 +2384,7 @@
   shows "closed s \<and> open s \<longleftrightarrow> s = {} \<or> s = UNIV"
 apply (rule iffI)
  apply (rule connected_UNIV [unfolded connected_clopen, rule_format])
- apply (force simp add: open_openin closed_closedin, force)
+ apply (force simp add: closed_closedin, force)
 done
 
 corollary compact_open:
@@ -12085,15 +12085,11 @@
     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
+      by (rule continuous_openin_preimage [where T=UNIV]) (simp_all add: contf)
     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
+      by (rule continuous_openin_preimage [where T=UNIV]) (simp_all add: contf)
     then show "openin (subtopology euclidean U) {x \<in> U. f x < 0}" by simp
   next
     show "S \<subseteq> {x \<in> U. 0 < f x}"
@@ -12671,7 +12667,7 @@
 apply safe
 apply (metis DIM_positive DIM_real card_ge_dim_independent contra_subsetD dim_empty dim_insert dim_singleton empty_subsetI independent_empty less_not_refl zero_le)
 by (metis dim_singleton dim_subset le_0_eq)
-
+                  
 lemma aff_dim_insert:
   fixes a :: "'a::euclidean_space"
   shows "aff_dim (insert a S) = (if a \<in> affine hull S then aff_dim S else aff_dim S + 1)"
@@ -13594,6 +13590,24 @@
   shows "aff_dim S < DIM('a) \<longleftrightarrow> (affine hull S \<noteq> UNIV)"
 by (metis (no_types) aff_dim_affine_hull aff_dim_le_DIM aff_dim_UNIV affine_hull_UNIV less_le)
 
+
+lemma dim_Times:
+  fixes S :: "'a :: euclidean_space set" and T :: "'a set"
+  assumes "subspace S" "subspace T"
+  shows "dim(S \<times> T) = dim S + dim T"
+proof -
+  have ss: "subspace ((\<lambda>x. (x, 0)) ` S)" "subspace (Pair 0 ` T)"
+    by (rule subspace_linear_image, unfold_locales, auto simp: assms)+
+  have "dim(S \<times> T) = dim({u + v |u v. u \<in> (\<lambda>x. (x, 0)) ` S \<and> v \<in> Pair 0 ` T})"
+    by (simp add: Times_eq_image_sum)
+  moreover have "dim ((\<lambda>x. (x, 0::'a)) ` S) = dim S" "dim (Pair (0::'a) ` T) = dim T"
+    by (auto simp: additive.intro linear.intro linear_axioms.intro inj_on_def intro: dim_image_eq)
+  moreover have "dim ((\<lambda>x. (x, 0)) ` S \<inter> Pair 0 ` T) = 0"
+    by (subst dim_eq_0) (force simp: zero_prod_def)
+  ultimately show ?thesis
+    using dim_sums_Int [OF ss] by linarith
+qed
+
 subsection\<open> Orthogonal bases, Gram-Schmidt process, and related theorems\<close>
 
 lemma span_delete_0 [simp]: "span(S - {0}) = span S"
@@ -13934,6 +13948,74 @@
     by (metis (no_types, lifting) dim_orthogonal_sum dim_span mem_Collect_eq orthogonal_commute orthogonal_def)
 qed
 
+lemma aff_dim_openin:
+  fixes S :: "'a::euclidean_space set"
+  assumes ope: "openin (subtopology euclidean T) S" and "affine T" "S \<noteq> {}"
+  shows "aff_dim S = aff_dim T"
+proof -
+  show ?thesis
+  proof (rule order_antisym)
+    show "aff_dim S \<le> aff_dim T"
+      by (blast intro: aff_dim_subset [OF openin_imp_subset] ope)
+  next
+    obtain a where "a \<in> S"
+      using \<open>S \<noteq> {}\<close> by blast
+    have "S \<subseteq> T"
+      using ope openin_imp_subset by auto
+    then have "a \<in> T"
+      using \<open>a \<in> S\<close> by auto
+    then have subT': "subspace ((\<lambda>x. - a + x) ` T)"
+      using affine_diffs_subspace \<open>affine T\<close> by auto
+    then obtain B where Bsub: "B \<subseteq> ((\<lambda>x. - a + x) ` T)" and po: "pairwise orthogonal B"
+                    and eq1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1" and "independent B"
+                    and cardB: "card B = dim ((\<lambda>x. - a + x) ` T)"
+                    and spanB: "span B = ((\<lambda>x. - a + x) ` T)"
+      by (rule orthonormal_basis_subspace) auto
+    obtain e where "0 < e" and e: "cball a e \<inter> T \<subseteq> S"
+      by (meson \<open>a \<in> S\<close> openin_contains_cball ope)
+    have "aff_dim T = aff_dim ((\<lambda>x. - a + x) ` T)"
+      by (metis aff_dim_translation_eq)
+    also have "... = dim ((\<lambda>x. - a + x) ` T)"
+      using aff_dim_subspace subT' by blast
+    also have "... = card B"
+      by (simp add: cardB)
+    also have "... = card ((\<lambda>x. e *\<^sub>R x) ` B)"
+      using \<open>0 < e\<close>  by (force simp: inj_on_def card_image)
+    also have "... \<le> dim ((\<lambda>x. - a + x) ` S)"
+    proof (simp, rule independent_card_le_dim)
+      have e': "cball 0 e \<inter> (\<lambda>x. x - a) ` T \<subseteq> (\<lambda>x. x - a) ` S"
+        using e by (auto simp: dist_norm norm_minus_commute subset_eq)
+      have "(\<lambda>x. e *\<^sub>R x) ` B \<subseteq> cball 0 e \<inter> (\<lambda>x. x - a) ` T"
+        using Bsub \<open>0 < e\<close> eq1 subT' \<open>a \<in> T\<close> by (auto simp: subspace_def)
+      then show "(\<lambda>x. e *\<^sub>R x) ` B \<subseteq> (\<lambda>x. x - a) ` S"
+        using e' by blast
+      show "independent ((\<lambda>x. e *\<^sub>R x) ` B)"
+        using \<open>independent B\<close>
+        apply (rule independent_injective_image, simp)
+        by (metis \<open>0 < e\<close> injective_scaleR less_irrefl)
+    qed
+    also have "... = aff_dim S"
+      using \<open>a \<in> S\<close> aff_dim_eq_dim hull_inc by force
+    finally show "aff_dim T \<le> aff_dim S" .
+  qed
+qed
+
+lemma dim_openin:
+  fixes S :: "'a::euclidean_space set"
+  assumes ope: "openin (subtopology euclidean T) S" and "subspace T" "S \<noteq> {}"
+  shows "dim S = dim T"
+proof (rule order_antisym)
+  show "dim S \<le> dim T"
+    by (metis ope dim_subset openin_subset topspace_euclidean_subtopology)
+next
+  have "dim T = aff_dim S"
+    using aff_dim_openin
+    by (metis aff_dim_subspace \<open>subspace T\<close> \<open>S \<noteq> {}\<close> ope subspace_affine)
+  also have "... \<le> dim S"
+    by (metis aff_dim_subset aff_dim_subspace dim_span span_inc subspace_span)
+  finally show "dim T \<le> dim S" by simp
+qed
+
 subsection\<open>Parallel slices, etc.\<close>
 
 text\<open> If we take a slice out of a set, we can do it perpendicularly,
@@ -14249,7 +14331,6 @@
     done
 qed
 
-
 corollary paracompact_closedin:
   fixes S :: "'a :: euclidean_space set"
   assumes cin: "closedin (subtopology euclidean U) S"
diff -r f2c8f6b11dcf -r 74fde524799e src/HOL/Analysis/FurtherTopology.thy
--- a/src/HOL/Analysis/FurtherTopology.thy	Sun Oct 09 16:27:01 2016 +0200
+++ b/src/HOL/Analysis/FurtherTopology.thy	Mon Oct 10 15:45:41 2016 +0100
@@ -1,4 +1,4 @@
-section \<open>Extending Continous Maps, etc..\<close>
+section \<open>Extending Continous Maps, Invariance of Domain, etc..\<close>
 
 text\<open>Ported from HOL Light (moretop.ml) by L C Paulson\<close>
 
@@ -1888,4 +1888,468 @@
     done
 qed
 
+subsection\<open> Invariance of domain and corollaries\<close>
+
+lemma invariance_of_domain_ball:
+  fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
+  assumes contf: "continuous_on (cball a r) f" and "0 < r"
+     and inj: "inj_on f (cball a r)"
+   shows "open(f ` ball a r)"
+proof (cases "DIM('a) = 1")
+  case True
+  obtain h::"'a\<Rightarrow>real" and k
+        where "linear h" "linear k" "h ` UNIV = UNIV" "k ` UNIV = UNIV"
+              "\<And>x. norm(h x) = norm x" "\<And>x. norm(k x) = norm x"
+              "\<And>x. k(h x) = x" "\<And>x. h(k x) = x"
+    apply (rule isomorphisms_UNIV_UNIV [where 'M='a and 'N=real])
+      using True
+       apply force
+      by (metis UNIV_I UNIV_eq_I imageI)
+    have cont: "continuous_on S h"  "continuous_on T k" for S T
+      by (simp_all add: \<open>linear h\<close> \<open>linear k\<close> linear_continuous_on linear_linear)
+    have "continuous_on (h ` cball a r) (h \<circ> f \<circ> k)"
+      apply (intro continuous_on_compose cont continuous_on_subset [OF contf])
+      apply (auto simp: \<open>\<And>x. k (h x) = x\<close>)
+      done
+    moreover have "is_interval (h ` cball a r)"
+      by (simp add: is_interval_connected_1 \<open>linear h\<close> linear_continuous_on linear_linear connected_continuous_image)
+    moreover have "inj_on (h \<circ> f \<circ> k) (h ` cball a r)"
+      using inj by (simp add: inj_on_def) (metis \<open>\<And>x. k (h x) = x\<close>)
+    ultimately have *: "\<And>T. \<lbrakk>open T; T \<subseteq> h ` cball a r\<rbrakk> \<Longrightarrow> open ((h \<circ> f \<circ> k) ` T)"
+      using injective_eq_1d_open_map_UNIV by blast
+    have "open ((h \<circ> f \<circ> k) ` (h ` ball a r))"
+      by (rule *) (auto simp: \<open>linear h\<close> \<open>range h = UNIV\<close> open_surjective_linear_image)
+    then have "open ((h \<circ> f) ` ball a r)"
+      by (simp add: image_comp \<open>\<And>x. k (h x) = x\<close> cong: image_cong)
+    then show ?thesis
+      apply (simp add: image_comp [symmetric])
+      apply (metis open_bijective_linear_image_eq \<open>linear h\<close> \<open>\<And>x. k (h x) = x\<close> \<open>range h = UNIV\<close> bijI inj_on_def)
+      done
+next
+  case False
+  then have 2: "DIM('a) \<ge> 2"
+    by (metis DIM_ge_Suc0 One_nat_def Suc_1 antisym not_less_eq_eq)
+  have fimsub: "f ` ball a r \<subseteq> - f ` sphere a r"
+    using inj  by clarsimp (metis inj_onD less_eq_real_def mem_cball order_less_irrefl)
+  have hom: "f ` sphere a r homeomorphic sphere a r"
+    by (meson compact_sphere contf continuous_on_subset homeomorphic_compact homeomorphic_sym inj inj_on_subset sphere_cball)
+  then have nconn: "\<not> connected (- f ` sphere a r)"
+    by (rule Jordan_Brouwer_separation) (auto simp: \<open>0 < r\<close>)
+  obtain C where C: "C \<in> components (- f ` sphere a r)" and "bounded C"
+    apply (rule cobounded_has_bounded_component [OF _ nconn])
+      apply (simp_all add: 2)
+    by (meson compact_imp_bounded compact_continuous_image_eq compact_sphere contf inj sphere_cball)
+  moreover have "f ` (ball a r) = C"
+  proof
+    have "C \<noteq> {}"
+      by (rule in_components_nonempty [OF C])
+    show "C \<subseteq> f ` ball a r"
+    proof (rule ccontr)
+      assume nonsub: "\<not> C \<subseteq> f ` ball a r"
+      have "- f ` cball a r \<subseteq> C"
+      proof (rule components_maximal [OF C])
+        have "f ` cball a r homeomorphic cball a r"
+          using compact_cball contf homeomorphic_compact homeomorphic_sym inj by blast
+        then show "connected (- f ` cball a r)"
+          by (auto intro: connected_complement_homeomorphic_convex_compact 2)
+        show "- f ` cball a r \<subseteq> - f ` sphere a r"
+          by auto
+        then show "C \<inter> - f ` cball a r \<noteq> {}"
+          using \<open>C \<noteq> {}\<close> in_components_subset [OF C] nonsub
+          using image_iff by fastforce
+      qed
+      then have "bounded (- f ` cball a r)"
+        using bounded_subset \<open>bounded C\<close> by auto
+      then have "\<not> bounded (f ` cball a r)"
+        using cobounded_imp_unbounded by blast
+      then show "False"
+        using compact_continuous_image [OF contf] compact_cball compact_imp_bounded by blast
+    qed
+    with \<open>C \<noteq> {}\<close> have "C \<inter> f ` ball a r \<noteq> {}"
+      by (simp add: inf.absorb_iff1)
+    then show "f ` ball a r \<subseteq> C"
+      by (metis components_maximal [OF C _ fimsub] connected_continuous_image ball_subset_cball connected_ball contf continuous_on_subset)
+  qed
+  moreover have "open (- f ` sphere a r)"
+    using hom compact_eq_bounded_closed compact_sphere homeomorphic_compactness by blast
+  ultimately show ?thesis
+    using open_components by blast
+qed
+
+
+text\<open>Proved by L. E. J. Brouwer (1912)\<close>
+theorem invariance_of_domain:
+  fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
+  assumes "continuous_on S f" "open S" "inj_on f S"
+    shows "open(f ` S)"
+  unfolding open_subopen [of "f`S"]
+proof clarify
+  fix a
+  assume "a \<in> S"
+  obtain \<delta> where "\<delta> > 0" and \<delta>: "cball a \<delta> \<subseteq> S"
+    using \<open>open S\<close> \<open>a \<in> S\<close> open_contains_cball_eq by blast
+  show "\<exists>T. open T \<and> f a \<in> T \<and> T \<subseteq> f ` S"
+  proof (intro exI conjI)
+    show "open (f ` (ball a \<delta>))"
+      by (meson \<delta> \<open>0 < \<delta>\<close> assms continuous_on_subset inj_on_subset invariance_of_domain_ball)
+    show "f a \<in> f ` ball a \<delta>"
+      by (simp add: \<open>0 < \<delta>\<close>)
+    show "f ` ball a \<delta> \<subseteq> f ` S"
+      using \<delta> ball_subset_cball by blast
+  qed
+qed
+
+lemma inv_of_domain_ss0:
+  fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
+  assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U \<subseteq> S"
+      and "subspace S" and dimS: "dim S = DIM('b::euclidean_space)"
+      and ope: "openin (subtopology euclidean S) U"
+    shows "openin (subtopology euclidean S) (f ` U)"
+proof -
+  have "U \<subseteq> S"
+    using ope openin_imp_subset by blast
+  have "(UNIV::'b set) homeomorphic S"
+    by (simp add: \<open>subspace S\<close> dimS dim_UNIV homeomorphic_subspaces)
+  then obtain h k where homhk: "homeomorphism (UNIV::'b set) S h k"
+    using homeomorphic_def by blast
+  have homkh: "homeomorphism S (k ` S) k h"
+    using homhk homeomorphism_image2 homeomorphism_sym by fastforce
+  have "open ((k \<circ> f \<circ> h) ` k ` U)"
+  proof (rule invariance_of_domain)
+    show "continuous_on (k ` U) (k \<circ> f \<circ> h)"
+    proof (intro continuous_intros)
+      show "continuous_on (k ` U) h"
+        by (meson continuous_on_subset [OF homeomorphism_cont1 [OF homhk]] top_greatest)
+      show "continuous_on (h ` k ` U) f"
+        apply (rule continuous_on_subset [OF contf], clarify)
+        apply (metis homhk homeomorphism_def ope openin_imp_subset rev_subsetD)
+        done
+      show "continuous_on (f ` h ` k ` U) k"
+        apply (rule continuous_on_subset [OF homeomorphism_cont2 [OF homhk]])
+        using fim homhk homeomorphism_apply2 ope openin_subset by fastforce
+    qed
+    have ope_iff: "\<And>T. open T \<longleftrightarrow> openin (subtopology euclidean (k ` S)) T"
+      using homhk homeomorphism_image2 open_openin by fastforce
+    show "open (k ` U)"
+      by (simp add: ope_iff homeomorphism_imp_open_map [OF homkh ope])
+    show "inj_on (k \<circ> f \<circ> h) (k ` U)"
+      apply (clarsimp simp: inj_on_def)
+      by (metis subsetD fim homeomorphism_apply2 [OF homhk] image_subset_iff inj_on_eq_iff injf \<open>U \<subseteq> S\<close>)
+  qed
+  moreover
+  have eq: "f ` U = h ` (k \<circ> f \<circ> h \<circ> k) ` U"
+    apply (auto simp: image_comp [symmetric])
+    apply (metis homkh \<open>U \<subseteq> S\<close> fim homeomorphism_image2 homeomorphism_of_subsets homhk imageI subset_UNIV)
+    by (metis \<open>U \<subseteq> S\<close> subsetD fim homeomorphism_def homhk image_eqI)
+  ultimately show ?thesis
+    by (metis (no_types, hide_lams) homeomorphism_imp_open_map homhk image_comp open_openin subtopology_UNIV)
+qed
+
+lemma inv_of_domain_ss1:
+  fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
+  assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U \<subseteq> S"
+      and "subspace S"
+      and ope: "openin (subtopology euclidean S) U"
+    shows "openin (subtopology euclidean S) (f ` U)"
+proof -
+  define S' where "S' \<equiv> {y. \<forall>x \<in> S. orthogonal x y}"
+  have "subspace S'"
+    by (simp add: S'_def subspace_orthogonal_to_vectors)
+  define g where "g \<equiv> \<lambda>z::'a*'a. ((f \<circ> fst)z, snd z)"
+  have "openin (subtopology euclidean (S \<times> S')) (g ` (U \<times> S'))"
+  proof (rule inv_of_domain_ss0)
+    show "continuous_on (U \<times> S') g"
+      apply (simp add: g_def)
+      apply (intro continuous_intros continuous_on_compose2 [OF contf continuous_on_fst], auto)
+      done
+    show "g ` (U \<times> S') \<subseteq> S \<times> S'"
+      using fim  by (auto simp: g_def)
+    show "inj_on g (U \<times> S')"
+      using injf by (auto simp: g_def inj_on_def)
+    show "subspace (S \<times> S')"
+      by (simp add: \<open>subspace S'\<close> \<open>subspace S\<close> subspace_Times)
+    show "openin (subtopology euclidean (S \<times> S')) (U \<times> S')"
+      by (simp add: openin_Times [OF ope])
+    have "dim (S \<times> S') = dim S + dim S'"
+      by (simp add: \<open>subspace S'\<close> \<open>subspace S\<close> dim_Times)
+    also have "... = DIM('a)"
+      using dim_subspace_orthogonal_to_vectors [OF \<open>subspace S\<close> subspace_UNIV]
+      by (simp add: add.commute S'_def)
+    finally show "dim (S \<times> S') = DIM('a)" .
+  qed
+  moreover have "g ` (U \<times> S') = f ` U \<times> S'"
+    by (auto simp: g_def image_iff)
+  moreover have "0 \<in> S'"
+    using \<open>subspace S'\<close> subspace_affine by blast
+  ultimately show ?thesis
+    by (auto simp: openin_Times_eq)
+qed
+
+
+corollary invariance_of_domain_subspaces:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes ope: "openin (subtopology euclidean U) S"
+      and "subspace U" "subspace V" and VU: "dim V \<le> dim U"
+      and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+      and injf: "inj_on f S"
+    shows "openin (subtopology euclidean V) (f ` S)"
+proof -
+  obtain V' where "subspace V'" "V' \<subseteq> U" "dim V' = dim V"
+    using choose_subspace_of_subspace [OF VU]
+    by (metis span_eq \<open>subspace U\<close>)
+  then have "V homeomorphic V'"
+    by (simp add: \<open>subspace V\<close> homeomorphic_subspaces)
+  then obtain h k where homhk: "homeomorphism V V' h k"
+    using homeomorphic_def by blast
+  have eq: "f ` S = k ` (h \<circ> f) ` S"
+  proof -
+    have "k ` h ` f ` S = f ` S"
+      by (meson fim homeomorphism_def homeomorphism_of_subsets homhk subset_refl)
+    then show ?thesis
+      by (simp add: image_comp)
+  qed
+  show ?thesis
+    unfolding eq
+  proof (rule homeomorphism_imp_open_map)
+    show homkh: "homeomorphism V' V k h"
+      by (simp add: homeomorphism_symD homhk)
+    have hfV': "(h \<circ> f) ` S \<subseteq> V'"
+      using fim homeomorphism_image1 homhk by fastforce
+    moreover have "openin (subtopology euclidean U) ((h \<circ> f) ` S)"
+    proof (rule inv_of_domain_ss1)
+      show "continuous_on S (h \<circ> f)"
+        by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_cont1 homhk)
+      show "inj_on (h \<circ> f) S"
+        apply (clarsimp simp: inj_on_def)
+        by (metis fim homeomorphism_apply2 [OF homkh] image_subset_iff inj_onD injf)
+      show "(h \<circ> f) ` S \<subseteq> U"
+        using \<open>V' \<subseteq> U\<close> hfV' by auto
+      qed (auto simp: assms)
+    ultimately show "openin (subtopology euclidean V') ((h \<circ> f) ` S)"
+      using openin_subset_trans \<open>V' \<subseteq> U\<close> by force
+  qed
+qed
+
+corollary invariance_of_dimension_subspaces:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes ope: "openin (subtopology euclidean U) S"
+      and "subspace U" "subspace V"
+      and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+      and injf: "inj_on f S" and "S \<noteq> {}"
+    shows "dim U \<le> dim V"
+proof -
+  have "False" if "dim V < dim U"
+  proof -
+    obtain T where "subspace T" "T \<subseteq> U" "dim T = dim V"
+      using choose_subspace_of_subspace [of "dim V" U]
+      by (metis span_eq \<open>subspace U\<close> \<open>dim V < dim U\<close> linear not_le)
+    then have "V homeomorphic T"
+      by (simp add: \<open>subspace V\<close> homeomorphic_subspaces)
+    then obtain h k where homhk: "homeomorphism V T h k"
+      using homeomorphic_def  by blast
+    have "continuous_on S (h \<circ> f)"
+      by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_cont1 homhk)
+    moreover have "(h \<circ> f) ` S \<subseteq> U"
+      using \<open>T \<subseteq> U\<close> fim homeomorphism_image1 homhk by fastforce
+    moreover have "inj_on (h \<circ> f) S"
+      apply (clarsimp simp: inj_on_def)
+      by (metis fim homeomorphism_apply1 homhk image_subset_iff inj_onD injf)
+    ultimately have ope_hf: "openin (subtopology euclidean U) ((h \<circ> f) ` S)"
+      using invariance_of_domain_subspaces [OF ope \<open>subspace U\<close> \<open>subspace U\<close>] by auto
+    have "(h \<circ> f) ` S \<subseteq> T"
+      using fim homeomorphism_image1 homhk by fastforce
+    then show ?thesis
+      by (metis dim_openin \<open>dim T = dim V\<close> ope_hf \<open>subspace U\<close> \<open>S \<noteq> {}\<close> dim_subset image_is_empty not_le that)
+  qed
+  then show ?thesis
+    using not_less by blast
+qed
+
+corollary invariance_of_domain_affine_sets:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes ope: "openin (subtopology euclidean U) S"
+      and aff: "affine U" "affine V" "aff_dim V \<le> aff_dim U"
+      and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+      and injf: "inj_on f S"
+    shows "openin (subtopology euclidean V) (f ` S)"
+proof (cases "S = {}")
+  case True
+  then show ?thesis by auto
+next
+  case False
+  obtain a b where "a \<in> S" "a \<in> U" "b \<in> V"
+    using False fim ope openin_contains_cball by fastforce
+  have "openin (subtopology euclidean (op + (- b) ` V)) ((op + (- b) \<circ> f \<circ> op + a) ` op + (- a) ` S)"
+  proof (rule invariance_of_domain_subspaces)
+    show "openin (subtopology euclidean (op + (- a) ` U)) (op + (- a) ` S)"
+      by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois)
+    show "subspace (op + (- a) ` U)"
+      by (simp add: \<open>a \<in> U\<close> affine_diffs_subspace \<open>affine U\<close>)
+    show "subspace (op + (- b) ` V)"
+      by (simp add: \<open>b \<in> V\<close> affine_diffs_subspace \<open>affine V\<close>)
+    show "dim (op + (- b) ` V) \<le> dim (op + (- a) ` U)"
+      by (metis \<open>a \<in> U\<close> \<open>b \<in> V\<close> aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
+    show "continuous_on (op + (- a) ` S) (op + (- b) \<circ> f \<circ> op + a)"
+      by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
+    show "(op + (- b) \<circ> f \<circ> op + a) ` op + (- a) ` S \<subseteq> op + (- b) ` V"
+      using fim by auto
+    show "inj_on (op + (- b) \<circ> f \<circ> op + a) (op + (- a) ` S)"
+      by (auto simp: inj_on_def) (meson inj_onD injf)
+  qed
+  then show ?thesis
+    by (metis (no_types, lifting) homeomorphism_imp_open_map homeomorphism_translation image_comp translation_galois)
+qed
+
+corollary invariance_of_dimension_affine_sets:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes ope: "openin (subtopology euclidean U) S"
+      and aff: "affine U" "affine V"
+      and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+      and injf: "inj_on f S" and "S \<noteq> {}"
+    shows "aff_dim U \<le> aff_dim V"
+proof -
+  obtain a b where "a \<in> S" "a \<in> U" "b \<in> V"
+    using \<open>S \<noteq> {}\<close> fim ope openin_contains_cball by fastforce
+  have "dim (op + (- a) ` U) \<le> dim (op + (- b) ` V)"
+  proof (rule invariance_of_dimension_subspaces)
+    show "openin (subtopology euclidean (op + (- a) ` U)) (op + (- a) ` S)"
+      by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois)
+    show "subspace (op + (- a) ` U)"
+      by (simp add: \<open>a \<in> U\<close> affine_diffs_subspace \<open>affine U\<close>)
+    show "subspace (op + (- b) ` V)"
+      by (simp add: \<open>b \<in> V\<close> affine_diffs_subspace \<open>affine V\<close>)
+    show "continuous_on (op + (- a) ` S) (op + (- b) \<circ> f \<circ> op + a)"
+      by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
+    show "(op + (- b) \<circ> f \<circ> op + a) ` op + (- a) ` S \<subseteq> op + (- b) ` V"
+      using fim by auto
+    show "inj_on (op + (- b) \<circ> f \<circ> op + a) (op + (- a) ` S)"
+      by (auto simp: inj_on_def) (meson inj_onD injf)
+  qed (use \<open>S \<noteq> {}\<close> in auto)
+  then show ?thesis
+    by (metis \<open>a \<in> U\<close> \<open>b \<in> V\<close> aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
+qed
+
+corollary invariance_of_dimension:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes contf: "continuous_on S f" and "open S"
+      and injf: "inj_on f S" and "S \<noteq> {}"
+    shows "DIM('a) \<le> DIM('b)"
+  using invariance_of_dimension_subspaces [of UNIV S UNIV f] assms
+  by auto
+
+
+corollary continuous_injective_image_subspace_dim_le:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "subspace S" "subspace T"
+      and contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
+      and injf: "inj_on f S"
+    shows "dim S \<le> dim T"
+  apply (rule invariance_of_dimension_subspaces [of S S _ f])
+  using assms by (auto simp: subspace_affine)
+
+lemma invariance_of_dimension_convex_domain:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "convex S"
+      and contf: "continuous_on S f" and fim: "f ` S \<subseteq> affine hull T"
+      and injf: "inj_on f S"
+    shows "aff_dim S \<le> aff_dim T"
+proof (cases "S = {}")
+  case True
+  then show ?thesis by (simp add: aff_dim_geq)
+next
+  case False
+  have "aff_dim (affine hull S) \<le> aff_dim (affine hull T)"
+  proof (rule invariance_of_dimension_affine_sets)
+    show "openin (subtopology euclidean (affine hull S)) (rel_interior S)"
+      by (simp add: openin_rel_interior)
+    show "continuous_on (rel_interior S) f"
+      using contf continuous_on_subset rel_interior_subset by blast
+    show "f ` rel_interior S \<subseteq> affine hull T"
+      using fim rel_interior_subset by blast
+    show "inj_on f (rel_interior S)"
+      using inj_on_subset injf rel_interior_subset by blast
+    show "rel_interior S \<noteq> {}"
+      by (simp add: False \<open>convex S\<close> rel_interior_eq_empty)
+  qed auto
+  then show ?thesis
+    by simp
+qed
+
+
+lemma homeomorphic_convex_sets_le:
+  assumes "convex S" "S homeomorphic T"
+  shows "aff_dim S \<le> aff_dim T"
+proof -
+  obtain h k where homhk: "homeomorphism S T h k"
+    using homeomorphic_def assms  by blast
+  show ?thesis
+  proof (rule invariance_of_dimension_convex_domain [OF \<open>convex S\<close>])
+    show "continuous_on S h"
+      using homeomorphism_def homhk by blast
+    show "h ` S \<subseteq> affine hull T"
+      by (metis homeomorphism_def homhk hull_subset)
+    show "inj_on h S"
+      by (meson homeomorphism_apply1 homhk inj_on_inverseI)
+  qed
+qed
+
+lemma homeomorphic_convex_sets:
+  assumes "convex S" "convex T" "S homeomorphic T"
+  shows "aff_dim S = aff_dim T"
+  by (meson assms dual_order.antisym homeomorphic_convex_sets_le homeomorphic_sym)
+
+lemma homeomorphic_convex_compact_sets_eq:
+  assumes "convex S" "compact S" "convex T" "compact T"
+  shows "S homeomorphic T \<longleftrightarrow> aff_dim S = aff_dim T"
+  by (meson assms homeomorphic_convex_compact_sets homeomorphic_convex_sets)
+
+lemma invariance_of_domain_gen:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "open S" "continuous_on S f" "inj_on f S" "DIM('b) \<le> DIM('a)"
+    shows "open(f ` S)"
+  using invariance_of_domain_subspaces [of UNIV S UNIV f] assms by auto
+
+lemma injective_into_1d_imp_open_map_UNIV:
+  fixes f :: "'a::euclidean_space \<Rightarrow> real"
+  assumes "open T" "continuous_on S f" "inj_on f S" "T \<subseteq> S"
+    shows "open (f ` T)"
+  apply (rule invariance_of_domain_gen [OF \<open>open T\<close>])
+  using assms apply (auto simp: elim: continuous_on_subset subset_inj_on)
+  done
+
+lemma continuous_on_inverse_open:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" and gf: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
+    shows "continuous_on (f ` S) g"
+proof (clarsimp simp add: continuous_openin_preimage_eq)
+  fix T :: "'a set"
+  assume "open T"
+  have eq: "{x. x \<in> f ` S \<and> g x \<in> T} = f ` (S \<inter> T)"
+    by (auto simp: gf)
+  show "openin (subtopology euclidean (f ` S)) {x \<in> f ` S. g x \<in> T}"
+    apply (subst eq)
+    apply (rule open_openin_trans)
+      apply (rule invariance_of_domain_gen)
+    using assms
+         apply auto
+    using inj_on_inverseI apply auto[1]
+    by (metis \<open>open T\<close> continuous_on_subset inj_onI inj_on_subset invariance_of_domain_gen openin_open openin_open_eq)
+qed
+
+lemma invariance_of_domain_homeomorphism:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" "inj_on f S"
+  obtains g where "homeomorphism S (f ` S) f g"
+proof
+  show "homeomorphism S (f ` S) f (inv_into S f)"
+    by (simp add: assms continuous_on_inverse_open homeomorphism_def)
+qed
+
+corollary invariance_of_domain_homeomorphic:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" "inj_on f S"
+  shows "S homeomorphic (f ` S)"
+  using invariance_of_domain_homeomorphism [OF assms]
+  by (meson homeomorphic_def)
+
 end
diff -r f2c8f6b11dcf -r 74fde524799e src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Sun Oct 09 16:27:01 2016 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Mon Oct 10 15:45:41 2016 +0100
@@ -2178,7 +2178,7 @@
 
 text \<open>More lemmas about dimension.\<close>
 
-lemma dim_UNIV: "dim (UNIV :: 'a::euclidean_space set) = DIM('a)"
+lemma dim_UNIV [simp]: "dim (UNIV :: 'a::euclidean_space set) = DIM('a)"
   using independent_Basis
   by (intro dim_unique[of Basis]) auto
 
diff -r f2c8f6b11dcf -r 74fde524799e src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Sun Oct 09 16:27:01 2016 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy	Mon Oct 10 15:45:41 2016 +0100
@@ -1261,8 +1261,90 @@
   using midpoints_in_convex_hull segment_convex_hull by blast
 
 lemma midpoint_in_open_segment [simp]: "midpoint a b \<in> open_segment a b \<longleftrightarrow> a \<noteq> b"
-  by (simp add: midpoint_eq_endpoint(1) midpoint_eq_endpoint(2) open_segment_def)
-
+  by (simp add: open_segment_def)
+
+lemma continuous_IVT_local_extremum:
+  fixes f :: "'a::euclidean_space \<Rightarrow> real"
+  assumes contf: "continuous_on (closed_segment a b) f"
+      and "a \<noteq> b" "f a = f b"
+  obtains z where "z \<in> open_segment a b"
+                  "(\<forall>w \<in> closed_segment a b. (f w) \<le> (f z)) \<or>
+                   (\<forall>w \<in> closed_segment a b. (f z) \<le> (f w))"
+proof -
+  obtain c where "c \<in> closed_segment a b" and c: "\<And>y. y \<in> closed_segment a b \<Longrightarrow> f y \<le> f c"
+    using continuous_attains_sup [of "closed_segment a b" f] contf by auto
+  obtain d where "d \<in> closed_segment a b" and d: "\<And>y. y \<in> closed_segment a b \<Longrightarrow> f d \<le> f y"
+    using continuous_attains_inf [of "closed_segment a b" f] contf by auto
+  show ?thesis
+  proof (cases "c \<in> open_segment a b \<or> d \<in> open_segment a b")
+    case True
+    then show ?thesis
+      using c d that by blast
+  next
+    case False
+    then have "(c = a \<or> c = b) \<and> (d = a \<or> d = b)"
+      by (simp add: \<open>c \<in> closed_segment a b\<close> \<open>d \<in> closed_segment a b\<close> open_segment_def)
+    with \<open>a \<noteq> b\<close> \<open>f a = f b\<close> c d show ?thesis
+      by (rule_tac z = "midpoint a b" in that) (fastforce+)
+  qed
+qed
+
+text\<open>An injective map into R is also an open map w.r.T. the universe, and conversely. \<close>
+proposition injective_eq_1d_open_map_UNIV:
+  fixes f :: "real \<Rightarrow> real"
+  assumes contf: "continuous_on S f" and S: "is_interval S"
+    shows "inj_on f S \<longleftrightarrow> (\<forall>T. open T \<and> T \<subseteq> S \<longrightarrow> open(f ` T))"
+          (is "?lhs = ?rhs")
+proof safe
+  fix T
+  assume injf: ?lhs and "open T" and "T \<subseteq> S"
+  have "\<exists>U. open U \<and> f x \<in> U \<and> U \<subseteq> f ` T" if "x \<in> T" for x
+  proof -
+    obtain \<delta> where "\<delta> > 0" and \<delta>: "cball x \<delta> \<subseteq> T"
+      using \<open>open T\<close> \<open>x \<in> T\<close> open_contains_cball_eq by blast
+    show ?thesis
+    proof (intro exI conjI)
+      have "closed_segment (x-\<delta>) (x+\<delta>) = {x-\<delta>..x+\<delta>}"
+        using \<open>0 < \<delta>\<close> by (auto simp: closed_segment_eq_real_ivl)
+      also have "... \<subseteq> S"
+        using \<delta> \<open>T \<subseteq> S\<close> by (auto simp: dist_norm subset_eq)
+      finally have "f ` (open_segment (x-\<delta>) (x+\<delta>)) = open_segment (f (x-\<delta>)) (f (x+\<delta>))"
+        using continuous_injective_image_open_segment_1
+        by (metis continuous_on_subset [OF contf] inj_on_subset [OF injf])
+      then show "open (f ` {x-\<delta><..<x+\<delta>})"
+        using \<open>0 < \<delta>\<close> by (simp add: open_segment_eq_real_ivl)
+      show "f x \<in> f ` {x - \<delta><..<x + \<delta>}"
+        by (auto simp: \<open>\<delta> > 0\<close>)
+      show "f ` {x - \<delta><..<x + \<delta>} \<subseteq> f ` T"
+        using \<delta> by (auto simp: dist_norm subset_iff)
+    qed
+  qed
+  with open_subopen show "open (f ` T)"
+    by blast
+next
+  assume R: ?rhs
+  have False if xy: "x \<in> S" "y \<in> S" and "f x = f y" "x \<noteq> y" for x y
+  proof -
+    have "open (f ` open_segment x y)"
+      using R
+      by (metis S convex_contains_open_segment is_interval_convex open_greaterThanLessThan open_segment_eq_real_ivl xy)
+    moreover
+    have "continuous_on (closed_segment x y) f"
+      by (meson S closed_segment_subset contf continuous_on_subset is_interval_convex that)
+    then obtain \<xi> where "\<xi> \<in> open_segment x y"
+                    and \<xi>: "(\<forall>w \<in> closed_segment x y. (f w) \<le> (f \<xi>)) \<or>
+                            (\<forall>w \<in> closed_segment x y. (f \<xi>) \<le> (f w))"
+      using continuous_IVT_local_extremum [of x y f] \<open>f x = f y\<close> \<open>x \<noteq> y\<close> by blast
+    ultimately obtain e where "e>0" and e: "\<And>u. dist u (f \<xi>) < e \<Longrightarrow> u \<in> f ` open_segment x y"
+      using open_dist by (metis image_eqI)
+    have fin: "f \<xi> + (e/2) \<in> f ` open_segment x y" "f \<xi> - (e/2) \<in> f ` open_segment x y"
+      using e [of "f \<xi> + (e/2)"] e [of "f \<xi> - (e/2)"] \<open>e > 0\<close> by (auto simp: dist_norm)
+    show ?thesis
+      using \<xi> \<open>0 < e\<close> fin open_closed_segment by fastforce
+  qed
+  then show ?lhs
+    by (force simp: inj_on_def)
+qed
 
 subsection \<open>Bounding a point away from a path\<close>
 
@@ -2319,9 +2401,10 @@
   by (metis cobounded_unique_unbounded_component)
 
 lemma cobounded_has_bounded_component:
-    fixes s :: "'a :: euclidean_space set"
-    shows "\<lbrakk>bounded (- s); ~connected s; 2 \<le> DIM('a)\<rbrakk> \<Longrightarrow> \<exists>c. c \<in> components s \<and> bounded c"
-  by (meson cobounded_unique_unbounded_components connected_eq_connected_components_eq)
+  fixes S :: "'a :: euclidean_space set"
+  assumes "bounded (- S)" "\<not> connected S" "2 \<le> DIM('a)"
+  obtains C where "C \<in> components S" "bounded C"
+  by (meson cobounded_unique_unbounded_components connected_eq_connected_components_eq assms)
 
 
 section\<open>The "inside" and "outside" of a set\<close>
@@ -7510,7 +7593,7 @@
     have hUS: "h ` U \<subseteq> h ` S"
       by (meson homeomorphism_imp_open_map homeomorphism_of_subsets homhj hull_subset opeS opeU open_UNIV openin_open_eq)
     have op: "openin (subtopology euclidean (affine hull S)) U \<Longrightarrow> open (h ` U)" for U
-      using homeomorphism_imp_open_map [OF homhj]  by (simp add: open_openin)
+      using homeomorphism_imp_open_map [OF homhj]  by simp
     have "open (h ` U)" "open (h ` S)"
       by (auto intro: opeS opeU openin_trans op)
     then obtain f g where hom: "homeomorphism (h ` T) (h ` T) f g"
diff -r f2c8f6b11dcf -r 74fde524799e src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Oct 09 16:27:01 2016 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Oct 10 15:45:41 2016 +0100
@@ -18,6 +18,11 @@
 
 (* FIXME: move elsewhere *)
 
+lemma Times_eq_image_sum:
+  fixes S :: "'a :: comm_monoid_add set" and T :: "'b :: comm_monoid_add set"
+  shows "S \<times> T = {u + v |u v. u \<in> (\<lambda>x. (x, 0)) ` S \<and> v \<in> Pair 0 ` T}"
+  by force
+
 lemma halfspace_Int_eq:
      "{x. a \<bullet> x \<le> b} \<inter> {x. b \<le> a \<bullet> x} = {x. a \<bullet> x = b}"
      "{x. b \<le> a \<bullet> x} \<inter> {x. a \<bullet> x \<le> b} = {x. a \<bullet> x = b}"
@@ -730,20 +735,19 @@
   apply (auto simp add: istopology_def)
   done
 
+declare open_openin [symmetric, simp]
+
 lemma topspace_euclidean [simp]: "topspace euclidean = UNIV"
-  apply (simp add: topspace_def)
-  apply (rule set_eqI)
-  apply (auto simp add: open_openin[symmetric])
-  done
+  by (force simp add: topspace_def)
 
 lemma topspace_euclidean_subtopology[simp]: "topspace (subtopology euclidean S) = S"
-  by (simp add: topspace_euclidean topspace_subtopology)
+  by (simp add: topspace_subtopology)
 
 lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S"
-  by (simp add: closed_def closedin_def topspace_euclidean open_openin Compl_eq_Diff_UNIV)
+  by (simp add: closed_def closedin_def Compl_eq_Diff_UNIV)
 
 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])
+  using openI by auto
 
 lemma openin_subtopology_self [simp]: "openin (subtopology euclidean S) S"
   by (metis openin_topspace topspace_euclidean_subtopology)
@@ -751,7 +755,7 @@
 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))"
-  by (auto simp add: openin_subtopology open_openin[symmetric])
+  by (auto simp add: openin_subtopology)
 
 lemma openin_Int_open:
    "\<lbrakk>openin (subtopology euclidean U) S; open T\<rbrakk>
@@ -1968,7 +1972,7 @@
 lemma closure_UNIV [simp]: "closure UNIV = UNIV"
   using closed_UNIV by (rule closure_closed)
 
-lemma closure_union [simp]: "closure (S \<union> T) = closure S \<union> closure T"
+lemma closure_Un [simp]: "closure (S \<union> T) = closure S \<union> closure T"
   unfolding closure_interior by simp
 
 lemma closure_eq_empty [iff]: "closure S = {} \<longleftrightarrow> S = {}"
@@ -2084,6 +2088,71 @@
      \<Longrightarrow> openin (subtopology euclidean T) S"
   by (auto simp: openin_open)
 
+lemma openin_Times:
+   "\<lbrakk>openin (subtopology euclidean S) S'; openin (subtopology euclidean T) T'\<rbrakk>
+    \<Longrightarrow> openin (subtopology euclidean (S \<times> T)) (S' \<times> T')"
+  unfolding openin_open using open_Times by blast
+
+lemma Times_in_interior_subtopology:
+  fixes U :: "('a::metric_space * 'b::metric_space) set"
+  assumes "(x, y) \<in> U" "openin (subtopology euclidean (S \<times> T)) U"
+  obtains V W where "openin (subtopology euclidean S) V" "x \<in> V"
+                    "openin (subtopology euclidean T) W" "y \<in> W" "(V \<times> W) \<subseteq> U"
+proof -
+  from assms obtain e where "e > 0" and "U \<subseteq> S \<times> T"
+                and e: "\<And>x' y'. \<lbrakk>x'\<in>S; y'\<in>T; dist (x', y') (x, y) < e\<rbrakk> \<Longrightarrow> (x', y') \<in> U"
+    by (force simp: openin_euclidean_subtopology_iff)
+  with assms have "x \<in> S" "y \<in> T"
+    by auto
+  show ?thesis
+  proof
+    show "openin (subtopology euclidean S) (ball x (e/2) \<inter> S)"
+      by (simp add: Int_commute openin_open_Int)
+    show "x \<in> ball x (e / 2) \<inter> S"
+      by (simp add: \<open>0 < e\<close> \<open>x \<in> S\<close>)
+    show "openin (subtopology euclidean T) (ball y (e/2) \<inter> T)"
+      by (simp add: Int_commute openin_open_Int)
+    show "y \<in> ball y (e / 2) \<inter> T"
+      by (simp add: \<open>0 < e\<close> \<open>y \<in> T\<close>)
+    show "(ball x (e / 2) \<inter> S) \<times> (ball y (e / 2) \<inter> T) \<subseteq> U"
+      by clarify (simp add: e dist_Pair_Pair \<open>0 < e\<close> dist_commute sqrt_sum_squares_half_less)
+  qed
+qed
+
+lemma openin_Times_eq:
+  fixes S :: "'a::metric_space set" and T :: "'b::metric_space set"
+  shows
+   "openin (subtopology euclidean (S \<times> T)) (S' \<times> T') \<longleftrightarrow>
+    (S' = {} \<or> T' = {} \<or>
+     openin (subtopology euclidean S) S' \<and> openin (subtopology euclidean T) T')"
+    (is "?lhs = ?rhs")
+proof (cases "S' = {} \<or> T' = {}")
+  case True
+  then show ?thesis by auto
+next
+  case False
+  then obtain x y where "x \<in> S'" "y \<in> T'"
+    by blast
+  show ?thesis
+  proof
+    assume L: ?lhs
+    have "openin (subtopology euclidean S) S'"
+      apply (subst openin_subopen, clarify)
+      apply (rule Times_in_interior_subtopology [OF _ L])
+      using \<open>y \<in> T'\<close> by auto
+    moreover have "openin (subtopology euclidean T) T'"
+      apply (subst openin_subopen, clarify)
+      apply (rule Times_in_interior_subtopology [OF _ L])
+      using \<open>x \<in> S'\<close> by auto
+    ultimately show ?rhs
+      by simp
+  next
+    assume ?rhs
+    with False show ?lhs
+      by (simp add: openin_Times)
+  qed
+qed
+
 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')"
@@ -8502,7 +8571,7 @@
 proof -
   from gt_ex obtain b where "a < b" by auto
   hence "{a<..} = {a<..<b} \<union> {b..}" by auto
-  also have "closure \<dots> = {a..}" using \<open>a < b\<close> unfolding closure_union
+  also have "closure \<dots> = {a..}" using \<open>a < b\<close> unfolding closure_Un
     by auto
   finally show ?thesis .
 qed
@@ -8513,7 +8582,7 @@
 proof -
   from lt_ex obtain a where "a < b" by auto
   hence "{..<b} = {a<..<b} \<union> {..a}" by auto
-  also have "closure \<dots> = {..b}" using \<open>a < b\<close> unfolding closure_union
+  also have "closure \<dots> = {..b}" using \<open>a < b\<close> unfolding closure_Un
     by auto
   finally show ?thesis .
 qed
@@ -8524,7 +8593,7 @@
   shows "closure {a ..< b} = {a .. b}"
 proof -
   from assms have "{a ..< b} = {a} \<union> {a <..< b}" by auto
-  also have "closure \<dots> = {a .. b}" unfolding closure_union
+  also have "closure \<dots> = {a .. b}" unfolding closure_Un
     by (auto simp add: assms less_imp_le)
   finally show ?thesis .
 qed
@@ -8535,7 +8604,7 @@
   shows "closure {a <.. b} = {a .. b}"
 proof -
   from assms have "{a <.. b} = {b} \<union> {a <..< b}" by auto
-  also have "closure \<dots> = {a .. b}" unfolding closure_union
+  also have "closure \<dots> = {a .. b}" unfolding closure_Un
     by (auto simp add: assms less_imp_le)
   finally show ?thesis .
 qed
diff -r f2c8f6b11dcf -r 74fde524799e src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Sun Oct 09 16:27:01 2016 +0200
+++ b/src/HOL/NthRoot.thy	Mon Oct 10 15:45:41 2016 +0100
@@ -692,15 +692,12 @@
   by (metis not_less not_less_iff_gr_or_eq numeral_less_iff real_sqrt_four
       real_sqrt_le_iff semiring_norm(75) semiring_norm(78) semiring_norm(85))
 
-
-text \<open>Needed for the infinitely close relation over the nonstandard complex numbers.\<close>
-lemma lemma_sqrt_hcomplex_capprox:
-  "0 < u \<Longrightarrow> x < u/2 \<Longrightarrow> y < u/2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) < u"
+lemma sqrt_sum_squares_half_less:
+  "x < u/2 \<Longrightarrow> y < u/2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) < u"
   apply (rule real_sqrt_sum_squares_less)
    apply (auto simp add: abs_if field_simps)
    apply (rule le_less_trans [where y = "x*2"])
-  using less_eq_real_def sqrt2_less_2
-    apply force
+  using less_eq_real_def sqrt2_less_2 apply force
    apply assumption
   apply (rule le_less_trans [where y = "y*2"])
   using less_eq_real_def sqrt2_less_2 mult_le_cancel_left