# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1509458359 0
# Node ID 289f390c4e578eb2e04d76573ca2fc152b5cb76a
# Parent  0230af0f3c590e728a27df19c8c5add4563e881a
A few more topological results. And made some slow proofs faster

diff -r 0230af0f3c59 -r 289f390c4e57 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Tue Oct 31 07:11:03 2017 +0000
+++ b/src/HOL/Analysis/Further_Topology.thy	Tue Oct 31 13:59:19 2017 +0000
@@ -3799,7 +3799,7 @@
     by (simp add: Int_assoc openin_INT2 [OF \<open>finite C\<close> \<open>C \<noteq> {}\<close>])
   with xin obtain d2 where "d2>0"
               and d2: "\<And>u v. \<lbrakk>u \<in> S; dist u x < d2; v \<in> C\<rbrakk> \<Longrightarrow> f u \<inter> T \<inter> ball v (e/2) \<noteq> {}"
-    by (force simp: openin_euclidean_subtopology_iff)
+    unfolding openin_euclidean_subtopology_iff using xin by fastforce
   show ?thesis
   proof (intro that conjI ballI)
     show "0 < min d1 d2"
@@ -3827,7 +3827,7 @@
 qed
 
 
-subsection\<open>complex logs exist on various "well-behaved" sets\<close>
+subsection\<open>Complex logs exist on various "well-behaved" sets\<close>
 
 lemma continuous_logarithm_on_contractible:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
@@ -3838,7 +3838,7 @@
     using nullhomotopic_from_contractible assms
     by (metis imageE subset_Compl_singleton)
   then show ?thesis
-    by (metis inessential_eq_continuous_logarithm of_real_0 that)
+    by (metis inessential_eq_continuous_logarithm that)
 qed
 
 lemma continuous_logarithm_on_simply_connected:
@@ -3896,6 +3896,72 @@
 qed
 
 
+subsection\<open>Another simple case where sphere maps are nullhomotopic.\<close>
+
+lemma inessential_spheremap_2_aux:
+  fixes f :: "'a::euclidean_space \<Rightarrow> complex"
+  assumes 2: "2 < DIM('a)" and contf: "continuous_on (sphere a r) f" 
+      and fim: "f `(sphere a r) \<subseteq> (sphere 0 1)" 
+  obtains c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere 0 1) f (\<lambda>x. c)"
+proof -
+  obtain g where contg: "continuous_on (sphere a r) g" 
+             and feq: "\<And>x. x \<in> sphere a r \<Longrightarrow> f x = exp(g x)"
+  proof (rule continuous_logarithm_on_simply_connected [OF contf])
+    show "simply_connected (sphere a r)"
+      using 2 by (simp add: simply_connected_sphere_eq)
+    show "locally path_connected (sphere a r)"
+      by (simp add: locally_path_connected_sphere)
+    show "\<And>z.  z \<in> sphere a r \<Longrightarrow> f z \<noteq> 0"
+      using fim by force
+  qed auto
+  have "\<exists>g. continuous_on (sphere a r) g \<and> (\<forall>x\<in>sphere a r. f x = exp (\<i> * complex_of_real (g x)))"
+  proof (intro exI conjI)
+    show "continuous_on (sphere a r) (Im \<circ> g)"
+      by (intro contg continuous_intros continuous_on_compose)
+    show "\<forall>x\<in>sphere a r. f x = exp (\<i> * complex_of_real ((Im \<circ> g) x))"
+      using exp_eq_polar feq fim norm_exp_eq_Re by auto
+  qed
+  with inessential_eq_continuous_logarithm_circle that show ?thesis 
+    by metis
+qed
+
+lemma inessential_spheremap_2:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes a2: "2 < DIM('a)" and b2: "DIM('b) = 2" 
+      and contf: "continuous_on (sphere a r) f" and fim: "f `(sphere a r) \<subseteq> (sphere b s)"
+  obtains c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. c)"
+proof (cases "s \<le> 0")
+  case True
+  then show ?thesis
+    using contf contractible_sphere fim nullhomotopic_into_contractible that by blast
+next
+  case False
+  then have "sphere b s homeomorphic sphere (0::complex) 1"
+    using assms by (simp add: homeomorphic_spheres_gen)
+  then obtain h k where hk: "homeomorphism (sphere b s) (sphere (0::complex) 1) h k"
+    by (auto simp: homeomorphic_def)
+  then have conth: "continuous_on (sphere b s) h"
+       and  contk: "continuous_on (sphere 0 1) k"
+       and  him: "h ` sphere b s \<subseteq> sphere 0 1"
+       and  kim: "k ` sphere 0 1 \<subseteq> sphere b s"
+    by (simp_all add: homeomorphism_def)
+  obtain c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere 0 1) (h \<circ> f) (\<lambda>x. c)"
+  proof (rule inessential_spheremap_2_aux [OF a2])
+    show "continuous_on (sphere a r) (h \<circ> f)"
+      by (meson continuous_on_compose [OF contf] conth continuous_on_subset fim)
+    show "(h \<circ> f) ` sphere a r \<subseteq> sphere 0 1"
+      using fim him by force
+  qed auto
+  then have "homotopic_with (\<lambda>f. True) (sphere a r) (sphere b s) (k \<circ> (h \<circ> f)) (k \<circ> (\<lambda>x. c))"
+    by (rule homotopic_compose_continuous_left [OF _ contk kim])
+  then have "homotopic_with (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. k c)"
+    apply (rule homotopic_with_eq, auto)
+    by (metis fim hk homeomorphism_def image_subset_iff mem_sphere)
+  then show ?thesis
+    by (metis that)
+qed
+
+
 subsection\<open>Holomorphic logarithms and square roots.\<close>
 
 lemma contractible_imp_holomorphic_log:
diff -r 0230af0f3c59 -r 289f390c4e57 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Tue Oct 31 07:11:03 2017 +0000
+++ b/src/HOL/Analysis/Path_Connected.thy	Tue Oct 31 13:59:19 2017 +0000
@@ -4864,7 +4864,7 @@
   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)
+  using assms unfolding locally_def by meson
 
 lemma locally_mono:
   assumes "locally P S" "\<And>t. P t \<Longrightarrow> Q t"
@@ -4981,7 +4981,7 @@
   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
+    using \<open>f ` v \<subseteq> W\<close> \<open>W \<subseteq> t\<close> continuous_on_subset [OF 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)
@@ -5903,7 +5903,7 @@
     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)
+      using in_components_subset by auto
     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