# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1477409413 -3600
# Node ID 3f4a86c9d2b54cf760c9e2ce0dbbd0946c25a082
# Parent  6b57eb9e779052c5ec6b6b4fe14f3521f4fe4845
more new material

diff -r 6b57eb9e7790 -r 3f4a86c9d2b5 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Tue Oct 25 15:48:31 2016 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy	Tue Oct 25 16:30:13 2016 +0100
@@ -2732,6 +2732,254 @@
     using clopen [of S] False  by simp
 qed
 
+subsection\<open> Dimension-based conditions for various homeomorphisms.\<close>
+
+lemma homeomorphic_subspaces_eq:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "subspace S" "subspace T"
+  shows "S homeomorphic T \<longleftrightarrow> dim S = dim T"
+proof
+  assume "S homeomorphic T"
+  then obtain f g where hom: "homeomorphism S T f g"
+    using homeomorphic_def by blast
+  show "dim S = dim T"
+  proof (rule order_antisym)
+    show "dim S \<le> dim T"
+      by (metis assms dual_order.refl inj_onI homeomorphism_cont1 [OF hom] homeomorphism_apply1 [OF hom] homeomorphism_image1 [OF hom] continuous_injective_image_subspace_dim_le)
+    show "dim T \<le> dim S"
+      by (metis assms dual_order.refl inj_onI homeomorphism_cont2 [OF hom] homeomorphism_apply2 [OF hom] homeomorphism_image2 [OF hom] continuous_injective_image_subspace_dim_le)
+  qed
+next
+  assume "dim S = dim T"
+  then show "S homeomorphic T"
+    by (simp add: assms homeomorphic_subspaces)
+qed
+
+lemma homeomorphic_affine_sets_eq:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "affine S" "affine T"
+  shows "S homeomorphic T \<longleftrightarrow> aff_dim S = aff_dim T"
+proof (cases "S = {} \<or> T = {}")
+  case True
+  then show ?thesis
+    using assms homeomorphic_affine_sets by force
+next
+  case False
+  then obtain a b where "a \<in> S" "b \<in> T"
+    by blast
+  then have "subspace (op + (- a) ` S)" "subspace (op + (- b) ` T)"
+    using affine_diffs_subspace assms by blast+
+  then show ?thesis
+    by (metis affine_imp_convex assms homeomorphic_affine_sets homeomorphic_convex_sets)
+qed
+
+lemma homeomorphic_hyperplanes_eq:
+  fixes a :: "'a::euclidean_space" and c :: "'b::euclidean_space"
+  assumes "a \<noteq> 0" "c \<noteq> 0"
+  shows "({x. a \<bullet> x = b} homeomorphic {x. c \<bullet> x = d} \<longleftrightarrow> DIM('a) = DIM('b))"
+  apply (auto simp: homeomorphic_affine_sets_eq affine_hyperplane assms)
+  by (metis DIM_positive Suc_pred)
+
+lemma homeomorphic_UNIV_UNIV:
+  shows "(UNIV::'a set) homeomorphic (UNIV::'b set) \<longleftrightarrow>
+    DIM('a::euclidean_space) = DIM('b::euclidean_space)"
+  by (simp add: homeomorphic_subspaces_eq)
+
+lemma simply_connected_sphere_gen:
+   assumes "convex S" "bounded S" and 3: "3 \<le> aff_dim S"
+   shows "simply_connected(rel_frontier S)"
+proof -
+  have pa: "path_connected (rel_frontier S)"
+    using assms by (simp add: path_connected_sphere_gen)
+  show ?thesis
+  proof (clarsimp simp add: simply_connected_eq_contractible_circlemap pa)
+    fix f
+    assume f: "continuous_on (sphere (0::complex) 1) f" "f ` sphere 0 1 \<subseteq> rel_frontier S"
+    have eq: "sphere (0::complex) 1 = rel_frontier(cball 0 1)"
+      by simp
+    have "convex (cball (0::complex) 1)"
+      by (rule convex_cball)
+    then obtain c where "homotopic_with (\<lambda>z. True) (sphere (0::complex) 1) (rel_frontier S) f (\<lambda>x. c)"
+      apply (rule inessential_spheremap_lowdim_gen [OF _ bounded_cball \<open>convex S\<close> \<open>bounded S\<close>, where f=f])
+      using f 3
+         apply (auto simp: aff_dim_cball)
+      done
+    then show "\<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) (rel_frontier S) f (\<lambda>x. a)"
+      by blast
+  qed
+qed
+
+subsection\<open>more invariance of domain\<close>
+
+proposition invariance_of_domain_sphere_affine_set_gen:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
+      and U: "bounded U" "convex U"
+      and "affine T" and affTU: "aff_dim T < aff_dim U"
+      and ope: "openin (subtopology euclidean (rel_frontier U)) S"
+   shows "openin (subtopology euclidean T) (f ` S)"
+proof (cases "rel_frontier U = {}")
+  case True
+  then show ?thesis
+    using ope openin_subset by force
+next
+  case False
+  obtain b c where b: "b \<in> rel_frontier U" and c: "c \<in> rel_frontier U" and "b \<noteq> c"
+    using \<open>bounded U\<close> rel_frontier_not_sing [of U] subset_singletonD False  by fastforce
+  obtain V :: "'a set" where "affine V" and affV: "aff_dim V = aff_dim U - 1"
+  proof (rule choose_affine_subset [OF affine_UNIV])
+    show "- 1 \<le> aff_dim U - 1"
+      by (metis aff_dim_empty aff_dim_geq aff_dim_negative_iff affTU diff_0 diff_right_mono not_le)
+    show "aff_dim U - 1 \<le> aff_dim (UNIV::'a set)"
+      by (metis aff_dim_UNIV aff_dim_le_DIM le_cases not_le zle_diff1_eq)
+  qed auto
+  have SU: "S \<subseteq> rel_frontier U"
+    using ope openin_imp_subset by auto
+  have homb: "rel_frontier U - {b} homeomorphic V"
+   and homc: "rel_frontier U - {c} homeomorphic V"
+    using homeomorphic_punctured_sphere_affine_gen [of U _ V]
+    by (simp_all add: \<open>affine V\<close> affV U b c)
+  then obtain g h j k
+           where gh: "homeomorphism (rel_frontier U - {b}) V g h"
+             and jk: "homeomorphism (rel_frontier U - {c}) V j k"
+    by (auto simp: homeomorphic_def)
+  with SU have hgsub: "(h ` g ` (S - {b})) \<subseteq> S" and kjsub: "(k ` j ` (S - {c})) \<subseteq> S"
+    by (simp_all add: homeomorphism_def subset_eq)
+  have [simp]: "aff_dim T \<le> aff_dim V"
+    by (simp add: affTU affV)
+  have "openin (subtopology euclidean T) ((f \<circ> h) ` g ` (S - {b}))"
+  proof (rule invariance_of_domain_affine_sets [OF _ \<open>affine V\<close>])
+    show "openin (subtopology euclidean V) (g ` (S - {b}))"
+      apply (rule homeomorphism_imp_open_map [OF gh])
+      by (meson Diff_mono Diff_subset SU ope openin_delete openin_subset_trans order_refl)
+    show "continuous_on (g ` (S - {b})) (f \<circ> h)"
+       apply (rule continuous_on_compose)
+        apply (meson Diff_mono SU homeomorphism_def homeomorphism_of_subsets gh set_eq_subset)
+      using contf continuous_on_subset hgsub by blast
+    show "inj_on (f \<circ> h) (g ` (S - {b}))"
+      using kjsub
+      apply (clarsimp simp add: inj_on_def)
+      by (metis SU b homeomorphism_def inj_onD injf insert_Diff insert_iff gh rev_subsetD)
+    show "(f \<circ> h) ` g ` (S - {b}) \<subseteq> T"
+      by (metis fim image_comp image_mono hgsub subset_trans)
+  qed (auto simp: assms)
+  moreover
+  have "openin (subtopology euclidean T) ((f \<circ> k) ` j ` (S - {c}))"
+  proof (rule invariance_of_domain_affine_sets [OF _ \<open>affine V\<close>])
+    show "openin (subtopology euclidean V) (j ` (S - {c}))"
+      apply (rule homeomorphism_imp_open_map [OF jk])
+      by (meson Diff_mono Diff_subset SU ope openin_delete openin_subset_trans order_refl)
+    show "continuous_on (j ` (S - {c})) (f \<circ> k)"
+       apply (rule continuous_on_compose)
+        apply (meson Diff_mono SU homeomorphism_def homeomorphism_of_subsets jk set_eq_subset)
+      using contf continuous_on_subset kjsub by blast
+    show "inj_on (f \<circ> k) (j ` (S - {c}))"
+      using kjsub
+      apply (clarsimp simp add: inj_on_def)
+      by (metis SU c homeomorphism_def inj_onD injf insert_Diff insert_iff jk rev_subsetD)
+    show "(f \<circ> k) ` j ` (S - {c}) \<subseteq> T"
+      by (metis fim image_comp image_mono kjsub subset_trans)
+  qed (auto simp: assms)
+  ultimately have "openin (subtopology euclidean T) ((f \<circ> h) ` g ` (S - {b}) \<union> ((f \<circ> k) ` j ` (S - {c})))"
+    by (rule openin_Un)
+  moreover have "(f \<circ> h) ` g ` (S - {b}) = f ` (S - {b})"
+  proof -
+    have "h ` g ` (S - {b}) = (S - {b})"
+    proof
+      show "h ` g ` (S - {b}) \<subseteq> S - {b}"
+        using homeomorphism_apply1 [OF gh] SU
+        by (fastforce simp add: image_iff image_subset_iff)
+      show "S - {b} \<subseteq> h ` g ` (S - {b})"
+        apply clarify
+        by  (metis SU subsetD homeomorphism_apply1 [OF gh] image_iff member_remove remove_def)
+    qed
+    then show ?thesis
+      by (metis image_comp)
+  qed
+  moreover have "(f \<circ> k) ` j ` (S - {c}) = f ` (S - {c})"
+  proof -
+    have "k ` j ` (S - {c}) = (S - {c})"
+    proof
+      show "k ` j ` (S - {c}) \<subseteq> S - {c}"
+        using homeomorphism_apply1 [OF jk] SU
+        by (fastforce simp add: image_iff image_subset_iff)
+      show "S - {c} \<subseteq> k ` j ` (S - {c})"
+        apply clarify
+        by  (metis SU subsetD homeomorphism_apply1 [OF jk] image_iff member_remove remove_def)
+    qed
+    then show ?thesis
+      by (metis image_comp)
+  qed
+  moreover have "f ` (S - {b}) \<union> f ` (S - {c}) = f ` (S)"
+    using \<open>b \<noteq> c\<close> by blast
+  ultimately show ?thesis
+    by simp
+qed
+
+
+lemma invariance_of_domain_sphere_affine_set:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
+      and "r \<noteq> 0" "affine T" and affTU: "aff_dim T < DIM('a)"
+      and ope: "openin (subtopology euclidean (sphere a r)) S"
+   shows "openin (subtopology euclidean T) (f ` S)"
+proof (cases "sphere a r = {}")
+  case True
+  then show ?thesis
+    using ope openin_subset by force
+next
+  case False
+  show ?thesis
+  proof (rule invariance_of_domain_sphere_affine_set_gen [OF contf injf fim bounded_cball convex_cball \<open>affine T\<close>])
+    show "aff_dim T < aff_dim (cball a r)"
+      by (metis False affTU aff_dim_cball assms(4) linorder_cases sphere_empty)
+    show "openin (subtopology euclidean (rel_frontier (cball a r))) S"
+      by (simp add: \<open>r \<noteq> 0\<close> ope)
+  qed
+qed
+
+lemma no_embedding_sphere_lowdim:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes contf: "continuous_on (sphere a r) f" and injf: "inj_on f (sphere a r)" and "r > 0"
+   shows "DIM('a) \<le> DIM('b)"
+proof -
+  have "False" if "DIM('a) > DIM('b)"
+  proof -
+    have "compact (f ` sphere a r)"
+      using compact_continuous_image
+      by (simp add: compact_continuous_image contf)
+    then have "\<not> open (f ` sphere a r)"
+      using compact_open
+      by (metis assms(3) image_is_empty not_less_iff_gr_or_eq sphere_eq_empty)
+    then show False
+      using invariance_of_domain_sphere_affine_set [OF contf injf subset_UNIV] \<open>r > 0\<close>
+      by (metis aff_dim_UNIV affine_UNIV less_irrefl of_nat_less_iff open_openin openin_subtopology_self subtopology_UNIV that)
+  qed
+  then show ?thesis
+    using not_less by blast
+qed
+
+
+subsection\<open> Dimension-based conditions for various homeomorphisms.\<close>
+
+lemma simply_connected_sphere:
+  fixes a :: "'a::euclidean_space"
+  assumes "3 \<le> DIM('a)"
+    shows "simply_connected(sphere a r)"
+proof (cases rule: linorder_cases [of r 0])
+  case less
+  then show ?thesis by simp
+next
+  case equal
+  then show ?thesis  by (auto simp: convex_imp_simply_connected)
+next
+  case greater
+  then show ?thesis
+    using simply_connected_sphere_gen [of "cball a r"] assms
+    by (simp add: aff_dim_cball)
+qed
+
+
 subsection\<open>The power, squaring and exponential functions as covering maps\<close>
 
 proposition covering_space_power_punctured_plane:
@@ -2978,7 +3226,6 @@
   by (simp add: covering_space_power_punctured_plane)
 
 
-
 proposition covering_space_exp_punctured_plane:
   "covering_space UNIV (\<lambda>z::complex. exp z) (- {0})"
 proof (simp add: covering_space_def, intro conjI ballI)
@@ -3094,83 +3341,4 @@
   qed
 qed
 
-subsection\<open> Dimension-based conditions for various homeomorphisms.\<close>
-
-lemma homeomorphic_subspaces_eq:
-  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
-  assumes "subspace S" "subspace T"
-  shows "S homeomorphic T \<longleftrightarrow> dim S = dim T"
-proof
-  assume "S homeomorphic T"
-  then obtain f g where hom: "homeomorphism S T f g"
-    using homeomorphic_def by blast
-  show "dim S = dim T"
-  proof (rule order_antisym)
-    show "dim S \<le> dim T"
-      by (metis assms dual_order.refl inj_onI homeomorphism_cont1 [OF hom] homeomorphism_apply1 [OF hom] homeomorphism_image1 [OF hom] continuous_injective_image_subspace_dim_le)
-    show "dim T \<le> dim S"
-      by (metis assms dual_order.refl inj_onI homeomorphism_cont2 [OF hom] homeomorphism_apply2 [OF hom] homeomorphism_image2 [OF hom] continuous_injective_image_subspace_dim_le)
-  qed
-next
-  assume "dim S = dim T"
-  then show "S homeomorphic T"
-    by (simp add: assms homeomorphic_subspaces)
-qed
-
-lemma homeomorphic_affine_sets_eq:
-  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
-  assumes "affine S" "affine T"
-  shows "S homeomorphic T \<longleftrightarrow> aff_dim S = aff_dim T"
-proof (cases "S = {} \<or> T = {}")
-  case True
-  then show ?thesis
-    using assms homeomorphic_affine_sets by force
-next
-  case False
-  then obtain a b where "a \<in> S" "b \<in> T"
-    by blast
-  then have "subspace (op + (- a) ` S)" "subspace (op + (- b) ` T)"
-    using affine_diffs_subspace assms by blast+
-  then show ?thesis
-    by (metis affine_imp_convex assms homeomorphic_affine_sets homeomorphic_convex_sets)
-qed
-
-
-lemma homeomorphic_hyperplanes_eq:
-  fixes a :: "'a::euclidean_space" and c :: "'b::euclidean_space"
-  assumes "a \<noteq> 0" "c \<noteq> 0"
-  shows "({x. a \<bullet> x = b} homeomorphic {x. c \<bullet> x = d} \<longleftrightarrow> DIM('a) = DIM('b))"
-  apply (auto simp: homeomorphic_affine_sets_eq affine_hyperplane assms)
-  by (metis DIM_positive Suc_pred)
-
-lemma homeomorphic_UNIV_UNIV:
-  shows "(UNIV::'a set) homeomorphic (UNIV::'b set) \<longleftrightarrow>
-    DIM('a::euclidean_space) = DIM('b::euclidean_space)"
-  by (simp add: homeomorphic_subspaces_eq)
-
-lemma simply_connected_sphere_gen:
-   assumes "convex S" "bounded S" and 3: "3 \<le> aff_dim S"
-   shows "simply_connected(rel_frontier S)"
-proof -
-  have pa: "path_connected (rel_frontier S)"
-    using assms by (simp add: path_connected_sphere_gen)
-  show ?thesis
-  proof (clarsimp simp add: simply_connected_eq_contractible_circlemap pa)
-    fix f
-    assume f: "continuous_on (sphere (0::complex) 1) f" "f ` sphere 0 1 \<subseteq> rel_frontier S"
-    have eq: "sphere (0::complex) 1 = rel_frontier(cball 0 1)"
-      by simp
-    have "convex (cball (0::complex) 1)"
-      by (rule convex_cball)
-    then obtain c where "homotopic_with (\<lambda>z. True) (sphere (0::complex) 1) (rel_frontier S) f (\<lambda>x. c)"
-      apply (rule inessential_spheremap_lowdim_gen [OF _ bounded_cball \<open>convex S\<close> \<open>bounded S\<close>, where f=f])
-      using f 3
-         apply (auto simp: aff_dim_cball)
-      done
-    then show "\<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) (rel_frontier S) f (\<lambda>x. a)"
-      by blast
-  qed
-qed
-
-
 end