diff --git a/src/HOL/Analysis/Homotopy.thy b/src/HOL/Analysis/Homotopy.thy --- a/src/HOL/Analysis/Homotopy.thy +++ b/src/HOL/Analysis/Homotopy.thy @@ -1,5520 +1,5457 @@ (* Title: HOL/Analysis/Path_Connected.thy Authors: LC Paulson and Robert Himmelmann (TU Muenchen), based on material from HOL Light *) section \Homotopy of Maps\ theory Homotopy imports Path_Connected Product_Topology Uncountable_Sets begin definition\<^marker>\tag important\ homotopic_with where "homotopic_with P X Y f g \ (\h. continuous_map (prod_topology (top_of_set {0..1::real}) X) Y h \ (\x. h(0, x) = f x) \ (\x. h(1, x) = g x) \ (\t \ {0..1}. P(\x. h(t,x))))" text\\p\, \q\ are functions \X \ Y\, and the property \P\ restricts all intermediate maps. We often just want to require that \P\ fixes some subset, but to include the case of a loop homotopy, it is convenient to have a general property \P\.\ abbreviation homotopic_with_canon :: "[('a::topological_space \ 'b::topological_space) \ bool, 'a set, 'b set, 'a \ 'b, 'a \ 'b] \ bool" where "homotopic_with_canon P S T p q \ homotopic_with P (top_of_set S) (top_of_set T) p q" lemma split_01: "{0..1::real} = {0..1/2} \ {1/2..1}" by force lemma split_01_prod: "{0..1::real} \ X = ({0..1/2} \ X) \ ({1/2..1} \ X)" by force lemma image_Pair_const: "(\x. (x, c)) ` A = A \ {c}" by auto lemma fst_o_paired [simp]: "fst \ (\(x,y). (f x y, g x y)) = (\(x,y). f x y)" by auto lemma snd_o_paired [simp]: "snd \ (\(x,y). (f x y, g x y)) = (\(x,y). g x y)" by auto lemma continuous_on_o_Pair: "\continuous_on (T \ X) h; t \ T\ \ continuous_on X (h \ Pair t)" by (fast intro: continuous_intros elim!: continuous_on_subset) lemma continuous_map_o_Pair: assumes h: "continuous_map (prod_topology X Y) Z h" and t: "t \ topspace X" shows "continuous_map Y Z (h \ Pair t)" by (intro continuous_map_compose [OF _ h] continuous_intros; simp add: t) subsection\<^marker>\tag unimportant\\Trivial properties\ text \We often want to just localize the ending function equality or whatever.\ text\<^marker>\tag important\ \%whitespace\ proposition homotopic_with: assumes "\h k. (\x. x \ topspace X \ h x = k x) \ (P h \ P k)" shows "homotopic_with P X Y p q \ (\h. continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y h \ (\x \ topspace X. h(0,x) = p x) \ (\x \ topspace X. h(1,x) = q x) \ (\t \ {0..1}. P(\x. h(t, x))))" unfolding homotopic_with_def apply (rule iffI, blast, clarify) apply (rule_tac x="\(u,v). if v \ topspace X then h(u,v) else if u = 0 then p v else q v" in exI) - apply auto - using continuous_map_eq apply fastforce - apply (drule_tac x=t in bspec, force) - apply (subst assms; simp) - done + apply simp + by (smt (verit, best) SigmaE assms case_prod_conv continuous_map_eq topspace_prod_topology) lemma homotopic_with_mono: assumes hom: "homotopic_with P X Y f g" and Q: "\h. \continuous_map X Y h; P h\ \ Q h" shows "homotopic_with Q X Y f g" using hom unfolding homotopic_with_def by (force simp: o_def dest: continuous_map_o_Pair intro: Q) lemma homotopic_with_imp_continuous_maps: assumes "homotopic_with P X Y f g" shows "continuous_map X Y f \ continuous_map X Y g" proof - obtain h :: "real \ 'a \ 'b" where conth: "continuous_map (prod_topology (top_of_set {0..1}) X) Y h" and h: "\x. h (0, x) = f x" "\x. h (1, x) = g x" using assms by (auto simp: homotopic_with_def) have *: "t \ {0..1} \ continuous_map X Y (h \ (\x. (t,x)))" for t by (rule continuous_map_compose [OF _ conth]) (simp add: o_def continuous_map_pairwise) show ?thesis using h *[of 0] *[of 1] by (simp add: continuous_map_eq) qed lemma homotopic_with_imp_continuous: assumes "homotopic_with_canon P X Y f g" shows "continuous_on X f \ continuous_on X g" by (meson assms continuous_map_subtopology_eu homotopic_with_imp_continuous_maps) lemma homotopic_with_imp_property: assumes "homotopic_with P X Y f g" shows "P f \ P g" proof obtain h where h: "\x. h(0, x) = f x" "\x. h(1, x) = g x" and P: "\t. t \ {0..1::real} \ P(\x. h(t,x))" using assms by (force simp: homotopic_with_def) show "P f" "P g" using P [of 0] P [of 1] by (force simp: h)+ qed lemma homotopic_with_equal: assumes "P f" "P g" and contf: "continuous_map X Y f" and fg: "\x. x \ topspace X \ f x = g x" shows "homotopic_with P X Y f g" unfolding homotopic_with_def proof (intro exI conjI allI ballI) let ?h = "\(t::real,x). if t = 1 then g x else f x" show "continuous_map (prod_topology (top_of_set {0..1}) X) Y ?h" proof (rule continuous_map_eq) show "continuous_map (prod_topology (top_of_set {0..1}) X) Y (f \ snd)" by (simp add: contf continuous_map_of_snd) qed (auto simp: fg) show "P (\x. ?h (t, x))" if "t \ {0..1}" for t by (cases "t = 1") (simp_all add: assms) qed auto lemma homotopic_with_imp_subset1: "homotopic_with_canon P X Y f g \ f ` X \ Y" - by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one) + by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps) lemma homotopic_with_imp_subset2: "homotopic_with_canon P X Y f g \ g ` X \ Y" - by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one) + by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps) lemma homotopic_with_subset_left: "\homotopic_with_canon P X Y f g; Z \ X\ \ homotopic_with_canon P Z Y f g" unfolding homotopic_with_def by (auto elim!: continuous_on_subset ex_forward) lemma homotopic_with_subset_right: "\homotopic_with_canon P X Y f g; Y \ Z\ \ homotopic_with_canon P X Z f g" unfolding homotopic_with_def by (auto elim!: continuous_on_subset ex_forward) subsection\Homotopy with P is an equivalence relation\ text \(on continuous functions mapping X into Y that satisfy P, though this only affects reflexivity)\ lemma homotopic_with_refl [simp]: "homotopic_with P X Y f f \ continuous_map X Y f \ P f" - by (auto simp: homotopic_with_imp_continuous_maps intro: homotopic_with_equal dest: homotopic_with_imp_property) + by (metis homotopic_with_equal homotopic_with_imp_continuous_maps homotopic_with_imp_property) lemma homotopic_with_symD: assumes "homotopic_with P X Y f g" shows "homotopic_with P X Y g f" proof - let ?I01 = "subtopology euclideanreal {0..1}" let ?j = "\y. (1 - fst y, snd y)" have 1: "continuous_map (prod_topology ?I01 X) (prod_topology euclideanreal X) ?j" by (intro continuous_intros; simp add: continuous_map_subtopology_fst prod_topology_subtopology) have *: "continuous_map (prod_topology ?I01 X) (prod_topology ?I01 X) ?j" proof - have "continuous_map (prod_topology ?I01 X) (subtopology (prod_topology euclideanreal X) ({0..1} \ topspace X)) ?j" by (simp add: continuous_map_into_subtopology [OF 1] image_subset_iff) then show ?thesis by (simp add: prod_topology_subtopology(1)) qed show ?thesis using assms apply (clarsimp simp add: homotopic_with_def) subgoal for h by (rule_tac x="h \ (\y. (1 - fst y, snd y))" in exI) (simp add: continuous_map_compose [OF *]) done qed lemma homotopic_with_sym: "homotopic_with P X Y f g \ homotopic_with P X Y g f" by (metis homotopic_with_symD) proposition homotopic_with_trans: assumes "homotopic_with P X Y f g" "homotopic_with P X Y g h" shows "homotopic_with P X Y f h" proof - let ?X01 = "prod_topology (subtopology euclideanreal {0..1}) X" obtain k1 k2 where contk1: "continuous_map ?X01 Y k1" and contk2: "continuous_map ?X01 Y k2" and k12: "\x. k1 (1, x) = g x" "\x. k2 (0, x) = g x" "\x. k1 (0, x) = f x" "\x. k2 (1, x) = h x" and P: "\t\{0..1}. P (\x. k1 (t, x))" "\t\{0..1}. P (\x. k2 (t, x))" using assms by (auto simp: homotopic_with_def) define k where "k \ \y. if fst y \ 1/2 then (k1 \ (\x. (2 *\<^sub>R fst x, snd x))) y else (k2 \ (\x. (2 *\<^sub>R fst x -1, snd x))) y" have keq: "k1 (2 * u, v) = k2 (2 * u -1, v)" if "u = 1/2" for u v by (simp add: k12 that) show ?thesis unfolding homotopic_with_def proof (intro exI conjI) show "continuous_map ?X01 Y k" unfolding k_def proof (rule continuous_map_cases_le) show fst: "continuous_map ?X01 euclideanreal fst" using continuous_map_fst continuous_map_in_subtopology by blast show "continuous_map ?X01 euclideanreal (\x. 1/2)" by simp show "continuous_map (subtopology ?X01 {y \ topspace ?X01. fst y \ 1/2}) Y (k1 \ (\x. (2 *\<^sub>R fst x, snd x)))" apply (intro fst continuous_map_compose [OF _ contk1] continuous_intros continuous_map_into_subtopology continuous_map_from_subtopology | simp)+ by (force simp: prod_topology_subtopology) show "continuous_map (subtopology ?X01 {y \ topspace ?X01. 1/2 \ fst y}) Y (k2 \ (\x. (2 *\<^sub>R fst x -1, snd x)))" apply (intro fst continuous_map_compose [OF _ contk2] continuous_intros continuous_map_into_subtopology continuous_map_from_subtopology | simp)+ by (force simp: prod_topology_subtopology) show "(k1 \ (\x. (2 *\<^sub>R fst x, snd x))) y = (k2 \ (\x. (2 *\<^sub>R fst x -1, snd x))) y" if "y \ topspace ?X01" and "fst y = 1/2" for y using that by (simp add: keq) qed show "\x. k (0, x) = f x" by (simp add: k12 k_def) show "\x. k (1, x) = h x" by (simp add: k12 k_def) show "\t\{0..1}. P (\x. k (t, x))" proof fix t show "t\{0..1} \ P (\x. k (t, x))" by (cases "t \ 1/2") (auto simp add: k_def P) qed qed qed lemma homotopic_with_id2: "(\x. x \ topspace X \ g (f x) = x) \ homotopic_with (\x. True) X X (g \ f) id" by (metis comp_apply continuous_map_id eq_id_iff homotopic_with_equal homotopic_with_symD) subsection\Continuity lemmas\ lemma homotopic_with_compose_continuous_map_left: "\homotopic_with p X1 X2 f g; continuous_map X2 X3 h; \j. p j \ q(h \ j)\ \ homotopic_with q X1 X3 (h \ f) (h \ g)" unfolding homotopic_with_def apply clarify subgoal for k by (rule_tac x="h \ k" in exI) (rule conjI continuous_map_compose | simp add: o_def)+ done lemma homotopic_with_compose_continuous_map_right: assumes hom: "homotopic_with p X2 X3 f g" and conth: "continuous_map X1 X2 h" and q: "\j. p j \ q(j \ h)" shows "homotopic_with q X1 X3 (f \ h) (g \ h)" proof - obtain k where contk: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X2) X3 k" and k: "\x. k (0, x) = f x" "\x. k (1, x) = g x" and p: "\t. t\{0..1} \ p (\x. k (t, x))" using hom unfolding homotopic_with_def by blast have hsnd: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) X2 (h \ snd)" by (rule continuous_map_compose [OF continuous_map_snd conth]) let ?h = "k \ (\(t,x). (t,h x))" show ?thesis unfolding homotopic_with_def proof (intro exI conjI allI ballI) have "continuous_map (prod_topology (top_of_set {0..1}) X1) (prod_topology (top_of_set {0..1::real}) X2) (\(t, x). (t, h x))" by (metis (mono_tags, lifting) case_prod_beta' comp_def continuous_map_eq continuous_map_fst continuous_map_pairedI hsnd) then show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) X3 ?h" by (intro conjI continuous_map_compose [OF _ contk]) show "q (\x. ?h (t, x))" if "t \ {0..1}" for t using q [OF p [OF that]] by (simp add: o_def) qed (auto simp: k) qed corollary homotopic_compose: assumes "homotopic_with (\x. True) X Y f f'" "homotopic_with (\x. True) Y Z g g'" shows "homotopic_with (\x. True) X Z (g \ f) (g' \ f')" -proof (rule homotopic_with_trans [where g = "g \ f'"]) - show "homotopic_with (\x. True) X Z (g \ f) (g \ f')" - using assms by (simp add: homotopic_with_compose_continuous_map_left homotopic_with_imp_continuous_maps) - show "homotopic_with (\x. True) X Z (g \ f') (g' \ f')" - using assms by (simp add: homotopic_with_compose_continuous_map_right homotopic_with_imp_continuous_maps) -qed + by (metis assms homotopic_with_compose_continuous_map_left homotopic_with_compose_continuous_map_right homotopic_with_imp_continuous_maps homotopic_with_trans) proposition homotopic_with_compose_continuous_right: "\homotopic_with_canon (\f. p (f \ h)) X Y f g; continuous_on W h; h ` W \ X\ \ homotopic_with_canon p W Y (f \ h) (g \ h)" - apply (clarsimp simp add: homotopic_with_def) - subgoal for k - apply (rule_tac x="k \ (\y. (fst y, h (snd y)))" in exI) - by (intro conjI continuous_intros continuous_on_compose2 [where f=snd and g=h]; fastforce simp: o_def elim: continuous_on_subset) - done + by (simp add: homotopic_with_compose_continuous_map_right) proposition homotopic_with_compose_continuous_left: "\homotopic_with_canon (\f. p (h \ f)) X Y f g; continuous_on Y h; h ` Y \ Z\ \ homotopic_with_canon p X Z (h \ f) (h \ g)" - apply (clarsimp simp add: homotopic_with_def) - subgoal for k - apply (rule_tac x="h \ k" in exI) - by (intro conjI continuous_intros continuous_on_compose [where f=snd and g=h, unfolded o_def]; fastforce simp: o_def elim: continuous_on_subset) - done + by (simp add: homotopic_with_compose_continuous_map_left) lemma homotopic_from_subtopology: - "homotopic_with P X X' f g \ homotopic_with P (subtopology X s) X' f g" - unfolding homotopic_with_def - by (force simp add: continuous_map_from_subtopology prod_topology_subtopology(2) elim!: ex_forward) + "homotopic_with P X X' f g \ homotopic_with P (subtopology X S) X' f g" + by (metis continuous_map_id_subt homotopic_with_compose_continuous_map_right o_id) lemma homotopic_on_emptyI: assumes "topspace X = {}" "P f" "P g" shows "homotopic_with P X X' f g" - unfolding homotopic_with_def -proof (intro exI conjI ballI) - show "P (\x. (\(t,x). if t = 0 then f x else g x) (t, x))" if "t \ {0..1}" for t::real - by (cases "t = 0", auto simp: assms) -qed (auto simp: continuous_map_atin assms) + by (metis assms continuous_map_on_empty empty_iff homotopic_with_equal) lemma homotopic_on_empty: "topspace X = {} \ (homotopic_with P X X' f g \ P f \ P g)" using homotopic_on_emptyI homotopic_with_imp_property by metis lemma homotopic_with_canon_on_empty [simp]: "homotopic_with_canon (\x. True) {} t f g" by (auto intro: homotopic_with_equal) lemma homotopic_constant_maps: "homotopic_with (\x. True) X X' (\x. a) (\x. b) \ topspace X = {} \ path_component_of X' a b" (is "?lhs = ?rhs") proof (cases "topspace X = {}") case False then obtain c where c: "c \ topspace X" by blast have "\g. continuous_map (top_of_set {0..1::real}) X' g \ g 0 = a \ g 1 = b" if "x \ topspace X" and hom: "homotopic_with (\x. True) X X' (\x. a) (\x. b)" for x proof - obtain h :: "real \ 'a \ 'b" where conth: "continuous_map (prod_topology (top_of_set {0..1}) X) X' h" and h: "\x. h (0, x) = a" "\x. h (1, x) = b" using hom by (auto simp: homotopic_with_def) have cont: "continuous_map (top_of_set {0..1}) X' (h \ (\t. (t, c)))" by (rule continuous_map_compose [OF _ conth] continuous_intros c | simp)+ then show ?thesis by (force simp: h) qed moreover have "homotopic_with (\x. True) X X' (\x. g 0) (\x. g 1)" if "x \ topspace X" "a = g 0" "b = g 1" "continuous_map (top_of_set {0..1}) X' g" for x and g :: "real \ 'b" unfolding homotopic_with_def by (force intro!: continuous_map_compose continuous_intros c that) ultimately show ?thesis using False by (auto simp: path_component_of_def pathin_def) qed (simp add: homotopic_on_empty) proposition homotopic_with_eq: assumes h: "homotopic_with P X Y f g" and f': "\x. x \ topspace X \ f' x = f x" and g': "\x. x \ topspace X \ g' x = g x" and P: "(\h k. (\x. x \ topspace X \ h x = k x) \ P h \ P k)" shows "homotopic_with P X Y f' g'" - using h unfolding homotopic_with_def - apply clarify - subgoal for h - apply (rule_tac x="\(u,v). if v \ topspace X then h(u,v) else if u = 0 then f' v else g' v" in exI) - apply (simp add: f' g', safe) - apply (fastforce intro: continuous_map_eq) - apply (subst P; fastforce) - done - done + by (smt (verit, ccfv_SIG) assms homotopic_with) lemma homotopic_with_prod_topology: assumes "homotopic_with p X1 Y1 f f'" and "homotopic_with q X2 Y2 g g'" and r: "\i j. \p i; q j\ \ r(\(x,y). (i x, j y))" shows "homotopic_with r (prod_topology X1 X2) (prod_topology Y1 Y2) (\z. (f(fst z),g(snd z))) (\z. (f'(fst z), g'(snd z)))" proof - obtain h where h: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) Y1 h" and h0: "\x. h (0, x) = f x" and h1: "\x. h (1, x) = f' x" and p: "\t. \0 \ t; t \ 1\ \ p (\x. h (t,x))" using assms unfolding homotopic_with_def by auto obtain k where k: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X2) Y2 k" and k0: "\x. k (0, x) = g x" and k1: "\x. k (1, x) = g' x" and q: "\t. \0 \ t; t \ 1\ \ q (\x. k (t,x))" using assms unfolding homotopic_with_def by auto let ?hk = "\(t,x,y). (h(t,x), k(t,y))" show ?thesis unfolding homotopic_with_def proof (intro conjI allI exI) show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (prod_topology X1 X2)) (prod_topology Y1 Y2) ?hk" unfolding continuous_map_pairwise case_prod_unfold by (rule conjI continuous_map_pairedI continuous_intros continuous_map_id [unfolded id_def] continuous_map_fst_of [unfolded o_def] continuous_map_snd_of [unfolded o_def] continuous_map_compose [OF _ h, unfolded o_def] continuous_map_compose [OF _ k, unfolded o_def])+ next fix x show "?hk (0, x) = (f (fst x), g (snd x))" "?hk (1, x) = (f' (fst x), g' (snd x))" by (auto simp: case_prod_beta h0 k0 h1 k1) qed (auto simp: p q r) qed lemma homotopic_with_product_topology: assumes ht: "\i. i \ I \ homotopic_with (p i) (X i) (Y i) (f i) (g i)" and pq: "\h. (\i. i \ I \ p i (h i)) \ q(\x. (\i\I. h i (x i)))" shows "homotopic_with q (product_topology X I) (product_topology Y I) (\z. (\i\I. (f i) (z i))) (\z. (\i\I. (g i) (z i)))" proof - obtain h where h: "\i. i \ I \ continuous_map (prod_topology (subtopology euclideanreal {0..1}) (X i)) (Y i) (h i)" and h0: "\i x. i \ I \ h i (0, x) = f i x" and h1: "\i x. i \ I \ h i (1, x) = g i x" and p: "\i t. \i \ I; t \ {0..1}\ \ p i (\x. h i (t,x))" using ht unfolding homotopic_with_def by metis show ?thesis unfolding homotopic_with_def proof (intro conjI allI exI) let ?h = "\(t,z). \i\I. h i (t,z i)" have "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (product_topology X I)) (Y i) (\x. h i (fst x, snd x i))" if "i \ I" for i proof - have \
: "continuous_map (prod_topology (top_of_set {0..1}) (product_topology X I)) (X i) (\x. snd x i)" using continuous_map_componentwise continuous_map_snd that by fastforce show ?thesis unfolding continuous_map_pairwise case_prod_unfold by (intro conjI that \
continuous_intros continuous_map_compose [OF _ h, unfolded o_def]) qed then show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (product_topology X I)) (product_topology Y I) ?h" by (auto simp: continuous_map_componentwise case_prod_beta) show "?h (0, x) = (\i\I. f i (x i))" "?h (1, x) = (\i\I. g i (x i))" for x by (auto simp: case_prod_beta h0 h1) show "\t\{0..1}. q (\x. ?h (t, x))" by (force intro: p pq) qed qed text\Homotopic triviality implicitly incorporates path-connectedness.\ lemma homotopic_triviality: shows "(\f g. continuous_on S f \ f ` S \ T \ continuous_on S g \ g ` S \ T \ homotopic_with_canon (\x. True) S T f g) \ (S = {} \ path_connected T) \ (\f. continuous_on S f \ f ` S \ T \ (\c. homotopic_with_canon (\x. True) S T f (\x. c)))" (is "?lhs = ?rhs") proof (cases "S = {} \ T = {}") case True then show ?thesis by (auto simp: homotopic_on_emptyI) next case False show ?thesis proof assume LHS [rule_format]: ?lhs have pab: "path_component T a b" if "a \ T" "b \ T" for a b proof - have "homotopic_with_canon (\x. True) S T (\x. a) (\x. b)" by (simp add: LHS image_subset_iff that) then show ?thesis using False homotopic_constant_maps [of "top_of_set S" "top_of_set T" a b] by auto qed moreover have "\c. homotopic_with_canon (\x. True) S T f (\x. c)" if "continuous_on S f" "f ` S \ T" for f using False LHS continuous_on_const that by blast ultimately show ?rhs by (simp add: path_connected_component) next assume RHS: ?rhs with False have T: "path_connected T" by blast show ?lhs proof clarify fix f g assume "continuous_on S f" "f ` S \ T" "continuous_on S g" "g ` S \ T" obtain c d where c: "homotopic_with_canon (\x. True) S T f (\x. c)" and d: "homotopic_with_canon (\x. True) S T g (\x. d)" using False \continuous_on S f\ \f ` S \ T\ RHS \continuous_on S g\ \g ` S \ T\ by blast - then have "c \ T" "d \ T" - using False homotopic_with_imp_continuous_maps by fastforce+ with T have "path_component T c d" - using path_connected_component by blast + by (metis False ex_in_conv homotopic_with_imp_subset2 image_subset_iff path_connected_component) then have "homotopic_with_canon (\x. True) S T (\x. c) (\x. d)" by (simp add: homotopic_constant_maps) with c d show "homotopic_with_canon (\x. True) S T f g" by (meson homotopic_with_symD homotopic_with_trans) qed qed qed subsection\Homotopy of paths, maintaining the same endpoints\ definition\<^marker>\tag important\ homotopic_paths :: "['a set, real \ 'a, real \ 'a::topological_space] \ bool" where - "homotopic_paths s p q \ - homotopic_with_canon (\r. pathstart r = pathstart p \ pathfinish r = pathfinish p) {0..1} s p q" + "homotopic_paths S p q \ + homotopic_with_canon (\r. pathstart r = pathstart p \ pathfinish r = pathfinish p) {0..1} S p q" lemma homotopic_paths: - "homotopic_paths s p q \ + "homotopic_paths S p q \ (\h. continuous_on ({0..1} \ {0..1}) h \ - h ` ({0..1} \ {0..1}) \ s \ + h ` ({0..1} \ {0..1}) \ S \ (\x \ {0..1}. h(0,x) = p x) \ (\x \ {0..1}. h(1,x) = q x) \ (\t \ {0..1::real}. pathstart(h \ Pair t) = pathstart p \ pathfinish(h \ Pair t) = pathfinish p))" by (auto simp: homotopic_paths_def homotopic_with pathstart_def pathfinish_def) proposition homotopic_paths_imp_pathstart: - "homotopic_paths s p q \ pathstart p = pathstart q" + "homotopic_paths S p q \ pathstart p = pathstart q" by (metis (mono_tags, lifting) homotopic_paths_def homotopic_with_imp_property) proposition homotopic_paths_imp_pathfinish: - "homotopic_paths s p q \ pathfinish p = pathfinish q" + "homotopic_paths S p q \ pathfinish p = pathfinish q" by (metis (mono_tags, lifting) homotopic_paths_def homotopic_with_imp_property) lemma homotopic_paths_imp_path: - "homotopic_paths s p q \ path p \ path q" + "homotopic_paths S p q \ path p \ path q" using homotopic_paths_def homotopic_with_imp_continuous_maps path_def continuous_map_subtopology_eu by blast lemma homotopic_paths_imp_subset: - "homotopic_paths s p q \ path_image p \ s \ path_image q \ s" + "homotopic_paths S p q \ path_image p \ S \ path_image q \ S" by (metis (mono_tags) continuous_map_subtopology_eu homotopic_paths_def homotopic_with_imp_continuous_maps path_image_def) -proposition homotopic_paths_refl [simp]: "homotopic_paths s p p \ path p \ path_image p \ s" +proposition homotopic_paths_refl [simp]: "homotopic_paths S p p \ path p \ path_image p \ S" by (simp add: homotopic_paths_def path_def path_image_def) -proposition homotopic_paths_sym: "homotopic_paths s p q \ homotopic_paths s q p" +proposition homotopic_paths_sym: "homotopic_paths S p q \ homotopic_paths S q p" by (metis (mono_tags) homotopic_paths_def homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart homotopic_with_symD) -proposition homotopic_paths_sym_eq: "homotopic_paths s p q \ homotopic_paths s q p" +proposition homotopic_paths_sym_eq: "homotopic_paths S p q \ homotopic_paths S q p" by (metis homotopic_paths_sym) proposition homotopic_paths_trans [trans]: - assumes "homotopic_paths s p q" "homotopic_paths s q r" - shows "homotopic_paths s p r" -proof - - have "pathstart q = pathstart p" "pathfinish q = pathfinish p" - using assms by (simp_all add: homotopic_paths_imp_pathstart homotopic_paths_imp_pathfinish) - then have "homotopic_with_canon (\f. pathstart f = pathstart p \ pathfinish f = pathfinish p) {0..1} s q r" - using \homotopic_paths s q r\ homotopic_paths_def by force - then show ?thesis - using assms homotopic_paths_def homotopic_with_trans by blast -qed + assumes "homotopic_paths S p q" "homotopic_paths S q r" + shows "homotopic_paths S p r" + using assms homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart unfolding homotopic_paths_def + by (smt (verit, ccfv_SIG) homotopic_with_mono homotopic_with_trans) proposition homotopic_paths_eq: - "\path p; path_image p \ s; \t. t \ {0..1} \ p t = q t\ \ homotopic_paths s p q" - unfolding homotopic_paths_def - by (rule homotopic_with_eq) - (auto simp: path_def pathstart_def pathfinish_def path_image_def elim: continuous_on_eq) + "\path p; path_image p \ S; \t. t \ {0..1} \ p t = q t\ \ homotopic_paths S p q" + by (smt (verit, best) homotopic_paths homotopic_paths_refl) proposition homotopic_paths_reparametrize: assumes "path p" - and pips: "path_image p \ s" + and pips: "path_image p \ S" and contf: "continuous_on {0..1} f" and f01:"f ` {0..1} \ {0..1}" and [simp]: "f(0) = 0" "f(1) = 1" and q: "\t. t \ {0..1} \ q(t) = p(f t)" - shows "homotopic_paths s p q" + shows "homotopic_paths S p q" proof - have contp: "continuous_on {0..1} p" by (metis \path p\ path_def) then have "continuous_on {0..1} (p \ f)" using contf continuous_on_compose continuous_on_subset f01 by blast then have "path q" by (simp add: path_def) (metis q continuous_on_cong) - have piqs: "path_image q \ s" + have piqs: "path_image q \ S" by (metis (no_types, opaque_lifting) pips f01 image_subset_iff path_image_def q) have fb0: "\a b. \0 \ a; a \ 1; 0 \ b; b \ 1\ \ 0 \ (1 - a) * f b + a * b" using f01 by force have fb1: "\0 \ a; a \ 1; 0 \ b; b \ 1\ \ (1 - a) * f b + a * b \ 1" for a b using f01 [THEN subsetD, of "f b"] by (simp add: convex_bound_le) - have "homotopic_paths s q p" + have "homotopic_paths S q p" proof (rule homotopic_paths_trans) - show "homotopic_paths s q (p \ f)" + show "homotopic_paths S q (p \ f)" using q by (force intro: homotopic_paths_eq [OF \path q\ piqs]) next - show "homotopic_paths s (p \ f) p" + show "homotopic_paths S (p \ f) p" using pips [unfolded path_image_def] apply (simp add: homotopic_paths_def homotopic_with_def) apply (rule_tac x="p \ (\y. (1 - (fst y)) *\<^sub>R ((f \ snd) y) + (fst y) *\<^sub>R snd y)" in exI) apply (rule conjI contf continuous_intros continuous_on_subset [OF contp] | simp)+ by (auto simp: fb0 fb1 pathstart_def pathfinish_def) qed then show ?thesis by (simp add: homotopic_paths_sym) qed -lemma homotopic_paths_subset: "\homotopic_paths s p q; s \ t\ \ homotopic_paths t p q" +lemma homotopic_paths_subset: "\homotopic_paths S p q; S \ t\ \ homotopic_paths t p q" unfolding homotopic_paths by fast text\ A slightly ad-hoc but useful lemma in constructing homotopies.\ lemma continuous_on_homotopic_join_lemma: fixes q :: "[real,real] \ 'a::topological_space" assumes p: "continuous_on ({0..1} \ {0..1}) (\y. p (fst y) (snd y))" (is "continuous_on ?A ?p") and q: "continuous_on ({0..1} \ {0..1}) (\y. q (fst y) (snd y))" (is "continuous_on ?A ?q") and pf: "\t. t \ {0..1} \ pathfinish(p t) = pathstart(q t)" shows "continuous_on ({0..1} \ {0..1}) (\y. (p(fst y) +++ q(fst y)) (snd y))" proof - have \
: "(\t. p (fst t) (2 * snd t)) = ?p \ (\y. (fst y, 2 * snd y))" "(\t. q (fst t) (2 * snd t - 1)) = ?q \ (\y. (fst y, 2 * snd y - 1))" by force+ show ?thesis unfolding joinpaths_def proof (rule continuous_on_cases_le) show "continuous_on {y \ ?A. snd y \ 1/2} (\t. p (fst t) (2 * snd t))" "continuous_on {y \ ?A. 1/2 \ snd y} (\t. q (fst t) (2 * snd t - 1))" "continuous_on ?A snd" unfolding \
by (rule continuous_intros continuous_on_subset [OF p] continuous_on_subset [OF q] | force)+ qed (use pf in \auto simp: mult.commute pathstart_def pathfinish_def\) qed text\ Congruence properties of homotopy w.r.t. path-combining operations.\ lemma homotopic_paths_reversepath_D: - assumes "homotopic_paths s p q" - shows "homotopic_paths s (reversepath p) (reversepath q)" + assumes "homotopic_paths S p q" + shows "homotopic_paths S (reversepath p) (reversepath q)" using assms apply (simp add: homotopic_paths_def homotopic_with_def, clarify) apply (rule_tac x="h \ (\x. (fst x, 1 - snd x))" in exI) apply (rule conjI continuous_intros)+ apply (auto simp: reversepath_def pathstart_def pathfinish_def elim!: continuous_on_subset) done proposition homotopic_paths_reversepath: - "homotopic_paths s (reversepath p) (reversepath q) \ homotopic_paths s p q" + "homotopic_paths S (reversepath p) (reversepath q) \ homotopic_paths S p q" using homotopic_paths_reversepath_D by force proposition homotopic_paths_join: - "\homotopic_paths s p p'; homotopic_paths s q q'; pathfinish p = pathstart q\ \ homotopic_paths s (p +++ q) (p' +++ q')" + "\homotopic_paths S p p'; homotopic_paths S q q'; pathfinish p = pathstart q\ \ homotopic_paths S (p +++ q) (p' +++ q')" apply (clarsimp simp add: homotopic_paths_def homotopic_with_def) apply (rename_tac k1 k2) apply (rule_tac x="(\y. ((k1 \ Pair (fst y)) +++ (k2 \ Pair (fst y))) (snd y))" in exI) apply (intro conjI continuous_intros continuous_on_homotopic_join_lemma; force simp: joinpaths_def pathstart_def pathfinish_def path_image_def) done proposition homotopic_paths_continuous_image: - "\homotopic_paths s f g; continuous_on s h; h ` s \ t\ \ homotopic_paths t (h \ f) (h \ g)" + "\homotopic_paths S f g; continuous_on S h; h ` S \ t\ \ homotopic_paths t (h \ f) (h \ g)" unfolding homotopic_paths_def by (simp add: homotopic_with_compose_continuous_map_left pathfinish_compose pathstart_compose) subsection\Group properties for homotopy of paths\ text\<^marker>\tag important\\So taking equivalence classes under homotopy would give the fundamental group\ proposition homotopic_paths_rid: - assumes "path p" "path_image p \ s" - shows "homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p)) p" + assumes "path p" "path_image p \ S" + shows "homotopic_paths S (p +++ linepath (pathfinish p) (pathfinish p)) p" proof - have \
: "continuous_on {0..1} (\t::real. if t \ 1/2 then 2 *\<^sub>R t else 1)" unfolding split_01 by (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def)+ show ?thesis apply (rule homotopic_paths_sym) using assms unfolding pathfinish_def joinpaths_def by (intro \
continuous_on_cases continuous_intros homotopic_paths_reparametrize [where f = "\t. if t \ 1/2 then 2 *\<^sub>R t else 1"]; force) qed proposition homotopic_paths_lid: - "\path p; path_image p \ s\ \ homotopic_paths s (linepath (pathstart p) (pathstart p) +++ p) p" - using homotopic_paths_rid [of "reversepath p" s] + "\path p; path_image p \ S\ \ homotopic_paths S (linepath (pathstart p) (pathstart p) +++ p) p" + using homotopic_paths_rid [of "reversepath p" S] by (metis homotopic_paths_reversepath path_image_reversepath path_reversepath pathfinish_linepath pathfinish_reversepath reversepath_joinpaths reversepath_linepath) proposition homotopic_paths_assoc: - "\path p; path_image p \ s; path q; path_image q \ s; path r; path_image r \ s; pathfinish p = pathstart q; + "\path p; path_image p \ S; path q; path_image q \ S; path r; path_image r \ S; pathfinish p = pathstart q; pathfinish q = pathstart r\ - \ homotopic_paths s (p +++ (q +++ r)) ((p +++ q) +++ r)" + \ homotopic_paths S (p +++ (q +++ r)) ((p +++ q) +++ r)" apply (subst homotopic_paths_sym) apply (rule homotopic_paths_reparametrize [where f = "\t. if t \ 1/2 then inverse 2 *\<^sub>R t else if t \ 3 / 4 then t - (1 / 4) else 2 *\<^sub>R t - 1"]) apply (simp_all del: le_divide_eq_numeral1 add: subset_path_image_join) apply (rule continuous_on_cases_1 continuous_intros | auto simp: joinpaths_def)+ done proposition homotopic_paths_rinv: - assumes "path p" "path_image p \ s" - shows "homotopic_paths s (p +++ reversepath p) (linepath (pathstart p) (pathstart p))" + assumes "path p" "path_image p \ S" + shows "homotopic_paths S (p +++ reversepath p) (linepath (pathstart p) (pathstart p))" proof - have p: "continuous_on {0..1} p" using assms by (auto simp: path_def) let ?A = "{0..1} \ {0..1}" have "continuous_on ?A (\x. (subpath 0 (fst x) p +++ reversepath (subpath 0 (fst x) p)) (snd x))" unfolding joinpaths_def subpath_def reversepath_def path_def add_0_right diff_0_right proof (rule continuous_on_cases_le) show "continuous_on {x \ ?A. snd x \ 1/2} (\t. p (fst t * (2 * snd t)))" "continuous_on {x \ ?A. 1/2 \ snd x} (\t. p (fst t * (1 - (2 * snd t - 1))))" "continuous_on ?A snd" by (intro continuous_on_compose2 [OF p] continuous_intros; auto simp add: mult_le_one)+ qed (auto simp add: algebra_simps) then show ?thesis using assms apply (subst homotopic_paths_sym_eq) unfolding homotopic_paths_def homotopic_with_def apply (rule_tac x="(\y. (subpath 0 (fst y) p +++ reversepath(subpath 0 (fst y) p)) (snd y))" in exI) apply (force simp: mult_le_one path_defs joinpaths_def subpath_def reversepath_def) done qed proposition homotopic_paths_linv: - assumes "path p" "path_image p \ s" - shows "homotopic_paths s (reversepath p +++ p) (linepath (pathfinish p) (pathfinish p))" - using homotopic_paths_rinv [of "reversepath p" s] assms by simp + assumes "path p" "path_image p \ S" + shows "homotopic_paths S (reversepath p +++ p) (linepath (pathfinish p) (pathfinish p))" + using homotopic_paths_rinv [of "reversepath p" S] assms by simp subsection\Homotopy of loops without requiring preservation of endpoints\ definition\<^marker>\tag important\ homotopic_loops :: "'a::topological_space set \ (real \ 'a) \ (real \ 'a) \ bool" where - "homotopic_loops s p q \ - homotopic_with_canon (\r. pathfinish r = pathstart r) {0..1} s p q" + "homotopic_loops S p q \ + homotopic_with_canon (\r. pathfinish r = pathstart r) {0..1} S p q" lemma homotopic_loops: - "homotopic_loops s p q \ + "homotopic_loops S p q \ (\h. continuous_on ({0..1::real} \ {0..1}) h \ - image h ({0..1} \ {0..1}) \ s \ + image h ({0..1} \ {0..1}) \ S \ (\x \ {0..1}. h(0,x) = p x) \ (\x \ {0..1}. h(1,x) = q x) \ (\t \ {0..1}. pathfinish(h \ Pair t) = pathstart(h \ Pair t)))" by (simp add: homotopic_loops_def pathstart_def pathfinish_def homotopic_with) proposition homotopic_loops_imp_loop: - "homotopic_loops s p q \ pathfinish p = pathstart p \ pathfinish q = pathstart q" + "homotopic_loops S p q \ pathfinish p = pathstart p \ pathfinish q = pathstart q" using homotopic_with_imp_property homotopic_loops_def by blast proposition homotopic_loops_imp_path: - "homotopic_loops s p q \ path p \ path q" + "homotopic_loops S p q \ path p \ path q" unfolding homotopic_loops_def path_def using homotopic_with_imp_continuous_maps continuous_map_subtopology_eu by blast proposition homotopic_loops_imp_subset: - "homotopic_loops s p q \ path_image p \ s \ path_image q \ s" + "homotopic_loops S p q \ path_image p \ S \ path_image q \ S" unfolding homotopic_loops_def path_image_def by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps) proposition homotopic_loops_refl: - "homotopic_loops s p p \ - path p \ path_image p \ s \ pathfinish p = pathstart p" + "homotopic_loops S p p \ + path p \ path_image p \ S \ pathfinish p = pathstart p" by (simp add: homotopic_loops_def path_image_def path_def) -proposition homotopic_loops_sym: "homotopic_loops s p q \ homotopic_loops s q p" +proposition homotopic_loops_sym: "homotopic_loops S p q \ homotopic_loops S q p" by (simp add: homotopic_loops_def homotopic_with_sym) -proposition homotopic_loops_sym_eq: "homotopic_loops s p q \ homotopic_loops s q p" +proposition homotopic_loops_sym_eq: "homotopic_loops S p q \ homotopic_loops S q p" by (metis homotopic_loops_sym) proposition homotopic_loops_trans: - "\homotopic_loops s p q; homotopic_loops s q r\ \ homotopic_loops s p r" + "\homotopic_loops S p q; homotopic_loops S q r\ \ homotopic_loops S p r" unfolding homotopic_loops_def by (blast intro: homotopic_with_trans) proposition homotopic_loops_subset: - "\homotopic_loops s p q; s \ t\ \ homotopic_loops t p q" + "\homotopic_loops S p q; S \ t\ \ homotopic_loops t p q" by (fastforce simp add: homotopic_loops) proposition homotopic_loops_eq: - "\path p; path_image p \ s; pathfinish p = pathstart p; \t. t \ {0..1} \ p(t) = q(t)\ - \ homotopic_loops s p q" + "\path p; path_image p \ S; pathfinish p = pathstart p; \t. t \ {0..1} \ p(t) = q(t)\ + \ homotopic_loops S p q" unfolding homotopic_loops_def path_image_def path_def pathstart_def pathfinish_def by (auto intro: homotopic_with_eq [OF homotopic_with_refl [where f = p, THEN iffD2]]) proposition homotopic_loops_continuous_image: - "\homotopic_loops s f g; continuous_on s h; h ` s \ t\ \ homotopic_loops t (h \ f) (h \ g)" + "\homotopic_loops S f g; continuous_on S h; h ` S \ t\ \ homotopic_loops t (h \ f) (h \ g)" unfolding homotopic_loops_def by (simp add: homotopic_with_compose_continuous_map_left pathfinish_def pathstart_def) subsection\Relations between the two variants of homotopy\ proposition homotopic_paths_imp_homotopic_loops: - "\homotopic_paths s p q; pathfinish p = pathstart p; pathfinish q = pathstart p\ \ homotopic_loops s p q" + "\homotopic_paths S p q; pathfinish p = pathstart p; pathfinish q = pathstart p\ \ homotopic_loops S p q" by (auto simp: homotopic_with_def homotopic_paths_def homotopic_loops_def) proposition homotopic_loops_imp_homotopic_paths_null: - assumes "homotopic_loops s p (linepath a a)" - shows "homotopic_paths s p (linepath (pathstart p) (pathstart p))" + assumes "homotopic_loops S p (linepath a a)" + shows "homotopic_paths S p (linepath (pathstart p) (pathstart p))" proof - have "path p" by (metis assms homotopic_loops_imp_path) have ploop: "pathfinish p = pathstart p" by (metis assms homotopic_loops_imp_loop) - have pip: "path_image p \ s" by (metis assms homotopic_loops_imp_subset) + have pip: "path_image p \ S" by (metis assms homotopic_loops_imp_subset) let ?A = "{0..1::real} \ {0..1::real}" obtain h where conth: "continuous_on ?A h" - and hs: "h ` ?A \ s" - and [simp]: "\x. x \ {0..1} \ h(0,x) = p x" - and [simp]: "\x. x \ {0..1} \ h(1,x) = a" + and hs: "h ` ?A \ S" + and h0[simp]: "\x. x \ {0..1} \ h(0,x) = p x" + and h1[simp]: "\x. x \ {0..1} \ h(1,x) = a" and ends: "\t. t \ {0..1} \ pathfinish (h \ Pair t) = pathstart (h \ Pair t)" using assms by (auto simp: homotopic_loops homotopic_with) have conth0: "path (\u. h (u, 0))" unfolding path_def proof (rule continuous_on_compose [of _ _ h, unfolded o_def]) show "continuous_on ((\x. (x, 0)) ` {0..1}) h" by (force intro: continuous_on_subset [OF conth]) qed (force intro: continuous_intros) - have pih0: "path_image (\u. h (u, 0)) \ s" + have pih0: "path_image (\u. h (u, 0)) \ S" using hs by (force simp: path_image_def) have c1: "continuous_on ?A (\x. h (fst x * snd x, 0))" proof (rule continuous_on_compose [of _ _ h, unfolded o_def]) show "continuous_on ((\x. (fst x * snd x, 0)) ` ?A) h" by (force simp: mult_le_one intro: continuous_on_subset [OF conth]) qed (force intro: continuous_intros)+ have c2: "continuous_on ?A (\x. h (fst x - fst x * snd x, 0))" proof (rule continuous_on_compose [of _ _ h, unfolded o_def]) show "continuous_on ((\x. (fst x - fst x * snd x, 0)) ` ?A) h" by (auto simp: algebra_simps add_increasing2 mult_left_le intro: continuous_on_subset [OF conth]) qed (force intro: continuous_intros) have [simp]: "\t. \0 \ t \ t \ 1\ \ h (t, 1) = h (t, 0)" using ends by (simp add: pathfinish_def pathstart_def) have adhoc_le: "c * 4 \ 1 + c * (d * 4)" if "\ d * 4 \ 3" "0 \ c" "c \ 1" for c d::real proof - have "c * 3 \ c * (d * 4)" using that less_eq_real_def by auto with \c \ 1\ show ?thesis by fastforce qed have *: "\p x. \path p \ path(reversepath p); - path_image p \ s \ path_image(reversepath p) \ s; + path_image p \ S \ path_image(reversepath p) \ S; pathfinish p = pathstart(linepath a a +++ reversepath p) \ pathstart(reversepath p) = a \ pathstart p = x\ - \ homotopic_paths s (p +++ linepath a a +++ reversepath p) (linepath x x)" + \ homotopic_paths S (p +++ linepath a a +++ reversepath p) (linepath x x)" by (metis homotopic_paths_lid homotopic_paths_join homotopic_paths_trans homotopic_paths_sym homotopic_paths_rinv) - have 1: "homotopic_paths s p (p +++ linepath (pathfinish p) (pathfinish p))" + have 1: "homotopic_paths S p (p +++ linepath (pathfinish p) (pathfinish p))" using \path p\ homotopic_paths_rid homotopic_paths_sym pip by blast - moreover have "homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p)) + moreover have "homotopic_paths S (p +++ linepath (pathfinish p) (pathfinish p)) (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p))" - apply (rule homotopic_paths_sym) - using homotopic_paths_lid [of "p +++ linepath (pathfinish p) (pathfinish p)" s] - by (metis 1 homotopic_paths_imp_path homotopic_paths_imp_pathstart homotopic_paths_imp_subset) + using homotopic_paths_lid [of "p +++ linepath (pathfinish p) (pathfinish p)" S] + by (metis 1 homotopic_paths_imp_path homotopic_paths_imp_subset homotopic_paths_sym pathstart_join) moreover - have "homotopic_paths s (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p)) + have "homotopic_paths S (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p)) ((\u. h (u, 0)) +++ linepath a a +++ reversepath (\u. h (u, 0)))" unfolding homotopic_paths_def homotopic_with_def proof (intro exI strip conjI) let ?h = "\y. (subpath 0 (fst y) (\u. h (u, 0)) +++ (\u. h (Pair (fst y) u)) +++ subpath (fst y) 0 (\u. h (u, 0))) (snd y)" have "continuous_on ?A ?h" by (intro continuous_on_homotopic_join_lemma; simp add: path_defs joinpaths_def subpath_def conth c1 c2) - moreover have "?h ` ?A \ s" + moreover have "?h ` ?A \ S" unfolding joinpaths_def subpath_def by (force simp: algebra_simps mult_le_one mult_left_le intro: hs [THEN subsetD] adhoc_le) ultimately show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) - (top_of_set s) ?h" + (top_of_set S) ?h" by (simp add: subpath_reversepath) qed (use ploop in \simp_all add: reversepath_def path_defs joinpaths_def o_def subpath_def conth c1 c2\) - moreover have "homotopic_paths s ((\u. h (u, 0)) +++ linepath a a +++ reversepath (\u. h (u, 0))) + moreover have "homotopic_paths S ((\u. h (u, 0)) +++ linepath a a +++ reversepath (\u. h (u, 0))) (linepath (pathstart p) (pathstart p))" - proof (rule *; simp add: pih0 pathstart_def pathfinish_def conth0) - show "a = (linepath a a +++ reversepath (\u. h (u, 0))) 0 \ reversepath (\u. h (u, 0)) 0 = a" - by (simp_all add: reversepath_def joinpaths_def) - qed + by (rule *; simp add: pih0 pathstart_def pathfinish_def conth0; simp add: reversepath_def joinpaths_def) ultimately show ?thesis by (blast intro: homotopic_paths_trans) qed proposition homotopic_loops_conjugate: - fixes s :: "'a::real_normed_vector set" - assumes "path p" "path q" and pip: "path_image p \ s" and piq: "path_image q \ s" + fixes S :: "'a::real_normed_vector set" + assumes "path p" "path q" and pip: "path_image p \ S" and piq: "path_image q \ S" and pq: "pathfinish p = pathstart q" and qloop: "pathfinish q = pathstart q" - shows "homotopic_loops s (p +++ q +++ reversepath p) q" + shows "homotopic_loops S (p +++ q +++ reversepath p) q" proof - have contp: "continuous_on {0..1} p" using \path p\ [unfolded path_def] by blast have contq: "continuous_on {0..1} q" using \path q\ [unfolded path_def] by blast let ?A = "{0..1::real} \ {0..1::real}" have c1: "continuous_on ?A (\x. p ((1 - fst x) * snd x + fst x))" proof (rule continuous_on_compose [of _ _ p, unfolded o_def]) show "continuous_on ((\x. (1 - fst x) * snd x + fst x) ` ?A) p" by (auto intro: continuous_on_subset [OF contp] simp: algebra_simps add_increasing2 mult_right_le_one_le sum_le_prod1) qed (force intro: continuous_intros) have c2: "continuous_on ?A (\x. p ((fst x - 1) * snd x + 1))" proof (rule continuous_on_compose [of _ _ p, unfolded o_def]) show "continuous_on ((\x. (fst x - 1) * snd x + 1) ` ?A) p" by (auto intro: continuous_on_subset [OF contp] simp: algebra_simps add_increasing2 mult_left_le_one_le) qed (force intro: continuous_intros) - have ps1: "\a b. \b * 2 \ 1; 0 \ b; 0 \ a; a \ 1\ \ p ((1 - a) * (2 * b) + a) \ s" + have ps1: "\a b. \b * 2 \ 1; 0 \ b; 0 \ a; a \ 1\ \ p ((1 - a) * (2 * b) + a) \ S" using sum_le_prod1 by (force simp: algebra_simps add_increasing2 mult_left_le intro: pip [unfolded path_image_def, THEN subsetD]) - have ps2: "\a b. \\ 4 * b \ 3; b \ 1; 0 \ a; a \ 1\ \ p ((a - 1) * (4 * b - 3) + 1) \ s" + have ps2: "\a b. \\ 4 * b \ 3; b \ 1; 0 \ a; a \ 1\ \ p ((a - 1) * (4 * b - 3) + 1) \ S" apply (rule pip [unfolded path_image_def, THEN subsetD]) apply (rule image_eqI, blast) apply (simp add: algebra_simps) - by (metis add_mono_thms_linordered_semiring(1) affine_ineq linear mult.commute mult.left_neutral mult_right_mono + by (metis add_mono affine_ineq linear mult.commute mult.left_neutral mult_right_mono add.commute zero_le_numeral) - have qs: "\a b. \4 * b \ 3; \ b * 2 \ 1\ \ q (4 * b - 2) \ s" + have qs: "\a b. \4 * b \ 3; \ b * 2 \ 1\ \ q (4 * b - 2) \ S" using path_image_def piq by fastforce - have "homotopic_loops s (p +++ q +++ reversepath p) + have "homotopic_loops S (p +++ q +++ reversepath p) (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q))" unfolding homotopic_loops_def homotopic_with_def proof (intro exI strip conjI) let ?h = "(\y. (subpath (fst y) 1 p +++ q +++ subpath 1 (fst y) p) (snd y))" have "continuous_on ?A (\y. q (snd y))" by (force simp: contq intro: continuous_on_compose [of _ _ q, unfolded o_def] continuous_on_id continuous_on_snd) then have "continuous_on ?A ?h" using pq qloop by (intro continuous_on_homotopic_join_lemma) (auto simp: path_defs joinpaths_def subpath_def c1 c2) - then show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) (top_of_set s) ?h" + then show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) (top_of_set S) ?h" by (auto simp: joinpaths_def subpath_def ps1 ps2 qs) show "?h (1,x) = (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q)) x" for x using pq by (simp add: pathfinish_def subpath_refl) qed (auto simp: subpath_reversepath) - moreover have "homotopic_loops s (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q)) q" + moreover have "homotopic_loops S (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q)) q" proof - - have "homotopic_paths s (linepath (pathfinish q) (pathfinish q) +++ q) q" + have "homotopic_paths S (linepath (pathfinish q) (pathfinish q) +++ q) q" using \path q\ homotopic_paths_lid qloop piq by auto - hence 1: "\f. homotopic_paths s f q \ \ homotopic_paths s f (linepath (pathfinish q) (pathfinish q) +++ q)" + hence 1: "\f. homotopic_paths S f q \ \ homotopic_paths S f (linepath (pathfinish q) (pathfinish q) +++ q)" using homotopic_paths_trans by blast - hence "homotopic_paths s (linepath (pathfinish q) (pathfinish q) +++ q +++ linepath (pathfinish q) (pathfinish q)) q" - proof - - have "homotopic_paths s (q +++ linepath (pathfinish q) (pathfinish q)) q" - by (simp add: \path q\ homotopic_paths_rid piq) - thus ?thesis - by (metis (no_types) 1 \path q\ homotopic_paths_join homotopic_paths_rinv homotopic_paths_sym - homotopic_paths_trans qloop pathfinish_linepath piq) - qed + hence "homotopic_paths S (linepath (pathfinish q) (pathfinish q) +++ q +++ linepath (pathfinish q) (pathfinish q)) q" + by (smt (verit, best) \path q\ homotopic_paths_imp_path homotopic_paths_imp_subset homotopic_paths_lid + homotopic_paths_rid homotopic_paths_trans pathstart_join piq qloop) thus ?thesis by (metis (no_types) qloop homotopic_loops_sym homotopic_paths_imp_homotopic_loops homotopic_paths_imp_pathfinish homotopic_paths_sym) qed ultimately show ?thesis by (blast intro: homotopic_loops_trans) qed lemma homotopic_paths_loop_parts: assumes loops: "homotopic_loops S (p +++ reversepath q) (linepath a a)" and "path q" shows "homotopic_paths S p q" proof - have paths: "homotopic_paths S (p +++ reversepath q) (linepath (pathstart p) (pathstart p))" using homotopic_loops_imp_homotopic_paths_null [OF loops] by simp then have "path p" using \path q\ homotopic_loops_imp_path loops path_join path_join_path_ends path_reversepath by blast show ?thesis proof (cases "pathfinish p = pathfinish q") case True - have pipq: "path_image p \ S" "path_image q \ S" + obtain pipq: "path_image p \ S" "path_image q \ S" by (metis Un_subset_iff paths \path p\ \path q\ homotopic_loops_imp_subset homotopic_paths_imp_path loops - path_image_join path_image_reversepath path_imp_reversepath path_join_eq)+ + path_image_join path_image_reversepath path_imp_reversepath path_join_eq) have "homotopic_paths S p (p +++ (linepath (pathfinish p) (pathfinish p)))" using \path p\ \path_image p \ S\ homotopic_paths_rid homotopic_paths_sym by blast moreover have "homotopic_paths S (p +++ (linepath (pathfinish p) (pathfinish p))) (p +++ (reversepath q +++ q))" by (simp add: True \path p\ \path q\ pipq homotopic_paths_join homotopic_paths_linv homotopic_paths_sym) moreover have "homotopic_paths S (p +++ (reversepath q +++ q)) ((p +++ reversepath q) +++ q)" by (simp add: True \path p\ \path q\ homotopic_paths_assoc pipq) moreover have "homotopic_paths S ((p +++ reversepath q) +++ q) (linepath (pathstart p) (pathstart p) +++ q)" by (simp add: \path q\ homotopic_paths_join paths pipq) - moreover then have "homotopic_paths S (linepath (pathstart p) (pathstart p) +++ q) q" - by (metis \path q\ homotopic_paths_imp_path homotopic_paths_lid linepath_trivial path_join_path_ends pathfinish_def pipq(2)) ultimately show ?thesis - using homotopic_paths_trans by metis + by (metis \path q\ homotopic_paths_imp_path homotopic_paths_lid homotopic_paths_trans path_join_path_ends pathfinish_linepath pipq(2)) next case False then show ?thesis using \path q\ homotopic_loops_imp_path loops path_join_path_ends by fastforce qed qed subsection\<^marker>\tag unimportant\\Homotopy of "nearby" function, paths and loops\ lemma homotopic_with_linear: fixes f g :: "_ \ 'b::real_normed_vector" assumes contf: "continuous_on S f" and contg:"continuous_on S g" and sub: "\x. x \ S \ closed_segment (f x) (g x) \ t" shows "homotopic_with_canon (\z. True) S t f g" unfolding homotopic_with_def apply (rule_tac x="\y. ((1 - (fst y)) *\<^sub>R f(snd y) + (fst y) *\<^sub>R g(snd y))" in exI) using sub closed_segment_def by (fastforce intro: continuous_intros continuous_on_subset [OF contf] continuous_on_compose2 [where g=f] continuous_on_subset [OF contg] continuous_on_compose2 [where g=g]) lemma homotopic_paths_linear: fixes g h :: "real \ 'a::real_normed_vector" assumes "path g" "path h" "pathstart h = pathstart g" "pathfinish h = pathfinish g" "\t. t \ {0..1} \ closed_segment (g t) (h t) \ S" shows "homotopic_paths S g h" using assms unfolding path_def apply (simp add: closed_segment_def pathstart_def pathfinish_def homotopic_paths_def homotopic_with_def) apply (rule_tac x="\y. ((1 - (fst y)) *\<^sub>R (g \ snd) y + (fst y) *\<^sub>R (h \ snd) y)" in exI) apply (intro conjI subsetI continuous_intros; force) done lemma homotopic_loops_linear: fixes g h :: "real \ 'a::real_normed_vector" assumes "path g" "path h" "pathfinish g = pathstart g" "pathfinish h = pathstart h" "\t x. t \ {0..1} \ closed_segment (g t) (h t) \ S" shows "homotopic_loops S g h" using assms unfolding path_defs homotopic_loops_def homotopic_with_def apply (rule_tac x="\y. ((1 - (fst y)) *\<^sub>R g(snd y) + (fst y) *\<^sub>R h(snd y))" in exI) by (force simp: closed_segment_def intro!: continuous_intros intro: continuous_on_compose2 [where g=g] continuous_on_compose2 [where g=h]) lemma homotopic_paths_nearby_explicit: assumes \
: "path g" "path h" "pathstart h = pathstart g" "pathfinish h = pathfinish g" and no: "\t x. \t \ {0..1}; x \ S\ \ norm(h t - g t) < norm(g t - x)" shows "homotopic_paths S g h" -proof (rule homotopic_paths_linear [OF \
]) - show "\t. t \ {0..1} \ closed_segment (g t) (h t) \ S" - by (metis no segment_bound(1) subsetI norm_minus_commute not_le) -qed + using homotopic_paths_linear [OF \
] by (metis linorder_not_le no norm_minus_commute segment_bound1 subsetI) lemma homotopic_loops_nearby_explicit: assumes \
: "path g" "path h" "pathfinish g = pathstart g" "pathfinish h = pathstart h" and no: "\t x. \t \ {0..1}; x \ S\ \ norm(h t - g t) < norm(g t - x)" shows "homotopic_loops S g h" -proof (rule homotopic_loops_linear [OF \
]) - show "\t. t \ {0..1} \ closed_segment (g t) (h t) \ S" - by (metis no segment_bound(1) subsetI norm_minus_commute not_le) -qed + using homotopic_loops_linear [OF \
] by (metis linorder_not_le no norm_minus_commute segment_bound1 subsetI) lemma homotopic_nearby_paths: fixes g h :: "real \ 'a::euclidean_space" assumes "path g" "open S" "path_image g \ S" shows "\e. 0 < e \ (\h. path h \ pathstart h = pathstart g \ pathfinish h = pathfinish g \ (\t \ {0..1}. norm(h t - g t) < e) \ homotopic_paths S g h)" proof - obtain e where "e > 0" and e: "\x y. x \ path_image g \ y \ - S \ e \ dist x y" using separate_compact_closed [of "path_image g" "-S"] assms by force show ?thesis using e [unfolded dist_norm] \e > 0\ by (fastforce simp: path_image_def intro!: homotopic_paths_nearby_explicit assms exI) qed lemma homotopic_nearby_loops: fixes g h :: "real \ 'a::euclidean_space" assumes "path g" "open S" "path_image g \ S" "pathfinish g = pathstart g" shows "\e. 0 < e \ (\h. path h \ pathfinish h = pathstart h \ (\t \ {0..1}. norm(h t - g t) < e) \ homotopic_loops S g h)" proof - obtain e where "e > 0" and e: "\x y. x \ path_image g \ y \ - S \ e \ dist x y" using separate_compact_closed [of "path_image g" "-S"] assms by force show ?thesis using e [unfolded dist_norm] \e > 0\ by (fastforce simp: path_image_def intro!: homotopic_loops_nearby_explicit assms exI) qed subsection\ Homotopy and subpaths\ lemma homotopic_join_subpaths1: - assumes "path g" and pag: "path_image g \ s" + assumes "path g" and pag: "path_image g \ S" and u: "u \ {0..1}" and v: "v \ {0..1}" and w: "w \ {0..1}" "u \ v" "v \ w" - shows "homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)" + shows "homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)" proof - have 1: "t * 2 \ 1 \ u + t * (v * 2) \ v + t * (u * 2)" for t using affine_ineq \u \ v\ by fastforce have 2: "t * 2 > 1 \ u + (2*t - 1) * v \ v + (2*t - 1) * w" for t by (metis add_mono_thms_linordered_semiring(1) diff_gt_0_iff_gt less_eq_real_def mult.commute mult_right_mono \u \ v\ \v \ w\) have t2: "\t::real. t*2 = 1 \ t = 1/2" by auto have "homotopic_paths (path_image g) (subpath u v g +++ subpath v w g) (subpath u w g)" proof (cases "w = u") case True then show ?thesis by (metis \path g\ homotopic_paths_rinv path_image_subpath_subset path_subpath pathstart_subpath reversepath_subpath subpath_refl u v) next case False let ?f = "\t. if t \ 1/2 then inverse((w - u)) *\<^sub>R (2 * (v - u)) *\<^sub>R t else inverse((w - u)) *\<^sub>R ((v - u) + (w - v) *\<^sub>R (2 *\<^sub>R t - 1))" show ?thesis proof (rule homotopic_paths_sym [OF homotopic_paths_reparametrize [where f = ?f]]) show "path (subpath u w g)" using assms(1) path_subpath u w(1) by blast show "path_image (subpath u w g) \ path_image g" by (meson path_image_subpath_subset u w(1)) show "continuous_on {0..1} ?f" unfolding split_01 by (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def dest!: t2)+ show "?f ` {0..1} \ {0..1}" using False assms by (force simp: field_simps not_le mult_left_mono affine_ineq dest!: 1 2) show "(subpath u v g +++ subpath v w g) t = subpath u w g (?f t)" if "t \ {0..1}" for t using assms unfolding joinpaths_def subpath_def by (auto simp add: divide_simps add.commute mult.commute mult.left_commute) qed (use False in auto) qed then show ?thesis by (rule homotopic_paths_subset [OF _ pag]) qed lemma homotopic_join_subpaths2: - assumes "homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)" - shows "homotopic_paths s (subpath w v g +++ subpath v u g) (subpath w u g)" -by (metis assms homotopic_paths_reversepath_D pathfinish_subpath pathstart_subpath reversepath_joinpaths reversepath_subpath) + assumes "homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)" + shows "homotopic_paths S (subpath w v g +++ subpath v u g) (subpath w u g)" + by (metis assms homotopic_paths_reversepath_D pathfinish_subpath pathstart_subpath reversepath_joinpaths reversepath_subpath) lemma homotopic_join_subpaths3: - assumes hom: "homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)" - and "path g" and pag: "path_image g \ s" + assumes hom: "homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)" + and "path g" and pag: "path_image g \ S" and u: "u \ {0..1}" and v: "v \ {0..1}" and w: "w \ {0..1}" - shows "homotopic_paths s (subpath v w g +++ subpath w u g) (subpath v u g)" + shows "homotopic_paths S (subpath v w g +++ subpath w u g) (subpath v u g)" proof - - have "homotopic_paths s (subpath u w g +++ subpath w v g) ((subpath u v g +++ subpath v w g) +++ subpath w v g)" - proof (rule homotopic_paths_join) - show "homotopic_paths s (subpath u w g) (subpath u v g +++ subpath v w g)" - using hom homotopic_paths_sym_eq by blast - show "homotopic_paths s (subpath w v g) (subpath w v g)" - by (metis \path g\ homotopic_paths_eq pag path_image_subpath_subset path_subpath subset_trans v w) - qed auto - also have "homotopic_paths s ((subpath u v g +++ subpath v w g) +++ subpath w v g) (subpath u v g +++ subpath v w g +++ subpath w v g)" - by (rule homotopic_paths_sym [OF homotopic_paths_assoc]) - (use assms in \simp_all add: path_image_subpath_subset [THEN order_trans]\) - also have "homotopic_paths s (subpath u v g +++ subpath v w g +++ subpath w v g) + obtain wvg: "path (subpath w v g)" "path_image (subpath w v g) \ S" + and wug: "path (subpath w u g)" "path_image (subpath w u g) \ S" + and vug: "path (subpath v u g)" "path_image (subpath v u g) \ S" + by (meson \path g\ pag path_image_subpath_subset path_subpath subset_trans u v w) + have "homotopic_paths S (subpath u w g +++ subpath w v g) + ((subpath u v g +++ subpath v w g) +++ subpath w v g)" + by (simp add: hom homotopic_paths_join homotopic_paths_sym wvg) + also have "homotopic_paths S ((subpath u v g +++ subpath v w g) +++ subpath w v g) + (subpath u v g +++ subpath v w g +++ subpath w v g)" + using wvg vug \path g\ + by (metis homotopic_paths_assoc homotopic_paths_sym path_image_subpath_commute path_subpath + pathfinish_subpath pathstart_subpath u v w) + also have "homotopic_paths S (subpath u v g +++ subpath v w g +++ subpath w v g) (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g)))" - proof (rule homotopic_paths_join; simp) - show "path (subpath u v g) \ path_image (subpath u v g) \ s" - by (metis \path g\ order.trans pag path_image_subpath_subset path_subpath u v) - show "homotopic_paths s (subpath v w g +++ subpath w v g) (linepath (g v) (g v))" - by (metis (no_types, lifting) \path g\ homotopic_paths_linv order_trans pag path_image_subpath_subset path_subpath pathfinish_subpath reversepath_subpath v w) - qed - also have "homotopic_paths s (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g))) (subpath u v g)" - proof (rule homotopic_paths_rid) - show "path (subpath u v g)" - using \path g\ path_subpath u v by blast - show "path_image (subpath u v g) \ s" - by (meson \path g\ order.trans pag path_image_subpath_subset u v) - qed - finally have "homotopic_paths s (subpath u w g +++ subpath w v g) (subpath u v g)" . + using wvg vug \path g\ + by (metis homotopic_paths_join homotopic_paths_linv homotopic_paths_refl path_image_subpath_commute + path_subpath pathfinish_subpath pathstart_join pathstart_subpath reversepath_subpath u v) + also have "homotopic_paths S (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g))) (subpath u v g)" + using vug \path g\ by (metis homotopic_paths_rid path_image_subpath_commute path_subpath u v) + finally have "homotopic_paths S (subpath u w g +++ subpath w v g) (subpath u v g)" . then show ?thesis using homotopic_join_subpaths2 by blast qed proposition homotopic_join_subpaths: - "\path g; path_image g \ s; u \ {0..1}; v \ {0..1}; w \ {0..1}\ - \ homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)" - using le_cases3 [of u v w] homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3 - by metis + "\path g; path_image g \ S; u \ {0..1}; v \ {0..1}; w \ {0..1}\ + \ homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)" + by (smt (verit, del_insts) homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3) text\Relating homotopy of trivial loops to path-connectedness.\ lemma path_component_imp_homotopic_points: assumes "path_component S a b" shows "homotopic_loops S (linepath a a) (linepath b b)" proof - obtain g :: "real \ 'a" where g: "continuous_on {0..1} g" "g ` {0..1} \ S" "g 0 = a" "g 1 = b" using assms by (auto simp: path_defs) then have "continuous_on ({0..1} \ {0..1}) (g \ fst)" by (fastforce intro!: continuous_intros)+ with g show ?thesis by (auto simp add: homotopic_loops_def homotopic_with_def path_defs image_subset_iff) qed lemma homotopic_loops_imp_path_component_value: "\homotopic_loops S p q; 0 \ t; t \ 1\ \ path_component S (p t) (q t)" apply (clarsimp simp add: homotopic_loops_def homotopic_with_def path_defs) apply (rule_tac x="h \ (\u. (u, t))" in exI) apply (fastforce elim!: continuous_on_subset intro!: continuous_intros) done lemma homotopic_points_eq_path_component: "homotopic_loops S (linepath a a) (linepath b b) \ path_component S a b" by (auto simp: path_component_imp_homotopic_points dest: homotopic_loops_imp_path_component_value [where t=1]) lemma path_connected_eq_homotopic_points: "path_connected S \ (\a b. a \ S \ b \ S \ homotopic_loops S (linepath a a) (linepath b b))" by (auto simp: path_connected_def path_component_def homotopic_points_eq_path_component) subsection\Simply connected sets\ text\<^marker>\tag important\\defined as "all loops are homotopic (as loops)\ definition\<^marker>\tag important\ simply_connected where "simply_connected S \ \p q. path p \ pathfinish p = pathstart p \ path_image p \ S \ path q \ pathfinish q = pathstart q \ path_image q \ S \ homotopic_loops S p q" lemma simply_connected_empty [iff]: "simply_connected {}" by (simp add: simply_connected_def) lemma simply_connected_imp_path_connected: fixes S :: "_::real_normed_vector set" shows "simply_connected S \ path_connected S" by (simp add: simply_connected_def path_connected_eq_homotopic_points) lemma simply_connected_imp_connected: fixes S :: "_::real_normed_vector set" shows "simply_connected S \ connected S" by (simp add: path_connected_imp_connected simply_connected_imp_path_connected) lemma simply_connected_eq_contractible_loop_any: fixes S :: "_::real_normed_vector set" shows "simply_connected S \ (\p a. path p \ path_image p \ S \ pathfinish p = pathstart p \ a \ S \ homotopic_loops S p (linepath a a))" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs unfolding simply_connected_def by force next assume ?rhs then show ?lhs unfolding simply_connected_def by (metis pathfinish_in_path_image subsetD homotopic_loops_trans homotopic_loops_sym) qed lemma simply_connected_eq_contractible_loop_some: fixes S :: "_::real_normed_vector set" shows "simply_connected S \ path_connected S \ (\p. path p \ path_image p \ S \ pathfinish p = pathstart p \ (\a. a \ S \ homotopic_loops S p (linepath a a)))" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs using simply_connected_eq_contractible_loop_any by (blast intro: simply_connected_imp_path_connected) next assume r: ?rhs note pa = r [THEN conjunct2, rule_format] show ?lhs proof (clarsimp simp add: simply_connected_eq_contractible_loop_any) fix p a assume "path p" and "path_image p \ S" "pathfinish p = pathstart p" and "a \ S" with pa [of p] show "homotopic_loops S p (linepath a a)" using homotopic_loops_trans path_connected_eq_homotopic_points r by blast qed qed lemma simply_connected_eq_contractible_loop_all: fixes S :: "_::real_normed_vector set" shows "simply_connected S \ S = {} \ (\a \ S. \p. path p \ path_image p \ S \ pathfinish p = pathstart p \ homotopic_loops S p (linepath a a))" (is "?lhs = ?rhs") proof (cases "S = {}") case True then show ?thesis by force next case False then obtain a where "a \ S" by blast show ?thesis proof assume "simply_connected S" then show ?rhs using \a \ S\ \simply_connected S\ simply_connected_eq_contractible_loop_any by blast next assume ?rhs then show "simply_connected S" unfolding simply_connected_eq_contractible_loop_any by (meson False homotopic_loops_refl homotopic_loops_sym homotopic_loops_trans path_component_imp_homotopic_points path_component_refl) qed qed lemma simply_connected_eq_contractible_path: fixes S :: "_::real_normed_vector set" shows "simply_connected S \ path_connected S \ (\p. path p \ path_image p \ S \ pathfinish p = pathstart p \ homotopic_paths S p (linepath (pathstart p) (pathstart p)))" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs unfolding simply_connected_imp_path_connected by (metis simply_connected_eq_contractible_loop_some homotopic_loops_imp_homotopic_paths_null) next assume ?rhs then show ?lhs using homotopic_paths_imp_homotopic_loops simply_connected_eq_contractible_loop_some by fastforce qed lemma simply_connected_eq_homotopic_paths: fixes S :: "_::real_normed_vector set" shows "simply_connected S \ path_connected S \ (\p q. path p \ path_image p \ S \ path q \ path_image q \ S \ pathstart q = pathstart p \ pathfinish q = pathfinish p \ homotopic_paths S p q)" (is "?lhs = ?rhs") proof assume ?lhs then have pc: "path_connected S" and *: "\p. \path p; path_image p \ S; pathfinish p = pathstart p\ \ homotopic_paths S p (linepath (pathstart p) (pathstart p))" by (auto simp: simply_connected_eq_contractible_path) have "homotopic_paths S p q" if "path p" "path_image p \ S" "path q" "path_image q \ S" "pathstart q = pathstart p" "pathfinish q = pathfinish p" for p q proof - have "homotopic_paths S p (p +++ linepath (pathfinish p) (pathfinish p))" by (simp add: homotopic_paths_rid homotopic_paths_sym that) also have "homotopic_paths S (p +++ linepath (pathfinish p) (pathfinish p)) (p +++ reversepath q +++ q)" using that by (metis homotopic_paths_join homotopic_paths_linv homotopic_paths_refl homotopic_paths_sym_eq pathstart_linepath) also have "homotopic_paths S (p +++ reversepath q +++ q) ((p +++ reversepath q) +++ q)" by (simp add: that homotopic_paths_assoc) also have "homotopic_paths S ((p +++ reversepath q) +++ q) (linepath (pathstart q) (pathstart q) +++ q)" using * [of "p +++ reversepath q"] that by (simp add: homotopic_paths_join path_image_join) also have "homotopic_paths S (linepath (pathstart q) (pathstart q) +++ q) q" using that homotopic_paths_lid by blast finally show ?thesis . qed then show ?rhs by (blast intro: pc *) next assume ?rhs then show ?lhs by (force simp: simply_connected_eq_contractible_path) qed proposition simply_connected_Times: fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" assumes S: "simply_connected S" and T: "simply_connected T" shows "simply_connected(S \ T)" proof - have "homotopic_loops (S \ T) p (linepath (a, b) (a, b))" if "path p" "path_image p \ S \ T" "p 1 = p 0" "a \ S" "b \ T" for p a b proof - have "path (fst \ p)" by (simp add: continuous_on_fst Path_Connected.path_continuous_image [OF \path p\]) moreover have "path_image (fst \ p) \ S" using that by (force simp add: path_image_def) ultimately have p1: "homotopic_loops S (fst \ p) (linepath a a)" using S that by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def) have "path (snd \ p)" by (simp add: continuous_on_snd Path_Connected.path_continuous_image [OF \path p\]) moreover have "path_image (snd \ p) \ T" using that by (force simp: path_image_def) ultimately have p2: "homotopic_loops T (snd \ p) (linepath b b)" using T that by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def) show ?thesis using p1 p2 unfolding homotopic_loops apply clarify subgoal for h k by (rule_tac x="\z. (h z, k z)" in exI) (force intro: continuous_intros simp: path_defs) done qed with assms show ?thesis by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def) qed subsection\Contractible sets\ definition\<^marker>\tag important\ contractible where "contractible S \ \a. homotopic_with_canon (\x. True) S S id (\x. a)" proposition contractible_imp_simply_connected: fixes S :: "_::real_normed_vector set" assumes "contractible S" shows "simply_connected S" proof (cases "S = {}") case True then show ?thesis by force next case False obtain a where a: "homotopic_with_canon (\x. True) S S id (\x. a)" using assms by (force simp: contractible_def) then have "a \ S" by (metis False homotopic_constant_maps homotopic_with_symD homotopic_with_trans path_component_in_topspace topspace_euclidean_subtopology) have "\p. path p \ path_image p \ S \ pathfinish p = pathstart p \ homotopic_loops S p (linepath a a)" using a apply (clarsimp simp add: homotopic_loops_def homotopic_with_def path_defs) apply (rule_tac x="(h \ (\y. (fst y, (p \ snd) y)))" in exI) apply (intro conjI continuous_on_compose continuous_intros; force elim: continuous_on_subset) done with \a \ S\ show ?thesis by (auto simp add: simply_connected_eq_contractible_loop_all False) qed corollary contractible_imp_connected: fixes S :: "_::real_normed_vector set" shows "contractible S \ connected S" by (simp add: contractible_imp_simply_connected simply_connected_imp_connected) lemma contractible_imp_path_connected: fixes S :: "_::real_normed_vector set" shows "contractible S \ path_connected S" by (simp add: contractible_imp_simply_connected simply_connected_imp_path_connected) lemma nullhomotopic_through_contractible: fixes S :: "_::topological_space set" assumes f: "continuous_on S f" "f ` S \ T" and g: "continuous_on T g" "g ` T \ U" and T: "contractible T" obtains c where "homotopic_with_canon (\h. True) S U (g \ f) (\x. c)" proof - obtain b where b: "homotopic_with_canon (\x. True) T T id (\x. b)" using assms by (force simp: contractible_def) have "homotopic_with_canon (\f. True) T U (g \ id) (g \ (\x. b))" by (metis Abstract_Topology.continuous_map_subtopology_eu b g homotopic_with_compose_continuous_map_left) then have "homotopic_with_canon (\f. True) S U (g \ id \ f) (g \ (\x. b) \ f)" by (simp add: f homotopic_with_compose_continuous_map_right) then show ?thesis by (simp add: comp_def that) qed lemma nullhomotopic_into_contractible: assumes f: "continuous_on S f" "f ` S \ T" and T: "contractible T" obtains c where "homotopic_with_canon (\h. True) S T f (\x. c)" by (rule nullhomotopic_through_contractible [OF f, of id T]) (use assms in auto) lemma nullhomotopic_from_contractible: assumes f: "continuous_on S f" "f ` S \ T" and S: "contractible S" obtains c where "homotopic_with_canon (\h. True) S T f (\x. c)" by (auto simp: comp_def intro: nullhomotopic_through_contractible [OF continuous_on_id _ f S]) lemma homotopic_through_contractible: fixes S :: "_::real_normed_vector set" assumes "continuous_on S f1" "f1 ` S \ T" "continuous_on T g1" "g1 ` T \ U" "continuous_on S f2" "f2 ` S \ T" "continuous_on T g2" "g2 ` T \ U" "contractible T" "path_connected U" shows "homotopic_with_canon (\h. True) S U (g1 \ f1) (g2 \ f2)" proof - obtain c1 where c1: "homotopic_with_canon (\h. True) S U (g1 \ f1) (\x. c1)" by (rule nullhomotopic_through_contractible [of S f1 T g1 U]) (use assms in auto) obtain c2 where c2: "homotopic_with_canon (\h. True) S U (g2 \ f2) (\x. c2)" by (rule nullhomotopic_through_contractible [of S f2 T g2 U]) (use assms in auto) have "S = {} \ (\t. path_connected t \ t \ U \ c2 \ t \ c1 \ t)" proof (cases "S = {}") case True then show ?thesis by force next case False with c1 c2 have "c1 \ U" "c2 \ U" using homotopic_with_imp_continuous_maps by fastforce+ with \path_connected U\ show ?thesis by blast qed then have "homotopic_with_canon (\h. True) S U (\x. c2) (\x. c1)" by (simp add: path_component homotopic_constant_maps) then show ?thesis using c1 c2 homotopic_with_symD homotopic_with_trans by blast qed lemma homotopic_into_contractible: fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set" assumes f: "continuous_on S f" "f ` S \ T" and g: "continuous_on S g" "g ` S \ T" and T: "contractible T" shows "homotopic_with_canon (\h. True) S T f g" using homotopic_through_contractible [of S f T id T g id] by (simp add: assms contractible_imp_path_connected) lemma homotopic_from_contractible: fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set" assumes f: "continuous_on S f" "f ` S \ T" and g: "continuous_on S g" "g ` S \ T" and "contractible S" "path_connected T" shows "homotopic_with_canon (\h. True) S T f g" using homotopic_through_contractible [of S id S f T id g] by (simp add: assms contractible_imp_path_connected) subsection\Starlike sets\ definition\<^marker>\tag important\ "starlike S \ (\a\S. \x\S. closed_segment a x \ S)" lemma starlike_UNIV [simp]: "starlike UNIV" by (simp add: starlike_def) lemma convex_imp_starlike: "convex S \ S \ {} \ starlike S" unfolding convex_contains_segment starlike_def by auto lemma starlike_convex_tweak_boundary_points: fixes S :: "'a::euclidean_space set" assumes "convex S" "S \ {}" and ST: "rel_interior S \ T" and TS: "T \ closure S" shows "starlike T" proof - have "rel_interior S \ {}" by (simp add: assms rel_interior_eq_empty) then obtain a where a: "a \ rel_interior S" by blast with ST have "a \ T" by blast have "\x. x \ T \ open_segment a x \ rel_interior S" by (rule rel_interior_closure_convex_segment [OF \convex S\ a]) (use assms in auto) then have "\x\T. a \ T \ open_segment a x \ T" using ST by (blast intro: a \a \ T\ rel_interior_closure_convex_segment [OF \convex S\ a]) then show ?thesis unfolding starlike_def using bexI [OF _ \a \ T\] by (simp add: closed_segment_eq_open) qed lemma starlike_imp_contractible_gen: fixes S :: "'a::real_normed_vector set" assumes S: "starlike S" and P: "\a T. \a \ S; 0 \ T; T \ 1\ \ P(\x. (1 - T) *\<^sub>R x + T *\<^sub>R a)" obtains a where "homotopic_with_canon P S S (\x. x) (\x. a)" proof - obtain a where "a \ S" and a: "\x. x \ S \ closed_segment a x \ S" using S by (auto simp: starlike_def) have "\t b. 0 \ t \ t \ 1 \ \u. (1 - t) *\<^sub>R b + t *\<^sub>R a = (1 - u) *\<^sub>R a + u *\<^sub>R b \ 0 \ u \ u \ 1" by (metis add_diff_cancel_right' diff_ge_0_iff_ge le_add_diff_inverse pth_c(1)) then have "(\y. (1 - fst y) *\<^sub>R snd y + fst y *\<^sub>R a) ` ({0..1} \ S) \ S" using a [unfolded closed_segment_def] by force then have "homotopic_with_canon P S S (\x. x) (\x. a)" using \a \ S\ unfolding homotopic_with_def apply (rule_tac x="\y. (1 - (fst y)) *\<^sub>R snd y + (fst y) *\<^sub>R a" in exI) apply (force simp add: P intro: continuous_intros) done then show ?thesis using that by blast qed lemma starlike_imp_contractible: fixes S :: "'a::real_normed_vector set" shows "starlike S \ contractible S" using starlike_imp_contractible_gen contractible_def by (fastforce simp: id_def) lemma contractible_UNIV [simp]: "contractible (UNIV :: 'a::real_normed_vector set)" by (simp add: starlike_imp_contractible) lemma starlike_imp_simply_connected: fixes S :: "'a::real_normed_vector set" shows "starlike S \ simply_connected S" by (simp add: contractible_imp_simply_connected starlike_imp_contractible) lemma convex_imp_simply_connected: fixes S :: "'a::real_normed_vector set" shows "convex S \ simply_connected S" using convex_imp_starlike starlike_imp_simply_connected by blast lemma starlike_imp_path_connected: fixes S :: "'a::real_normed_vector set" shows "starlike S \ path_connected S" by (simp add: simply_connected_imp_path_connected starlike_imp_simply_connected) lemma starlike_imp_connected: fixes S :: "'a::real_normed_vector set" shows "starlike S \ connected S" by (simp add: path_connected_imp_connected starlike_imp_path_connected) lemma is_interval_simply_connected_1: fixes S :: "real set" shows "is_interval S \ simply_connected S" using convex_imp_simply_connected is_interval_convex_1 is_interval_path_connected_1 simply_connected_imp_path_connected by auto lemma contractible_empty [simp]: "contractible {}" by (simp add: contractible_def homotopic_on_emptyI) lemma contractible_convex_tweak_boundary_points: fixes S :: "'a::euclidean_space set" assumes "convex S" and TS: "rel_interior S \ T" "T \ closure S" shows "contractible T" proof (cases "S = {}") case True with assms show ?thesis by (simp add: subsetCE) next case False show ?thesis by (meson False assms starlike_convex_tweak_boundary_points starlike_imp_contractible) qed lemma convex_imp_contractible: fixes S :: "'a::real_normed_vector set" shows "convex S \ contractible S" using contractible_empty convex_imp_starlike starlike_imp_contractible by blast lemma contractible_sing [simp]: fixes a :: "'a::real_normed_vector" shows "contractible {a}" by (rule convex_imp_contractible [OF convex_singleton]) lemma is_interval_contractible_1: fixes S :: "real set" shows "is_interval S \ contractible S" using contractible_imp_simply_connected convex_imp_contractible is_interval_convex_1 is_interval_simply_connected_1 by auto lemma contractible_Times: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes S: "contractible S" and T: "contractible T" shows "contractible (S \ T)" proof - obtain a h where conth: "continuous_on ({0..1} \ S) h" and hsub: "h ` ({0..1} \ S) \ S" and [simp]: "\x. x \ S \ h (0, x) = x" and [simp]: "\x. x \ S \ h (1::real, x) = a" using S by (auto simp: contractible_def homotopic_with) obtain b k where contk: "continuous_on ({0..1} \ T) k" and ksub: "k ` ({0..1} \ T) \ T" and [simp]: "\x. x \ T \ k (0, x) = x" and [simp]: "\x. x \ T \ k (1::real, x) = b" using T by (auto simp: contractible_def homotopic_with) show ?thesis apply (simp add: contractible_def homotopic_with) apply (rule exI [where x=a]) apply (rule exI [where x=b]) apply (rule exI [where x = "\z. (h (fst z, fst(snd z)), k (fst z, snd(snd z)))"]) using hsub ksub apply (fastforce intro!: continuous_intros continuous_on_compose2 [OF conth] continuous_on_compose2 [OF contk]) done qed subsection\Local versions of topological properties in general\ definition\<^marker>\tag important\ locally :: "('a::topological_space set \ bool) \ 'a set \ bool" where "locally P S \ \w x. openin (top_of_set S) w \ x \ w \ (\u v. openin (top_of_set S) u \ P v \ x \ u \ u \ v \ v \ w)" lemma locallyI: assumes "\w x. \openin (top_of_set S) w; x \ w\ \ \u v. openin (top_of_set S) u \ P v \ x \ u \ u \ v \ v \ w" shows "locally P S" using assms by (force simp: locally_def) lemma locallyE: assumes "locally P S" "openin (top_of_set S) w" "x \ w" obtains u v where "openin (top_of_set S) u" "P v" "x \ u" "u \ v" "v \ w" using assms unfolding locally_def by meson lemma locally_mono: assumes "locally P S" "\T. P T \ Q T" shows "locally Q S" by (metis assms locally_def) lemma locally_open_subset: assumes "locally P S" "openin (top_of_set S) t" shows "locally P t" using assms unfolding locally_def by (elim all_forward) (meson dual_order.trans openin_imp_subset openin_subset_trans openin_trans) lemma locally_diff_closed: "\locally P S; closedin (top_of_set S) t\ \ 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} \ P {a}" proof - have "\x::real. \ 0 < x \ P {a}" using zero_less_one by blast then show ?thesis unfolding locally_def by (auto simp add: openin_euclidean_subtopology_iff subset_singleton_iff conj_disj_distribR) qed lemma locally_iff: "locally P S \ (\T x. open T \ x \ S \ T \ (\U. open U \ (\V. P V \ x \ S \ U \ S \ U \ V \ V \ S \ 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: "\S T. P S \ P T \ P(S \ T)" shows "locally P (S \ T)" unfolding locally_iff proof clarify fix A x assume "open A" "x \ A" "x \ S" "x \ T" then obtain U1 V1 U2 V2 where "open U1" "P V1" "x \ S \ U1" "S \ U1 \ V1 \ V1 \ S \ A" "open U2" "P V2" "x \ T \ U2" "T \ U2 \ V2 \ V2 \ T \ A" using S T unfolding locally_iff by (meson IntI) then have "S \ T \ (U1 \ U2) \ V1 \ V2" "V1 \ V2 \ S \ T \ A" "x \ S \ T \ (U1 \ U2)" by blast+ moreover have "P (V1 \ V2)" by (simp add: P \P V1\ \P V2\) ultimately show "\U. open U \ (\V. P V \ x \ S \ T \ U \ S \ T \ U \ V \ V \ S \ T \ A)" using \open U1\ \open U2\ by blast qed lemma locally_Times: fixes S :: "('a::metric_space) set" and T :: "('b::metric_space) set" assumes PS: "locally P S" and QT: "locally Q T" and R: "\S T. P S \ Q T \ R(S \ T)" shows "locally R (S \ T)" unfolding locally_def proof (clarify) fix W x y assume W: "openin (top_of_set (S \ T)) W" and xy: "(x, y) \ W" then obtain U V where "openin (top_of_set S) U" "x \ U" "openin (top_of_set T) V" "y \ V" "U \ V \ W" using Times_in_interior_subtopology by metis then obtain U1 U2 V1 V2 where opeS: "openin (top_of_set S) U1 \ P U2 \ x \ U1 \ U1 \ U2 \ U2 \ U" and opeT: "openin (top_of_set T) V1 \ Q V2 \ y \ V1 \ V1 \ V2 \ V2 \ V" by (meson PS QT locallyE) then have "openin (top_of_set (S \ T)) (U1 \ V1)" by (simp add: openin_Times) moreover have "R (U2 \ V2)" by (simp add: R opeS opeT) moreover have "U1 \ V1 \ U2 \ V2 \ U2 \ V2 \ W" using opeS opeT \U \ V \ W\ by auto ultimately show "\U V. openin (top_of_set (S \ T)) U \ R V \ (x,y) \ U \ U \ V \ V \ W" using opeS opeT by auto qed 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: "\S S'. \P S; homeomorphism S S' f g\ \ Q S'" shows "locally Q T" proof (clarsimp simp: locally_def) fix W y assume "y \ W" and "openin (top_of_set T) W" then obtain A where T: "open A" "W = T \ A" by (force simp: openin_open) then have "W \ T" by auto have f: "\x. x \ S \ g(f x) = x" "f ` S = T" "continuous_on S f" and g: "\y. y \ T \ f(g y) = y" "g ` T = S" "continuous_on T g" using hom by (auto simp: homeomorphism_def) have gw: "g ` W = S \ f -` W" using \W \ T\ g by force have \: "openin (top_of_set S) (g ` W)" proof - have "continuous_on S f" using f(3) by blast then show "openin (top_of_set S) (g ` W)" by (simp add: gw Collect_conj_eq \openin (top_of_set T) W\ continuous_on_open f(2)) qed then obtain U V where osu: "openin (top_of_set S) U" and uv: "P V" "g y \ U" "U \ V" "V \ g ` W" using S [unfolded locally_def, rule_format, of "g ` W" "g y"] \y \ W\ by force have "V \ S" using uv by (simp add: gw) have fv: "f ` V = T \ {x. g x \ V}" using \f ` S = T\ f \V \ S\ by auto have "f ` V \ W" using uv using Int_lower2 gw image_subsetI mem_Collect_eq subset_iff by auto have contvf: "continuous_on V f" using \V \ S\ continuous_on_subset f(3) by blast have contvg: "continuous_on (f ` V) g" using \f ` V \ W\ \W \ T\ continuous_on_subset [OF g(3)] by blast have "V \ g ` f ` V" by (metis \V \ S\ hom homeomorphism_def homeomorphism_of_subsets order_refl) then have homv: "homeomorphism V (f ` V) f g" using \V \ S\ f by (auto simp add: homeomorphism_def contvf contvg) have "openin (top_of_set (g ` T)) U" using \g ` T = S\ by (simp add: osu) then have 1: "openin (top_of_set T) (T \ g -` U)" using \continuous_on T g\ continuous_on_open [THEN iffD1] by blast have 2: "\V. Q V \ y \ (T \ g -` U) \ (T \ g -` U) \ V \ V \ W" proof (intro exI conjI) show "Q (f ` V)" using Q homv \P V\ by blast show "y \ T \ g -` U" using T(2) \y \ W\ \g y \ U\ by blast show "T \ g -` U \ f ` V" using g(1) image_iff uv(3) by fastforce show "f ` V \ W" using \f ` V \ W\ by blast qed show "\U. openin (top_of_set T) U \ (\v. Q v \ y \ U \ U \ v \ v \ W)" by (meson 1 2) qed lemma homeomorphism_locally: fixes f:: "'a::metric_space \ 'b::metric_space" assumes hom: "homeomorphism S T f g" and eq: "\S T. homeomorphism S T f g \ (P S \ Q T)" shows "locally P S \ locally Q T" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs using eq hom homeomorphism_locally_imp by blast next assume ?rhs then show ?lhs using eq homeomorphism_sym homeomorphism_symD [OF hom] by (blast intro: homeomorphism_locally_imp) qed lemma homeomorphic_locally: fixes S:: "'a::metric_space set" and T:: "'b::metric_space set" assumes hom: "S homeomorphic T" and iff: "\X Y. X homeomorphic Y \ (P X \ Q Y)" shows "locally P S \ locally Q T" proof - obtain f g where hom: "homeomorphism S T f g" using assms by (force simp: homeomorphic_def) then show ?thesis using homeomorphic_def local.iff by (blast intro!: homeomorphism_locally) qed lemma homeomorphic_local_compactness: fixes S:: "'a::metric_space set" and T:: "'b::metric_space set" shows "S homeomorphic T \ locally compact S \ locally compact T" by (simp add: homeomorphic_compactness homeomorphic_locally) lemma locally_translation: fixes P :: "'a :: real_normed_vector set \ bool" shows "(\S. P ((+) a ` S) = P S) \ locally P ((+) a ` S) = locally P S" using homeomorphism_locally [OF homeomorphism_translation] by (metis (full_types) homeomorphism_image2) lemma locally_injective_linear_image: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes f: "linear f" "inj f" and iff: "\S. P (f ` S) \ Q S" shows "locally P (f ` S) \ locally Q S" using homeomorphism_locally [of "f`S" _ _ f] linear_homeomorphism_image [OF f] by (metis (no_types, lifting) homeomorphism_image2 iff) lemma locally_open_map_image: fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector" assumes P: "locally P S" and f: "continuous_on S f" and oo: "\T. openin (top_of_set S) T \ openin (top_of_set (f ` S)) (f ` T)" and Q: "\T. \T \ S; P T\ \ Q(f ` T)" shows "locally Q (f ` S)" proof (clarsimp simp add: locally_def) fix W y assume oiw: "openin (top_of_set (f ` S)) W" and "y \ W" then have "W \ f ` S" by (simp add: openin_euclidean_subtopology_iff) have oivf: "openin (top_of_set S) (S \ f -` W)" by (rule continuous_on_open [THEN iffD1, rule_format, OF f oiw]) then obtain x where "x \ S" "f x = y" using \W \ f ` S\ \y \ W\ by blast then obtain U V where "openin (top_of_set S) U" "P V" "x \ U" "U \ V" "V \ S \ f -` W" using P [unfolded locally_def, rule_format, of "(S \ f -` W)" x] oivf \y \ W\ by auto then have "openin (top_of_set (f ` S)) (f ` U)" by (simp add: oo) then show "\X. openin (top_of_set (f ` S)) X \ (\Y. Q Y \ y \ X \ X \ Y \ Y \ W)" using Q \P V\ \U \ V\ \V \ S \ f -` W\ \f x = y\ \x \ U\ by blast qed subsection\An induction principle for connected sets\ proposition connected_induction: assumes "connected S" and opD: "\T a. \openin (top_of_set S) T; a \ T\ \ \z. z \ T \ P z" and opI: "\a. a \ S \ \T. openin (top_of_set S) T \ a \ T \ (\x \ T. \y \ T. P x \ P y \ Q x \ Q y)" and etc: "a \ S" "b \ S" "P a" "P b" "Q a" shows "Q b" proof - let ?A = "{b. \T. openin (top_of_set S) T \ b \ T \ (\x\T. P x \ Q x)}" let ?B = "{b. \T. openin (top_of_set S) T \ b \ T \ (\x\T. P x \ \ Q x)}" have 1: "openin (top_of_set S) ?A" by (subst openin_subopen, blast) have 2: "openin (top_of_set S) ?B" by (subst openin_subopen, blast) have \
: "?A \ ?B = {}" by (clarsimp simp: set_eq_iff) (metis (no_types, opaque_lifting) Int_iff opD openin_Int) have *: "S \ ?A \ ?B" by clarsimp (meson opI) have "?A = {} \ ?B = {}" using \connected S\ [unfolded connected_openin, simplified, rule_format, OF 1 \
* 2] by blast then show ?thesis by clarsimp (meson opI etc) qed lemma connected_equivalence_relation_gen: assumes "connected S" and etc: "a \ S" "b \ S" "P a" "P b" and trans: "\x y z. \R x y; R y z\ \ R x z" and opD: "\T a. \openin (top_of_set S) T; a \ T\ \ \z. z \ T \ P z" and opI: "\a. a \ S \ \T. openin (top_of_set S) T \ a \ T \ (\x \ T. \y \ T. P x \ P y \ R x y)" shows "R a b" proof - have "\a b c. \a \ S; P a; b \ S; c \ S; P b; P c; R a b\ \ R a c" apply (rule connected_induction [OF \connected S\ opD], simp_all) by (meson trans opI) then show ?thesis by (metis etc opI) qed lemma connected_induction_simple: assumes "connected S" and etc: "a \ S" "b \ S" "P a" and opI: "\a. a \ S \ \T. openin (top_of_set S) T \ a \ T \ (\x \ T. \y \ T. P x \ P y)" shows "P b" by (rule connected_induction [OF \connected S\ _, where P = "\x. True"]) (use opI etc in auto) lemma connected_equivalence_relation: assumes "connected S" and etc: "a \ S" "b \ S" and sym: "\x y. \R x y; x \ S; y \ S\ \ R y x" and trans: "\x y z. \R x y; R y z; x \ S; y \ S; z \ S\ \ R x z" and opI: "\a. a \ S \ \T. openin (top_of_set S) T \ a \ T \ (\x \ T. R a x)" shows "R a b" proof - have "\a b c. \a \ S; b \ S; c \ S; R a b\ \ R a c" apply (rule connected_induction_simple [OF \connected S\], simp_all) by (meson local.sym local.trans opI openin_imp_subset subsetCE) then show ?thesis by (metis etc opI) qed lemma locally_constant_imp_constant: assumes "connected S" and opI: "\a. a \ S \ \T. openin (top_of_set S) T \ a \ T \ (\x \ T. f x = f a)" shows "f constant_on S" proof - have "\x y. x \ S \ y \ S \ f x = f y" apply (rule connected_equivalence_relation [OF \connected S\], simp_all) by (metis opI) then show ?thesis by (metis constant_on_def) qed lemma locally_constant: assumes "connected S" shows "locally (\U. f constant_on U) S \ f constant_on S" (is "?lhs = ?rhs") proof assume ?lhs then have "\a. a \ S \ \T. openin (top_of_set S) T \ a \ T \ (\x\T. f x = f a)" unfolding locally_def by (metis (mono_tags, opaque_lifting) constant_on_def constant_on_subset openin_subtopology_self) then show ?rhs using assms by (simp add: locally_constant_imp_constant) next assume ?rhs then show ?lhs using assms by (metis constant_on_subset locallyI openin_imp_subset order_refl) qed subsection\Basic properties of local compactness\ proposition locally_compact: - fixes s :: "'a :: metric_space set" + fixes S :: "'a :: metric_space set" shows - "locally compact s \ - (\x \ s. \u v. x \ u \ u \ v \ v \ s \ - openin (top_of_set s) u \ compact v)" + "locally compact S \ + (\x \ S. \u v. x \ u \ u \ v \ v \ S \ + openin (top_of_set S) u \ compact v)" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (meson locallyE openin_subtopology_self) next assume r [rule_format]: ?rhs have *: "\u v. - openin (top_of_set s) u \ - compact v \ x \ u \ u \ v \ v \ s \ T" - if "open T" "x \ s" "x \ T" for x T + openin (top_of_set S) u \ + compact v \ x \ u \ u \ v \ v \ S \ T" + if "open T" "x \ S" "x \ T" for x T proof - - obtain u v where uv: "x \ u" "u \ v" "v \ s" "compact v" "openin (top_of_set s) u" - using r [OF \x \ s\] by auto + obtain u v where uv: "x \ u" "u \ v" "v \ S" "compact v" "openin (top_of_set S) u" + using r [OF \x \ S\] by auto obtain e where "e>0" and e: "cball x e \ T" using open_contains_cball \open T\ \x \ T\ by blast show ?thesis - apply (rule_tac x="(s \ ball x e) \ u" in exI) + apply (rule_tac x="(S \ ball x e) \ u" in exI) apply (rule_tac x="cball x e \ v" in exI) using that \e > 0\ e uv apply auto done qed show ?lhs by (rule locallyI) (metis "*" Int_iff openin_open) qed lemma locally_compactE: fixes S :: "'a :: metric_space set" assumes "locally compact S" obtains u v where "\x. x \ S \ x \ u x \ u x \ v x \ v x \ S \ openin (top_of_set S) (u x) \ compact (v x)" using assms unfolding locally_compact by metis lemma locally_compact_alt: fixes S :: "'a :: heine_borel set" shows "locally compact S \ (\x \ S. \U. x \ U \ openin (top_of_set S) U \ compact(closure U) \ closure U \ S)" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (meson bounded_subset closure_minimal compact_closure compact_imp_bounded compact_imp_closed dual_order.trans locally_compactE) next assume ?rhs then show ?lhs by (meson closure_subset locally_compact) qed lemma locally_compact_Int_cball: fixes S :: "'a :: heine_borel set" shows "locally compact S \ (\x \ S. \e. 0 < e \ closed(cball x e \ S))" (is "?lhs = ?rhs") proof assume L: ?lhs then have "\x U V e. \U \ V; V \ S; compact V; 0 < e; cball x e \ S \ U\ \ closed (cball x e \ S)" by (metis compact_Int compact_cball compact_imp_closed inf.absorb_iff2 inf.assoc inf.orderE) with L show ?rhs by (meson locally_compactE openin_contains_cball) next assume R: ?rhs show ?lhs unfolding locally_compact proof fix x assume "x \ S" then obtain e where "e>0" and e: "closed (cball x e \ S)" using R by blast then have "compact (cball x e \ S)" by (simp add: bounded_Int compact_eq_bounded_closed) moreover have "\y\ball x e \ S. \\>0. cball y \ \ S \ ball x e" by (meson Elementary_Metric_Spaces.open_ball IntD1 le_infI1 open_contains_cball_eq) moreover have "openin (top_of_set S) (ball x e \ S)" by (simp add: inf_commute openin_open_Int) ultimately show "\U V. x \ U \ U \ V \ V \ S \ openin (top_of_set S) U \ compact V" by (metis Int_iff \0 < e\ \x \ S\ ball_subset_cball centre_in_ball inf_commute inf_le1 inf_mono order_refl) qed qed lemma locally_compact_compact: fixes S :: "'a :: heine_borel set" shows "locally compact S \ (\K. K \ S \ compact K \ (\U V. K \ U \ U \ V \ V \ S \ openin (top_of_set S) U \ compact V))" (is "?lhs = ?rhs") proof assume ?lhs then obtain u v where uv: "\x. x \ S \ x \ u x \ u x \ v x \ v x \ S \ openin (top_of_set S) (u x) \ compact (v x)" by (metis locally_compactE) have *: "\U V. K \ U \ U \ V \ V \ S \ openin (top_of_set S) U \ compact V" if "K \ S" "compact K" for K proof - have "\C. (\c\C. openin (top_of_set K) c) \ K \ \C \ \D\C. finite D \ K \ \D" using that by (simp add: compact_eq_openin_cover) moreover have "\c \ (\x. K \ u x) ` K. openin (top_of_set K) c" using that by clarify (metis subsetD inf.absorb_iff2 openin_subset openin_subtopology_Int_subset topspace_euclidean_subtopology uv) moreover have "K \ \((\x. K \ u x) ` K)" using that by clarsimp (meson subsetCE uv) ultimately obtain D where "D \ (\x. K \ u x) ` K" "finite D" "K \ \D" by metis then obtain T where T: "T \ K" "finite T" "K \ \((\x. K \ u x) ` T)" by (metis finite_subset_image) have Tuv: "\(u ` T) \ \(v ` T)" using T that by (force dest!: uv) moreover have "openin (top_of_set S) (\ (u ` T))" using T that uv by fastforce moreover have "compact (\ (v ` T))" by (meson T compact_UN subset_eq that(1) uv) moreover have "\ (v ` T) \ S" by (metis SUP_least T(1) subset_eq that(1) uv) ultimately show ?thesis using T by auto 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 *: "\U V. x \ U \ U \ V \ V \ S \ openin (top_of_set S) U \ compact V" if "x \ S" for x proof - obtain e where "e>0" and e: "cball x e \ S" using open_contains_cball assms \x \ S\ by blast have ope: "openin (top_of_set S) (ball x e)" by (meson e open_ball ball_subset_cball dual_order.trans open_subset) show ?thesis proof (intro exI conjI) let ?U = "ball x e" let ?V = "cball x e" show "x \ ?U" "?U \ ?V" "?V \ S" "compact ?V" using \e > 0\ e by auto show "openin (top_of_set S) ?U" using ope by blast qed 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 *: "\U V. x \ U \ U \ V \ V \ S \ openin (top_of_set S) U \ compact V" if "x \ S" for x apply (rule_tac x = "S \ ball x 1" in exI, rule_tac x = "S \ cball x 1" in exI) using \x \ S\ assms by auto 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 "\locally compact S; locally compact t\ \ locally compact (S \ t)" by (simp add: compact_Int locally_Int) lemma locally_compact_closedin: fixes S :: "'a :: heine_borel set" shows "\closedin (top_of_set S) t; locally compact S\ \ 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 \ 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 \ locally compact S" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs unfolding locally_def apply (elim all_forward imp_forward asm_rl exE) apply (rule_tac x = "u \ ball x 1" in exI) apply (rule_tac x = "v \ 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 lemma locally_compact_openin_Un: fixes S :: "'a::euclidean_space set" assumes LCS: "locally compact S" and LCT:"locally compact T" and opS: "openin (top_of_set (S \ T)) S" and opT: "openin (top_of_set (S \ T)) T" shows "locally compact (S \ T)" proof - have "\e>0. closed (cball x e \ (S \ T))" if "x \ S" for x proof - obtain e1 where "e1 > 0" and e1: "closed (cball x e1 \ S)" using LCS \x \ S\ unfolding locally_compact_Int_cball by blast moreover obtain e2 where "e2 > 0" and e2: "cball x e2 \ (S \ T) \ S" by (meson \x \ S\ opS openin_contains_cball) then have "cball x e2 \ (S \ T) = cball x e2 \ S" by force ultimately have "closed (cball x (min e1 e2) \ (S \ T))" by (metis (no_types, lifting) cball_min_Int closed_Int closed_cball inf_assoc inf_commute) then show ?thesis by (metis \0 < e1\ \0 < e2\ min_def) qed moreover have "\e>0. closed (cball x e \ (S \ T))" if "x \ T" for x proof - obtain e1 where "e1 > 0" and e1: "closed (cball x e1 \ T)" using LCT \x \ T\ unfolding locally_compact_Int_cball by blast moreover obtain e2 where "e2 > 0" and e2: "cball x e2 \ (S \ T) \ T" by (meson \x \ T\ opT openin_contains_cball) then have "cball x e2 \ (S \ T) = cball x e2 \ T" by force moreover have "closed (cball x e1 \ (cball x e2 \ T))" by (metis closed_Int closed_cball e1 inf_left_commute) ultimately show ?thesis by (rule_tac x="min e1 e2" in exI) (simp add: \0 < e2\ cball_min_Int inf_assoc) qed ultimately show ?thesis by (force simp: locally_compact_Int_cball) qed lemma locally_compact_closedin_Un: fixes S :: "'a::euclidean_space set" assumes LCS: "locally compact S" and LCT:"locally compact T" and clS: "closedin (top_of_set (S \ T)) S" and clT: "closedin (top_of_set (S \ T)) T" shows "locally compact (S \ T)" proof - have "\e>0. closed (cball x e \ (S \ T))" if "x \ S" "x \ T" for x proof - obtain e1 where "e1 > 0" and e1: "closed (cball x e1 \ S)" using LCS \x \ S\ unfolding locally_compact_Int_cball by blast moreover obtain e2 where "e2 > 0" and e2: "closed (cball x e2 \ T)" using LCT \x \ T\ unfolding locally_compact_Int_cball by blast moreover have "closed (cball x (min e1 e2) \ (S \ T))" proof - have "closed (cball x e1 \ (cball x e2 \ S))" by (metis closed_Int closed_cball e1 inf_left_commute) then show ?thesis by (simp add: Int_Un_distrib cball_min_Int closed_Int closed_Un e2 inf_assoc) qed ultimately show ?thesis by (rule_tac x="min e1 e2" in exI) linarith qed moreover have "\e>0. closed (cball x e \ (S \ T))" if x: "x \ S" "x \ T" for x proof - obtain e1 where "e1 > 0" and e1: "closed (cball x e1 \ S)" using LCS \x \ S\ unfolding locally_compact_Int_cball by blast moreover obtain e2 where "e2>0" and "cball x e2 \ (S \ T) \ S - T" using clT x by (fastforce simp: openin_contains_cball closedin_def) then have "closed (cball x e2 \ T)" proof - have "{} = T - (T - cball x e2)" using Diff_subset Int_Diff \cball x e2 \ (S \ T) \ S - T\ by auto then show ?thesis by (simp add: Diff_Diff_Int inf_commute) qed with e1 have "closed ((cball x e1 \ cball x e2) \ (S \ T))" apply (simp add: inf_commute inf_sup_distrib2) by (metis closed_Int closed_Un closed_cball inf_assoc inf_left_commute) then have "closed (cball x (min e1 e2) \ (S \ T))" by (simp add: cball_min_Int inf_commute) ultimately show ?thesis using \0 < e2\ by (rule_tac x="min e1 e2" in exI) linarith qed moreover have "\e>0. closed (cball x e \ (S \ T))" if x: "x \ S" "x \ T" for x proof - obtain e1 where "e1 > 0" and e1: "closed (cball x e1 \ T)" using LCT \x \ T\ unfolding locally_compact_Int_cball by blast moreover obtain e2 where "e2>0" and "cball x e2 \ (S \ T) \ S \ T - S" using clS x by (fastforce simp: openin_contains_cball closedin_def) then have "closed (cball x e2 \ S)" by (metis Diff_disjoint Int_empty_right closed_empty inf.left_commute inf.orderE inf_sup_absorb) with e1 have "closed ((cball x e1 \ cball x e2) \ (S \ T))" apply (simp add: inf_commute inf_sup_distrib2) by (metis closed_Int closed_Un closed_cball inf_assoc inf_left_commute) then have "closed (cball x (min e1 e2) \ (S \ T))" by (auto simp: cball_min_Int) ultimately show ?thesis using \0 < e2\ by (rule_tac x="min e1 e2" in exI) linarith qed ultimately show ?thesis by (auto simp: locally_compact_Int_cball) qed lemma locally_compact_Times: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" shows "\locally compact S; locally compact T\ \ locally compact (S \ T)" by (auto simp: compact_Times locally_Times) lemma locally_compact_compact_subopen: fixes S :: "'a :: heine_borel set" shows "locally compact S \ (\K T. K \ S \ compact K \ open T \ K \ T \ (\U V. K \ U \ U \ V \ U \ T \ V \ S \ openin (top_of_set S) U \ compact V))" (is "?lhs = ?rhs") proof assume L: ?lhs show ?rhs proof clarify fix K :: "'a set" and T :: "'a set" assume "K \ S" and "compact K" and "open T" and "K \ T" obtain U V where "K \ U" "U \ V" "V \ S" "compact V" and ope: "openin (top_of_set S) U" using L unfolding locally_compact_compact by (meson \K \ S\ \compact K\) show "\U V. K \ U \ U \ V \ U \ T \ V \ S \ openin (top_of_set S) U \ compact V" proof (intro exI conjI) show "K \ U \ T" by (simp add: \K \ T\ \K \ U\) show "U \ T \ closure(U \ T)" by (rule closure_subset) show "closure (U \ T) \ S" by (metis \U \ V\ \V \ S\ \compact V\ closure_closed closure_mono compact_imp_closed inf.cobounded1 subset_trans) show "openin (top_of_set S) (U \ T)" by (simp add: \open T\ ope openin_Int_open) show "compact (closure (U \ T))" by (meson Int_lower1 \U \ V\ \compact V\ bounded_subset compact_closure compact_eq_bounded_closed) qed auto qed next assume ?rhs then show ?lhs unfolding locally_compact_compact by (metis open_openin openin_topspace subtopology_superset top.extremum topspace_euclidean_subtopology) qed subsection\Sura-Bura's results about compact components of sets\ proposition Sura_Bura_compact: fixes S :: "'a::euclidean_space set" assumes "compact S" and C: "C \ components S" shows "C = \{T. C \ T \ openin (top_of_set S) T \ closedin (top_of_set S) T}" (is "C = \?\") proof obtain x where x: "C = connected_component_set S x" and "x \ S" using C by (auto simp: components_def) have "C \ S" by (simp add: C in_components_subset) have "\?\ \ connected_component_set S x" proof (rule connected_component_maximal) have "x \ C" by (simp add: \x \ S\ x) then show "x \ \?\" by blast have clo: "closed (\?\)" by (simp add: \compact S\ closed_Inter closedin_compact_eq compact_imp_closed) have False if K1: "closedin (top_of_set (\?\)) K1" and K2: "closedin (top_of_set (\?\)) K2" and K12_Int: "K1 \ K2 = {}" and K12_Un: "K1 \ K2 = \?\" and "K1 \ {}" "K2 \ {}" for K1 K2 proof - have "closed K1" "closed K2" using closedin_closed_trans clo K1 K2 by blast+ then obtain V1 V2 where "open V1" "open V2" "K1 \ V1" "K2 \ V2" and V12: "V1 \ V2 = {}" using separation_normal \K1 \ K2 = {}\ by metis have SV12_ne: "(S - (V1 \ V2)) \ (\?\) \ {}" proof (rule compact_imp_fip) show "compact (S - (V1 \ V2))" by (simp add: \open V1\ \open V2\ \compact S\ compact_diff open_Un) show clo\: "closed T" if "T \ ?\" for T using that \compact S\ by (force intro: closedin_closed_trans simp add: compact_imp_closed) show "(S - (V1 \ V2)) \ \\ \ {}" if "finite \" and \: "\ \ ?\" for \ proof assume djo: "(S - (V1 \ V2)) \ \\ = {}" obtain D where opeD: "openin (top_of_set S) D" and cloD: "closedin (top_of_set S) D" and "C \ D" and DV12: "D \ V1 \ V2" proof (cases "\ = {}") case True with \C \ S\ djo that show ?thesis by force next case False show ?thesis proof show ope: "openin (top_of_set S) (\\)" using openin_Inter \finite \\ False \ by blast then show "closedin (top_of_set S) (\\)" by (meson clo\ \ closed_Inter closed_subset openin_imp_subset subset_eq) show "C \ \\" using \ by auto show "\\ \ V1 \ V2" using ope djo openin_imp_subset by fastforce qed qed have "connected C" by (simp add: x) have "closed D" using \compact S\ cloD closedin_closed_trans compact_imp_closed by blast have cloV1: "closedin (top_of_set D) (D \ closure V1)" and cloV2: "closedin (top_of_set D) (D \ closure V2)" by (simp_all add: closedin_closed_Int) moreover have "D \ closure V1 = D \ V1" "D \ closure V2 = D \ V2" using \D \ V1 \ V2\ \open V1\ \open V2\ V12 by (auto simp add: closure_subset [THEN subsetD] closure_iff_nhds_not_empty, blast+) ultimately have cloDV1: "closedin (top_of_set D) (D \ V1)" and cloDV2: "closedin (top_of_set D) (D \ V2)" by metis+ then obtain U1 U2 where "closed U1" "closed U2" and D1: "D \ V1 = D \ U1" and D2: "D \ V2 = D \ U2" by (auto simp: closedin_closed) have "D \ U1 \ C \ {}" proof assume "D \ U1 \ C = {}" then have *: "C \ D \ V2" using D1 DV12 \C \ D\ by auto have 1: "openin (top_of_set S) (D \ V2)" by (simp add: \open V2\ opeD openin_Int_open) have 2: "closedin (top_of_set S) (D \ V2)" using cloD cloDV2 closedin_trans by blast have "\ ?\ \ D \ V2" by (rule Inter_lower) (use * 1 2 in simp) then show False using K1 V12 \K1 \ {}\ \K1 \ V1\ closedin_imp_subset by blast qed moreover have "D \ U2 \ C \ {}" proof assume "D \ U2 \ C = {}" then have *: "C \ D \ V1" using D2 DV12 \C \ D\ by auto have 1: "openin (top_of_set S) (D \ V1)" by (simp add: \open V1\ opeD openin_Int_open) have 2: "closedin (top_of_set S) (D \ V1)" using cloD cloDV1 closedin_trans by blast have "\?\ \ D \ V1" by (rule Inter_lower) (use * 1 2 in simp) then show False using K2 V12 \K2 \ {}\ \K2 \ V2\ closedin_imp_subset by blast qed ultimately show False using \connected C\ [unfolded connected_closed, simplified, rule_format, of concl: "D \ U1" "D \ U2"] using \C \ D\ D1 D2 V12 DV12 \closed U1\ \closed U2\ \closed D\ by blast qed qed show False by (metis (full_types) DiffE UnE Un_upper2 SV12_ne \K1 \ V1\ \K2 \ V2\ disjoint_iff_not_equal subsetCE sup_ge1 K12_Un) qed then show "connected (\?\)" by (auto simp: connected_closedin_eq) show "\?\ \ S" by (fastforce simp: C in_components_subset) qed with x show "\?\ \ C" by simp qed auto corollary Sura_Bura_clopen_subset: fixes S :: "'a::euclidean_space set" assumes S: "locally compact S" and C: "C \ components S" and "compact C" and U: "open U" "C \ U" obtains K where "openin (top_of_set S) K" "compact K" "C \ K" "K \ U" proof (rule ccontr) assume "\ thesis" with that have neg: "\K. openin (top_of_set S) K \ compact K \ C \ K \ K \ U" by metis obtain V K where "C \ V" "V \ U" "V \ K" "K \ S" "compact K" and opeSV: "openin (top_of_set S) V" using S U \compact C\ by (meson C in_components_subset locally_compact_compact_subopen) let ?\ = "{T. C \ T \ openin (top_of_set K) T \ compact T \ T \ K}" have CK: "C \ components K" by (meson C \C \ V\ \K \ S\ \V \ K\ components_intermediate_subset subset_trans) with \compact K\ have "C = \{T. C \ T \ openin (top_of_set K) T \ closedin (top_of_set K) T}" by (simp add: Sura_Bura_compact) then have Ceq: "C = \?\" by (simp add: closedin_compact_eq \compact K\) obtain W where "open W" and W: "V = S \ W" using opeSV by (auto simp: openin_open) have "-(U \ W) \ \?\ \ {}" proof (rule closed_imp_fip_compact) show "- (U \ W) \ \\ \ {}" if "finite \" and \: "\ \ ?\" for \ proof (cases "\ = {}") case True have False if "U = UNIV" "W = UNIV" proof - have "V = S" by (simp add: W \W = UNIV\) with neg show False using \C \ V\ \K \ S\ \V \ K\ \V \ U\ \compact K\ by auto qed with True show ?thesis by auto next case False show ?thesis proof assume "- (U \ W) \ \\ = {}" then have FUW: "\\ \ U \ W" by blast have "C \ \\" using \ by auto moreover have "compact (\\)" by (metis (no_types, lifting) compact_Inter False mem_Collect_eq subsetCE \) moreover have "\\ \ K" using False that(2) by fastforce moreover have opeKF: "openin (top_of_set K) (\\)" using False \ \finite \\ by blast then have opeVF: "openin (top_of_set V) (\\)" using W \K \ S\ \V \ K\ opeKF \\\ \ K\ FUW openin_subset_trans by fastforce then have "openin (top_of_set S) (\\)" by (metis opeSV openin_trans) moreover have "\\ \ U" by (meson \V \ U\ opeVF dual_order.trans openin_imp_subset) ultimately show False using neg by blast qed qed qed (use \open W\ \open U\ in auto) with W Ceq \C \ V\ \C \ U\ show False by auto qed corollary Sura_Bura_clopen_subset_alt: fixes S :: "'a::euclidean_space set" assumes S: "locally compact S" and C: "C \ components S" and "compact C" and opeSU: "openin (top_of_set S) U" and "C \ U" obtains K where "openin (top_of_set S) K" "compact K" "C \ K" "K \ U" proof - obtain V where "open V" "U = S \ V" using opeSU by (auto simp: openin_open) with \C \ U\ have "C \ V" by auto then show ?thesis using Sura_Bura_clopen_subset [OF S C \compact C\ \open V\] by (metis \U = S \ V\ inf.bounded_iff openin_imp_subset that) qed corollary Sura_Bura: fixes S :: "'a::euclidean_space set" assumes "locally compact S" "C \ components S" "compact C" shows "C = \ {K. C \ K \ compact K \ openin (top_of_set S) K}" (is "C = ?rhs") proof show "?rhs \ C" proof (clarsimp, rule ccontr) fix x assume *: "\X. C \ X \ compact X \ openin (top_of_set S) X \ x \ X" and "x \ C" obtain U V where "open U" "open V" "{x} \ U" "C \ V" "U \ V = {}" using separation_normal [of "{x}" C] by (metis Int_empty_left \x \ C\ \compact C\ closed_empty closed_insert compact_imp_closed insert_disjoint(1)) have "x \ V" using \U \ V = {}\ \{x} \ U\ by blast then show False by (meson "*" Sura_Bura_clopen_subset \C \ V\ \open V\ assms(1) assms(2) assms(3) subsetCE) qed qed blast subsection\Special cases of local connectedness and path connectedness\ lemma locally_connected_1: assumes "\V x. \openin (top_of_set S) V; x \ V\ \ \U. openin (top_of_set S) U \ connected U \ x \ U \ U \ V" shows "locally connected S" by (metis assms locally_def) lemma locally_connected_2: assumes "locally connected S" "openin (top_of_set S) t" "x \ t" shows "openin (top_of_set S) (connected_component_set t x)" proof - { fix y :: 'a let ?SS = "top_of_set S" assume 1: "openin ?SS t" "\w x. openin ?SS w \ x \ w \ (\u. openin ?SS u \ (\v. connected v \ x \ u \ u \ v \ v \ w))" and "connected_component t x y" then have "y \ t" and y: "y \ connected_component_set t x" using connected_component_subset by blast+ obtain F where "\x y. (\w. openin ?SS w \ (\u. connected u \ x \ w \ w \ u \ u \ y)) = (openin ?SS (F x y) \ (\u. connected u \ x \ F x y \ F x y \ u \ u \ y))" by moura then obtain G where "\a A. (\U. openin ?SS U \ (\V. connected V \ a \ U \ U \ V \ V \ A)) = (openin ?SS (F a A) \ connected (G a A) \ a \ F a A \ F a A \ G a A \ G a A \ A)" by moura then have *: "openin ?SS (F y t) \ connected (G y t) \ y \ F y t \ F y t \ G y t \ G y t \ t" using 1 \y \ t\ by presburger have "G y t \ connected_component_set t y" by (metis (no_types) * connected_component_eq_self connected_component_mono contra_subsetD) then have "\A. openin ?SS A \ y \ A \ A \ 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 "\t x. \openin (top_of_set S) t; x \ t\ \ openin (top_of_set S) (connected_component_set t x)" "openin (top_of_set S) v" "x \ v" shows "\u. openin (top_of_set S) u \ connected u \ x \ u \ u \ v" using assms connected_component_subset by fastforce lemma locally_connected: "locally connected S \ (\v x. openin (top_of_set S) v \ x \ v \ (\u. openin (top_of_set S) u \ connected u \ x \ u \ u \ v))" by (metis locally_connected_1 locally_connected_2 locally_connected_3) lemma locally_connected_open_connected_component: "locally connected S \ (\t x. openin (top_of_set S) t \ x \ t \ openin (top_of_set S) (connected_component_set t x))" by (metis locally_connected_1 locally_connected_2 locally_connected_3) lemma locally_path_connected_1: assumes "\v x. \openin (top_of_set S) v; x \ v\ \ \u. openin (top_of_set S) u \ path_connected u \ x \ u \ u \ v" shows "locally path_connected S" by (force simp add: locally_def dest: assms) lemma locally_path_connected_2: assumes "locally path_connected S" "openin (top_of_set S) t" "x \ t" shows "openin (top_of_set S) (path_component_set t x)" proof - { fix y :: 'a let ?SS = "top_of_set S" assume 1: "openin ?SS t" "\w x. openin ?SS w \ x \ w \ (\u. openin ?SS u \ (\v. path_connected v \ x \ u \ u \ v \ v \ w))" and "path_component t x y" then have "y \ t" and y: "y \ path_component_set t x" using path_component_mem(2) by blast+ obtain F where "\x y. (\w. openin ?SS w \ (\u. path_connected u \ x \ w \ w \ u \ u \ y)) = (openin ?SS (F x y) \ (\u. path_connected u \ x \ F x y \ F x y \ u \ u \ y))" by moura then obtain G where "\a A. (\U. openin ?SS U \ (\V. path_connected V \ a \ U \ U \ V \ V \ A)) = (openin ?SS (F a A) \ path_connected (G a A) \ a \ F a A \ F a A \ G a A \ G a A \ A)" by moura then have *: "openin ?SS (F y t) \ path_connected (G y t) \ y \ F y t \ F y t \ G y t \ G y t \ t" using 1 \y \ t\ by presburger have "G y t \ path_component_set t y" using * path_component_maximal rev_subsetD by blast then have "\A. openin ?SS A \ y \ A \ A \ path_component_set t x" by (metis "*" \G y t \ path_component_set t y\ 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 "\t x. \openin (top_of_set S) t; x \ t\ \ openin (top_of_set S) (path_component_set t x)" "openin (top_of_set S) v" "x \ v" shows "\u. openin (top_of_set S) u \ path_connected u \ x \ u \ u \ v" proof - have "path_component v x x" by (meson assms(3) path_component_refl) then show ?thesis by (metis assms mem_Collect_eq path_component_subset path_connected_path_component) qed proposition locally_path_connected: "locally path_connected S \ (\V x. openin (top_of_set S) V \ x \ V \ (\U. openin (top_of_set S) U \ path_connected U \ x \ U \ U \ V))" by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3) proposition locally_path_connected_open_path_component: "locally path_connected S \ (\t x. openin (top_of_set S) t \ x \ t \ openin (top_of_set 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 \ (\t c. openin (top_of_set S) t \ c \ components t \ openin (top_of_set S) c)" by (metis components_iff locally_connected_open_connected_component) proposition locally_connected_im_kleinen: "locally connected S \ (\v x. openin (top_of_set S) v \ x \ v \ (\u. openin (top_of_set S) u \ x \ u \ u \ v \ (\y. y \ u \ (\c. connected c \ c \ v \ x \ c \ y \ c))))" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (fastforce simp add: locally_connected) next assume ?rhs have *: "\T. openin (top_of_set S) T \ x \ T \ T \ c" if "openin (top_of_set S) t" and c: "c \ components t" and "x \ c" for t c x proof - from that \?rhs\ [rule_format, of t x] obtain u where u: "openin (top_of_set S) u \ x \ u \ u \ t \ (\y. y \ u \ (\c. connected c \ c \ t \ x \ c \ y \ c))" using in_components_subset by auto obtain F :: "'a set \ 'a set \ 'a" where "\x y. (\z. z \ x \ y = connected_component_set x z) = (F x y \ x \ y = connected_component_set x (F x y))" by moura then have F: "F t c \ t \ c = connected_component_set t (F t c)" by (meson components_iff c) obtain G :: "'a set \ 'a set \ 'a" where G: "\x y. (\z. z \ y \ z \ x) = (G x y \ y \ G x y \ x)" by moura have "G c u \ u \ G c u \ 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 unfolding locally_connected_open_component by (meson "*" openin_subopen) qed proposition locally_path_connected_im_kleinen: "locally path_connected S \ (\v x. openin (top_of_set S) v \ x \ v \ (\u. openin (top_of_set S) u \ x \ u \ u \ v \ (\y. y \ u \ (\p. path p \ path_image p \ v \ pathstart p = x \ 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 *: "\T. openin (top_of_set S) T \ x \ T \ T \ path_component_set u z" if "openin (top_of_set S) u" and "z \ u" and c: "path_component u z x" for u z x proof - have "x \ u" by (meson c path_component_mem(2)) with that \?rhs\ [rule_format, of u x] obtain U where U: "openin (top_of_set S) U \ x \ U \ U \ u \ (\y. y \ U \ (\p. path p \ path_image p \ u \ pathstart p = x \ pathfinish p = y))" by blast show ?thesis by (metis U c mem_Collect_eq path_component_def path_component_eq subsetI) qed show ?lhs unfolding locally_path_connected_open_path_component using "*" openin_subopen by fastforce qed lemma locally_path_connected_imp_locally_connected: "locally path_connected S \ locally connected S" using locally_mono path_connected_imp_connected by blast lemma locally_connected_components: "\locally connected S; c \ components S\ \ locally connected c" by (meson locally_connected_open_component locally_open_subset openin_subtopology_self) lemma locally_path_connected_components: "\locally path_connected S; c \ components S\ \ 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 \ 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" assumes "open S" shows "locally path_connected S" proof (rule locally_mono) show "locally convex S" using assms unfolding locally_def by (meson open_ball centre_in_ball convex_ball openE open_subset openin_imp_subset openin_open_trans subset_trans) show "\T::'a set. convex T \ path_connected T" using convex_imp_path_connected by blast qed lemma open_imp_locally_connected: fixes S :: "'a :: real_normed_vector set" shows "open S \ 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 \ openin (top_of_set S) (connected_component_set S x)" by (metis connected_component_eq_empty locally_connected_2 openin_empty openin_subtopology_self) lemma openin_components_locally_connected: "\locally connected S; c \ components S\ \ openin (top_of_set S) c" using locally_connected_open_component openin_subtopology_self by blast lemma openin_path_component_locally_path_connected: "locally path_connected S \ openin (top_of_set 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: assumes "locally path_connected S" shows "closedin (top_of_set S) (path_component_set S x)" proof - have "openin (top_of_set S) (\ ({path_component_set S y |y. y \ S} - {path_component_set S x}))" using locally_path_connected_2 assms by fastforce then show ?thesis by (simp add: closedin_def path_component_subset complement_path_component_Union) qed lemma convex_imp_locally_path_connected: fixes S :: "'a:: real_normed_vector set" assumes "convex S" shows "locally path_connected S" proof (clarsimp simp add: locally_path_connected) fix V x assume "openin (top_of_set S) V" and "x \ V" then obtain T e where "V = S \ T" "x \ S" "0 < e" "ball x e \ T" by (metis Int_iff openE openin_open) then have "openin (top_of_set S) (S \ ball x e)" "path_connected (S \ ball x e)" by (simp_all add: assms convex_Int convex_imp_path_connected openin_open_Int) then show "\U. openin (top_of_set S) U \ path_connected U \ x \ U \ U \ V" using \0 < e\ \V = S \ T\ \ball x e \ T\ \x \ S\ by auto qed lemma convex_imp_locally_connected: fixes S :: "'a:: real_normed_vector set" shows "convex S \ locally connected S" by (simp add: locally_path_connected_imp_locally_connected convex_imp_locally_path_connected) subsection\Relations between components and path components\ lemma path_component_eq_connected_component: assumes "locally path_connected S" shows "(path_component S x = connected_component S x)" proof (cases "x \ S") case True have "openin (top_of_set (connected_component_set S x)) (path_component_set S x)" proof (rule openin_subset_trans) show "openin (top_of_set S) (path_component_set S x)" by (simp add: True assms locally_path_connected_2) show "connected_component_set S x \ S" by (simp add: connected_component_subset) qed (simp add: path_component_subset_connected_component) moreover have "closedin (top_of_set (connected_component_set S x)) (path_component_set S x)" proof (rule closedin_subset_trans [of S]) show "closedin (top_of_set S) (path_component_set S x)" by (simp add: assms closedin_path_component_locally_path_connected) show "connected_component_set S x \ S" by (simp add: connected_component_subset) qed (simp add: path_component_subset_connected_component) ultimately have *: "path_component_set S x = connected_component_set S x" by (metis connected_connected_component connected_clopen True path_component_eq_empty) then show ?thesis by blast next case False then show ?thesis by (metis Collect_empty_eq_bot connected_component_eq_empty path_component_eq_empty) qed lemma path_component_eq_connected_component_set: "locally path_connected S \ (path_component_set S x = connected_component_set S x)" by (simp add: path_component_eq_connected_component) lemma locally_path_connected_path_component: "locally path_connected S \ locally path_connected (path_component_set S x)" using locally_path_connected_connected_component path_component_eq_connected_component by fastforce lemma open_path_connected_component: fixes S :: "'a :: real_normed_vector set" shows "open S \ path_component S x = connected_component S x" by (simp add: path_component_eq_connected_component open_imp_locally_path_connected) lemma open_path_connected_component_set: fixes S :: "'a :: real_normed_vector set" shows "open S \ path_component_set S x = connected_component_set S x" by (simp add: open_path_connected_component) proposition locally_connected_quotient_image: assumes lcS: "locally connected S" and oo: "\T. T \ f ` S \ openin (top_of_set S) (S \ f -` T) \ openin (top_of_set (f ` S)) T" shows "locally connected (f ` S)" proof (clarsimp simp: locally_connected_open_component) fix U C assume opefSU: "openin (top_of_set (f ` S)) U" and "C \ components U" then have "C \ U" "U \ f ` S" by (meson in_components_subset openin_imp_subset)+ then have "openin (top_of_set (f ` S)) C \ openin (top_of_set S) (S \ f -` C)" by (auto simp: oo) moreover have "openin (top_of_set S) (S \ f -` C)" proof (subst openin_subopen, clarify) fix x assume "x \ S" "f x \ C" show "\T. openin (top_of_set S) T \ x \ T \ T \ (S \ f -` C)" proof (intro conjI exI) show "openin (top_of_set S) (connected_component_set (S \ f -` U) x)" proof (rule ccontr) assume **: "\ openin (top_of_set S) (connected_component_set (S \ f -` U) x)" then have "x \ (S \ f -` U)" using \U \ f ` S\ opefSU lcS locally_connected_2 oo by blast with ** show False by (metis (no_types) connected_component_eq_empty empty_iff openin_subopen) qed next show "x \ connected_component_set (S \ f -` U) x" using \C \ U\ \f x \ C\ \x \ S\ by auto next have contf: "continuous_on S f" by (simp add: continuous_on_open oo openin_imp_subset) then have "continuous_on (connected_component_set (S \ f -` U) x) f" by (meson connected_component_subset continuous_on_subset inf.boundedE) then have "connected (f ` connected_component_set (S \ f -` U) x)" by (rule connected_continuous_image [OF _ connected_connected_component]) moreover have "f ` connected_component_set (S \ f -` U) x \ U" using connected_component_in by blast moreover have "C \ f ` connected_component_set (S \ f -` U) x \ {}" using \C \ U\ \f x \ C\ \x \ S\ by fastforce ultimately have fC: "f ` (connected_component_set (S \ f -` U) x) \ C" by (rule components_maximal [OF \C \ components U\]) have cUC: "connected_component_set (S \ f -` U) x \ (S \ f -` C)" using connected_component_subset fC by blast have "connected_component_set (S \ f -` U) x \ connected_component_set (S \ f -` C) x" proof - { assume "x \ connected_component_set (S \ f -` U) x" then have ?thesis using cUC connected_component_idemp connected_component_mono by blast } then show ?thesis using connected_component_eq_empty by auto qed also have "\ \ (S \ f -` C)" by (rule connected_component_subset) finally show "connected_component_set (S \ f -` U) x \ (S \ f -` C)" . qed qed ultimately show "openin (top_of_set (f ` S)) C" by metis qed text\The proof resembles that above but is not identical!\ proposition locally_path_connected_quotient_image: assumes lcS: "locally path_connected S" and oo: "\T. T \ f ` S \ openin (top_of_set S) (S \ f -` T) \ openin (top_of_set (f ` S)) T" shows "locally path_connected (f ` S)" proof (clarsimp simp: locally_path_connected_open_path_component) fix U y assume opefSU: "openin (top_of_set (f ` S)) U" and "y \ U" then have "path_component_set U y \ U" "U \ f ` S" by (meson path_component_subset openin_imp_subset)+ then have "openin (top_of_set (f ` S)) (path_component_set U y) \ openin (top_of_set S) (S \ f -` path_component_set U y)" proof - have "path_component_set U y \ f ` S" using \U \ f ` S\ \path_component_set U y \ U\ by blast then show ?thesis using oo by blast qed moreover have "openin (top_of_set S) (S \ f -` path_component_set U y)" proof (subst openin_subopen, clarify) fix x assume "x \ S" and Uyfx: "path_component U y (f x)" then have "f x \ U" using path_component_mem by blast show "\T. openin (top_of_set S) T \ x \ T \ T \ (S \ f -` path_component_set U y)" proof (intro conjI exI) show "openin (top_of_set S) (path_component_set (S \ f -` U) x)" proof (rule ccontr) assume **: "\ openin (top_of_set S) (path_component_set (S \ f -` U) x)" then have "x \ (S \ f -` U)" by (metis (no_types, lifting) \U \ f ` S\ opefSU lcS oo locally_path_connected_open_path_component) then show False using ** \path_component_set U y \ U\ \x \ S\ \path_component U y (f x)\ by blast qed next show "x \ path_component_set (S \ f -` U) x" by (simp add: \f x \ U\ \x \ S\ path_component_refl) next have contf: "continuous_on S f" by (simp add: continuous_on_open oo openin_imp_subset) then have "continuous_on (path_component_set (S \ f -` U) x) f" by (meson Int_lower1 continuous_on_subset path_component_subset) then have "path_connected (f ` path_component_set (S \ f -` U) x)" by (simp add: path_connected_continuous_image) moreover have "f ` path_component_set (S \ f -` U) x \ U" using path_component_mem by fastforce moreover have "f x \ f ` path_component_set (S \ f -` U) x" by (force simp: \x \ S\ \f x \ U\ path_component_refl_eq) ultimately have "f ` (path_component_set (S \ f -` U) x) \ path_component_set U (f x)" by (meson path_component_maximal) also have "\ \ path_component_set U y" by (simp add: Uyfx path_component_maximal path_component_subset path_component_sym) finally have fC: "f ` (path_component_set (S \ f -` U) x) \ path_component_set U y" . have cUC: "path_component_set (S \ f -` U) x \ (S \ f -` path_component_set U y)" using path_component_subset fC by blast have "path_component_set (S \ f -` U) x \ path_component_set (S \ f -` path_component_set U y) x" proof - have "\a. path_component_set (path_component_set (S \ f -` U) x) a \ path_component_set (S \ f -` path_component_set U y) a" using cUC path_component_mono by blast then show ?thesis using path_component_path_component by blast qed also have "\ \ (S \ f -` path_component_set U y)" by (rule path_component_subset) finally show "path_component_set (S \ f -` U) x \ (S \ f -` path_component_set U y)" . qed qed ultimately show "openin (top_of_set (f ` S)) (path_component_set U y)" by metis qed subsection\<^marker>\tag unimportant\\Components, continuity, openin, closedin\ lemma continuous_on_components_gen: fixes f :: "'a::topological_space \ 'b::topological_space" assumes "\C. C \ components S \ openin (top_of_set S) C \ continuous_on C f" shows "continuous_on S f" proof (clarsimp simp: continuous_openin_preimage_eq) fix t :: "'b set" assume "open t" have *: "S \ f -` t = (\c \ components S. c \ f -` t)" by auto show "openin (top_of_set S) (S \ f -` t)" unfolding * using \open t\ assms continuous_openin_preimage_gen openin_trans openin_Union by blast qed lemma continuous_on_components: fixes f :: "'a::topological_space \ 'b::topological_space" assumes "locally connected S " "\C. C \ components S \ continuous_on C f" shows "continuous_on S f" proof (rule continuous_on_components_gen) fix C assume "C \ components S" then show "openin (top_of_set S) C \ continuous_on C f" by (simp add: assms openin_components_locally_connected) qed lemma continuous_on_components_eq: "locally connected S \ (continuous_on S f \ (\c \ components S. continuous_on c f))" by (meson continuous_on_components continuous_on_subset in_components_subset) lemma continuous_on_components_open: fixes S :: "'a::real_normed_vector set" assumes "open S " "\c. c \ components S \ continuous_on c f" shows "continuous_on S f" using continuous_on_components open_imp_locally_connected assms by blast lemma continuous_on_components_open_eq: fixes S :: "'a::real_normed_vector set" shows "open S \ (continuous_on S f \ (\c \ components S. continuous_on c f))" using continuous_on_subset in_components_subset by (blast intro: continuous_on_components_open) lemma closedin_union_complement_components: assumes U: "locally connected U" and S: "closedin (top_of_set U) S" and cuS: "c \ components(U - S)" shows "closedin (top_of_set U) (S \ \c)" proof - have di: "(\S T. S \ c \ T \ c' \ disjnt S T) \ disjnt (\ c) (\ c')" for c' by (simp add: disjnt_def) blast have "S \ U" using S closedin_imp_subset by blast moreover have "U - S = \c \ \(components (U - S) - c)" by (metis Diff_partition Union_components Union_Un_distrib assms(3)) moreover have "disjnt (\c) (\(components (U - S) - c))" apply (rule di) by (metis di DiffD1 DiffD2 assms(3) components_nonoverlap disjnt_def subsetCE) ultimately have eq: "S \ \c = U - (\(components(U - S) - c))" by (auto simp: disjnt_def) have *: "openin (top_of_set U) (\(components (U - S) - c))" proof (rule openin_Union [OF openin_trans [of "U - S"]]) show "openin (top_of_set (U - S)) T" if "T \ components (U - S) - c" for T using that by (simp add: U S locally_diff_closed openin_components_locally_connected) show "openin (top_of_set U) (U - S)" if "T \ components (U - S) - c" for T using that by (simp add: openin_diff S) qed have "closedin (top_of_set U) (U - \ (components (U - S) - c))" by (metis closedin_diff closedin_topspace topspace_euclidean_subtopology *) then have "openin (top_of_set U) (U - (U - \(components (U - S) - c)))" by (simp add: openin_diff) then show ?thesis by (force simp: eq closedin_def) qed lemma closed_union_complement_components: fixes S :: "'a::real_normed_vector set" assumes S: "closed S" and c: "c \ components(- S)" shows "closed(S \ \ c)" proof - have "closedin (top_of_set UNIV) (S \ \c)" by (metis Compl_eq_Diff_UNIV S c closed_closedin closedin_union_complement_components locally_connected_UNIV subtopology_UNIV) then show ?thesis by simp qed lemma closedin_Un_complement_component: fixes S :: "'a::real_normed_vector set" assumes u: "locally connected u" and S: "closedin (top_of_set u) S" and c: " c \ components(u - S)" shows "closedin (top_of_set u) (S \ c)" proof - have "closedin (top_of_set u) (S \ \{c})" using c by (blast intro: closedin_union_complement_components [OF u S]) then show ?thesis by simp qed lemma closed_Un_complement_component: fixes S :: "'a::real_normed_vector set" assumes S: "closed S" and c: " c \ components(-S)" shows "closed (S \ c)" by (metis Compl_eq_Diff_UNIV S c closed_closedin closedin_Un_complement_component locally_connected_UNIV subtopology_UNIV) subsection\Existence of isometry between subspaces of same dimension\ lemma isometry_subset_subspace: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes S: "subspace S" and T: "subspace T" and d: "dim S \ dim T" obtains f where "linear f" "f ` S \ T" "\x. x \ S \ norm(f x) = norm x" proof - obtain B where "B \ S" and Borth: "pairwise orthogonal B" and B1: "\x. x \ B \ norm x = 1" and "independent B" "finite B" "card B = dim S" "span B = S" by (metis orthonormal_basis_subspace [OF S] independent_finite) obtain C where "C \ T" and Corth: "pairwise orthogonal C" and C1:"\x. x \ C \ norm x = 1" and "independent C" "finite C" "card C = dim T" "span C = T" by (metis orthonormal_basis_subspace [OF T] independent_finite) obtain fb where "fb ` B \ C" "inj_on fb B" by (metis \card B = dim S\ \card C = dim T\ \finite B\ \finite C\ card_le_inj d) then have pairwise_orth_fb: "pairwise (\v j. orthogonal (fb v) (fb j)) B" using Corth unfolding pairwise_def inj_on_def by (blast intro: orthogonal_clauses) obtain f where "linear f" and ffb: "\x. x \ B \ f x = fb x" using linear_independent_extend \independent B\ by fastforce have "span (f ` B) \ span C" by (metis \fb ` B \ C\ ffb image_cong span_mono) then have "f ` S \ T" unfolding \span B = S\ \span C = T\ span_linear_image[OF \linear f\] . have [simp]: "\x. x \ B \ norm (fb x) = norm x" using B1 C1 \fb ` B \ C\ by auto have "norm (f x) = norm x" if "x \ S" for x proof - interpret linear f by fact obtain a where x: "x = (\v \ B. a v *\<^sub>R v)" using \finite B\ \span B = S\ \x \ S\ span_finite by fastforce have "norm (f x)^2 = norm (\v\B. a v *\<^sub>R fb v)^2" by (simp add: sum scale ffb x) also have "\ = (\v\B. norm ((a v *\<^sub>R fb v))^2)" proof (rule norm_sum_Pythagorean [OF \finite B\]) show "pairwise (\v j. orthogonal (a v *\<^sub>R fb v) (a j *\<^sub>R fb j)) B" by (rule pairwise_ortho_scaleR [OF pairwise_orth_fb]) qed also have "\ = norm x ^2" by (simp add: x pairwise_ortho_scaleR Borth norm_sum_Pythagorean [OF \finite B\]) finally show ?thesis by (simp add: norm_eq_sqrt_inner) qed then show ?thesis by (rule that [OF \linear f\ \f ` S \ T\]) qed proposition isometries_subspaces: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes S: "subspace S" and T: "subspace T" and d: "dim S = dim T" obtains f g where "linear f" "linear g" "f ` S = T" "g ` T = S" "\x. x \ S \ norm(f x) = norm x" "\x. x \ T \ norm(g x) = norm x" "\x. x \ S \ g(f x) = x" "\x. x \ T \ f(g x) = x" proof - obtain B where "B \ S" and Borth: "pairwise orthogonal B" and B1: "\x. x \ B \ norm x = 1" and "independent B" "finite B" "card B = dim S" "span B = S" by (metis orthonormal_basis_subspace [OF S] independent_finite) obtain C where "C \ T" and Corth: "pairwise orthogonal C" and C1:"\x. x \ C \ norm x = 1" and "independent C" "finite C" "card C = dim T" "span C = T" by (metis orthonormal_basis_subspace [OF T] independent_finite) obtain fb where "bij_betw fb B C" by (metis \finite B\ \finite C\ bij_betw_iff_card \card B = dim S\ \card C = dim T\ d) then have pairwise_orth_fb: "pairwise (\v j. orthogonal (fb v) (fb j)) B" using Corth unfolding pairwise_def inj_on_def bij_betw_def by (blast intro: orthogonal_clauses) obtain f where "linear f" and ffb: "\x. x \ B \ f x = fb x" using linear_independent_extend \independent B\ by fastforce interpret f: linear f by fact define gb where "gb \ inv_into B fb" then have pairwise_orth_gb: "pairwise (\v j. orthogonal (gb v) (gb j)) C" using Borth \bij_betw fb B C\ unfolding pairwise_def bij_betw_def by force obtain g where "linear g" and ggb: "\x. x \ C \ g x = gb x" using linear_independent_extend \independent C\ by fastforce interpret g: linear g by fact have "span (f ` B) \ span C" by (metis \bij_betw fb B C\ bij_betw_imp_surj_on eq_iff ffb image_cong) then have "f ` S \ T" unfolding \span B = S\ \span C = T\ span_linear_image[OF \linear f\] . have [simp]: "\x. x \ B \ norm (fb x) = norm x" using B1 C1 \bij_betw fb B C\ bij_betw_imp_surj_on by fastforce have f [simp]: "norm (f x) = norm x" "g (f x) = x" if "x \ S" for x proof - obtain a where x: "x = (\v \ B. a v *\<^sub>R v)" using \finite B\ \span B = S\ \x \ S\ span_finite by fastforce have "f x = (\v \ B. f (a v *\<^sub>R v))" using linear_sum [OF \linear f\] x by auto also have "\ = (\v \ B. a v *\<^sub>R f v)" by (simp add: f.sum f.scale) also have "\ = (\v \ B. a v *\<^sub>R fb v)" by (simp add: ffb cong: sum.cong) finally have *: "f x = (\v\B. a v *\<^sub>R fb v)" . then have "(norm (f x))\<^sup>2 = (norm (\v\B. a v *\<^sub>R fb v))\<^sup>2" by simp also have "\ = (\v\B. norm ((a v *\<^sub>R fb v))^2)" proof (rule norm_sum_Pythagorean [OF \finite B\]) show "pairwise (\v j. orthogonal (a v *\<^sub>R fb v) (a j *\<^sub>R fb j)) B" by (rule pairwise_ortho_scaleR [OF pairwise_orth_fb]) qed also have "\ = (norm x)\<^sup>2" by (simp add: x pairwise_ortho_scaleR Borth norm_sum_Pythagorean [OF \finite B\]) finally show "norm (f x) = norm x" by (simp add: norm_eq_sqrt_inner) have "g (f x) = g (\v\B. a v *\<^sub>R fb v)" by (simp add: *) also have "\ = (\v\B. g (a v *\<^sub>R fb v))" by (simp add: g.sum g.scale) also have "\ = (\v\B. a v *\<^sub>R g (fb v))" by (simp add: g.scale) also have "\ = (\v\B. a v *\<^sub>R v)" proof (rule sum.cong [OF refl]) show "a x *\<^sub>R g (fb x) = a x *\<^sub>R x" if "x \ B" for x using that \bij_betw fb B C\ bij_betwE bij_betw_inv_into_left gb_def ggb by fastforce qed also have "\ = x" using x by blast finally show "g (f x) = x" . qed have [simp]: "\x. x \ C \ norm (gb x) = norm x" by (metis B1 C1 \bij_betw fb B C\ bij_betw_imp_surj_on gb_def inv_into_into) have g [simp]: "f (g x) = x" if "x \ T" for x proof - obtain a where x: "x = (\v \ C. a v *\<^sub>R v)" using \finite C\ \span C = T\ \x \ T\ span_finite by fastforce have "g x = (\v \ C. g (a v *\<^sub>R v))" by (simp add: x g.sum) also have "\ = (\v \ C. a v *\<^sub>R g v)" by (simp add: g.scale) also have "\ = (\v \ C. a v *\<^sub>R gb v)" by (simp add: ggb cong: sum.cong) finally have "f (g x) = f (\v\C. a v *\<^sub>R gb v)" by simp also have "\ = (\v\C. f (a v *\<^sub>R gb v))" by (simp add: f.scale f.sum) also have "\ = (\v\C. a v *\<^sub>R f (gb v))" by (simp add: f.scale f.sum) also have "\ = (\v\C. a v *\<^sub>R v)" using \bij_betw fb B C\ by (simp add: bij_betw_def gb_def bij_betw_inv_into_right ffb inv_into_into) also have "\ = x" using x by blast finally show "f (g x) = x" . qed have gim: "g ` T = S" by (metis (full_types) S T \f ` S \ T\ d dim_eq_span dim_image_le f(2) g.linear_axioms image_iff linear_subspace_image span_eq_iff subset_iff) have fim: "f ` S = T" using \g ` T = S\ image_iff by fastforce have [simp]: "norm (g x) = norm x" if "x \ T" for x using fim that by auto show ?thesis by (rule that [OF \linear f\ \linear g\]) (simp_all add: fim gim) qed corollary isometry_subspaces: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes S: "subspace S" and T: "subspace T" and d: "dim S = dim T" obtains f where "linear f" "f ` S = T" "\x. x \ S \ norm(f x) = norm x" using isometries_subspaces [OF assms] by metis corollary isomorphisms_UNIV_UNIV: assumes "DIM('M) = DIM('N)" obtains f::"'M::euclidean_space \'N::euclidean_space" and g where "linear f" "linear g" "\x. norm(f x) = norm x" "\y. norm(g y) = norm y" "\x. g (f x) = x" "\y. f(g y) = y" using assms by (auto intro: isometries_subspaces [of "UNIV::'M set" "UNIV::'N set"]) lemma homeomorphic_subspaces: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes S: "subspace S" and T: "subspace T" and d: "dim S = dim T" shows "S homeomorphic T" proof - obtain f g where "linear f" "linear g" "f ` S = T" "g ` T = S" "\x. x \ S \ g(f x) = x" "\x. x \ T \ f(g x) = x" by (blast intro: isometries_subspaces [OF assms]) then show ?thesis unfolding homeomorphic_def homeomorphism_def apply (rule_tac x=f in exI, rule_tac x=g in exI) apply (auto simp: linear_continuous_on linear_conv_bounded_linear) done qed lemma homeomorphic_affine_sets: assumes "affine S" "affine T" "aff_dim S = aff_dim T" shows "S homeomorphic T" proof (cases "S = {} \ T = {}") case True with assms aff_dim_empty homeomorphic_empty show ?thesis by metis next case False then obtain a b where ab: "a \ S" "b \ T" by auto then have ss: "subspace ((+) (- a) ` S)" "subspace ((+) (- b) ` T)" using affine_diffs_subspace assms by blast+ have dd: "dim ((+) (- a) ` S) = dim ((+) (- b) ` T)" using assms ab by (simp add: aff_dim_eq_dim [OF hull_inc] image_def) have "S homeomorphic ((+) (- a) ` S)" by (fact homeomorphic_translation) also have "\ homeomorphic ((+) (- b) ` T)" by (rule homeomorphic_subspaces [OF ss dd]) also have "\ homeomorphic T" using homeomorphic_translation [of T "- b"] by (simp add: homeomorphic_sym [of T]) finally show ?thesis . qed subsection\Retracts, in a general sense, preserve (co)homotopic triviality)\ locale\<^marker>\tag important\ Retracts = - fixes s h t k - assumes conth: "continuous_on s h" - and imh: "h ` s = t" + 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 \ s" + and imk: "k ` t \ S" and idhk: "\y. y \ t \ h(k y) = y" begin lemma homotopically_trivial_retraction_gen: assumes P: "\f. \continuous_on U f; f ` U \ t; Q f\ \ P(k \ f)" - and Q: "\f. \continuous_on U f; f ` U \ s; P f\ \ Q(h \ f)" + and Q: "\f. \continuous_on U f; f ` U \ S; P f\ \ Q(h \ f)" and Qeq: "\h k. (\x. x \ U \ h x = k x) \ Q h = Q k" - and hom: "\f g. \continuous_on U f; f ` U \ s; P f; - continuous_on U g; g ` U \ s; P g\ - \ homotopic_with_canon P U s f g" + and hom: "\f g. \continuous_on U f; f ` U \ S; P f; + continuous_on U g; g ` U \ S; P g\ + \ homotopic_with_canon P U S f g" and contf: "continuous_on U f" and imf: "f ` U \ t" and Qf: "Q f" and contg: "continuous_on U g" and img: "g ` U \ t" and Qg: "Q g" shows "homotopic_with_canon Q U t f g" proof - have "continuous_on U (k \ f)" using contf continuous_on_compose continuous_on_subset contk imf by blast - moreover have "(k \ f) ` U \ s" + moreover have "(k \ f) ` U \ S" using imf imk by fastforce moreover have "P (k \ f)" by (simp add: P Qf contf imf) moreover have "continuous_on U (k \ g)" using contg continuous_on_compose continuous_on_subset contk img by blast - moreover have "(k \ g) ` U \ s" + moreover have "(k \ g) ` U \ S" using img imk by fastforce moreover have "P (k \ g)" by (simp add: P Qg contg img) - ultimately have "homotopic_with_canon P U s (k \ f) (k \ g)" + ultimately have "homotopic_with_canon P U S (k \ f) (k \ g)" by (rule hom) then have "homotopic_with_canon Q U t (h \ (k \ f)) (h \ (k \ g))" apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono]) using Q by (auto simp: conth imh) then show ?thesis proof (rule homotopic_with_eq; simp) show "\h k. (\x. x \ U \ h x = k x) \ Q h = Q k" using Qeq topspace_euclidean_subtopology by blast show "\x. x \ U \ f x = h (k (f x))" "\x. x \ U \ g x = h (k (g x))" using idhk imf img by auto qed qed lemma homotopically_trivial_retraction_null_gen: assumes P: "\f. \continuous_on U f; f ` U \ t; Q f\ \ P(k \ f)" - and Q: "\f. \continuous_on U f; f ` U \ s; P f\ \ Q(h \ f)" + and Q: "\f. \continuous_on U f; f ` U \ S; P f\ \ Q(h \ f)" and Qeq: "\h k. (\x. x \ U \ h x = k x) \ Q h = Q k" - and hom: "\f. \continuous_on U f; f ` U \ s; P f\ - \ \c. homotopic_with_canon P U s f (\x. c)" + and hom: "\f. \continuous_on U f; f ` U \ S; P f\ + \ \c. homotopic_with_canon P U S f (\x. c)" and contf: "continuous_on U f" and imf:"f ` U \ t" and Qf: "Q f" obtains c where "homotopic_with_canon Q U t f (\x. c)" proof - have feq: "\x. x \ U \ (h \ (k \ f)) x = f x" using idhk imf by auto have "continuous_on U (k \ f)" using contf continuous_on_compose continuous_on_subset contk imf by blast - moreover have "(k \ f) ` U \ s" + moreover have "(k \ f) ` U \ S" using imf imk by fastforce moreover have "P (k \ f)" by (simp add: P Qf contf imf) - ultimately obtain c where "homotopic_with_canon P U s (k \ f) (\x. c)" + ultimately obtain c where "homotopic_with_canon P U S (k \ f) (\x. c)" by (metis hom) then have "homotopic_with_canon Q U t (h \ (k \ f)) (h \ (\x. c))" apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono]) using Q by (auto simp: conth imh) then have "homotopic_with_canon Q U t f (\x. h c)" proof (rule homotopic_with_eq) show "\x. x \ topspace (top_of_set U) \ f x = (h \ (k \ f)) x" using feq by auto show "\h k. (\x. x \ topspace (top_of_set U) \ h x = k x) \ Q h = Q k" using Qeq topspace_euclidean_subtopology by blast qed auto then show ?thesis using that by blast qed lemma cohomotopically_trivial_retraction_gen: assumes P: "\f. \continuous_on t f; f ` t \ U; Q f\ \ P(f \ h)" - and Q: "\f. \continuous_on s f; f ` s \ U; P f\ \ Q(f \ k)" + and Q: "\f. \continuous_on S f; f ` S \ U; P f\ \ Q(f \ k)" and Qeq: "\h k. (\x. x \ t \ h x = k x) \ Q h = Q k" - and hom: "\f g. \continuous_on s f; f ` s \ U; P f; - continuous_on s g; g ` s \ U; P g\ - \ homotopic_with_canon P s U f g" + and hom: "\f g. \continuous_on S f; f ` S \ U; P f; + continuous_on S g; g ` S \ U; P g\ + \ homotopic_with_canon P S U f g" and contf: "continuous_on t f" and imf: "f ` t \ U" and Qf: "Q f" and contg: "continuous_on t g" and img: "g ` t \ U" and Qg: "Q g" shows "homotopic_with_canon Q t U f g" proof - have feq: "\x. x \ t \ (f \ h \ k) x = f x" using idhk imf by auto have geq: "\x. x \ t \ (g \ h \ k) x = g x" using idhk img by auto - have "continuous_on s (f \ h)" + have "continuous_on S (f \ h)" using contf conth continuous_on_compose imh by blast - moreover have "(f \ h) ` s \ U" + moreover have "(f \ h) ` S \ U" using imf imh by fastforce moreover have "P (f \ h)" by (simp add: P Qf contf imf) - moreover have "continuous_on s (g \ h)" + moreover have "continuous_on S (g \ h)" using contg continuous_on_compose continuous_on_subset conth imh by blast - moreover have "(g \ h) ` s \ U" + moreover have "(g \ h) ` S \ U" using img imh by fastforce moreover have "P (g \ h)" by (simp add: P Qg contg img) - ultimately have "homotopic_with_canon P s U (f \ h) (g \ h)" + ultimately have "homotopic_with_canon P S U (f \ h) (g \ h)" by (rule hom) then have "homotopic_with_canon Q t U (f \ h \ k) (g \ h \ k)" apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono]) using Q by (auto simp: contk imk) then show ?thesis proof (rule homotopic_with_eq) show "f x = (f \ h \ k) x" "g x = (g \ h \ k) x" if "x \ topspace (top_of_set t)" for x using feq geq that by force+ qed (use Qeq topspace_euclidean_subtopology in blast) qed lemma cohomotopically_trivial_retraction_null_gen: assumes P: "\f. \continuous_on t f; f ` t \ U; Q f\ \ P(f \ h)" - and Q: "\f. \continuous_on s f; f ` s \ U; P f\ \ Q(f \ k)" + and Q: "\f. \continuous_on S f; f ` S \ U; P f\ \ Q(f \ k)" and Qeq: "\h k. (\x. x \ t \ h x = k x) \ Q h = Q k" - and hom: "\f g. \continuous_on s f; f ` s \ U; P f\ - \ \c. homotopic_with_canon P s U f (\x. c)" + and hom: "\f g. \continuous_on S f; f ` S \ U; P f\ + \ \c. homotopic_with_canon P S U f (\x. c)" and contf: "continuous_on t f" and imf: "f ` t \ U" and Qf: "Q f" obtains c where "homotopic_with_canon Q t U f (\x. c)" proof - have feq: "\x. x \ t \ (f \ h \ k) x = f x" using idhk imf by auto - have "continuous_on s (f \ h)" + have "continuous_on S (f \ h)" using contf conth continuous_on_compose imh by blast - moreover have "(f \ h) ` s \ U" + moreover have "(f \ h) ` S \ U" using imf imh by fastforce moreover have "P (f \ h)" by (simp add: P Qf contf imf) - ultimately obtain c where "homotopic_with_canon P s U (f \ h) (\x. c)" + ultimately obtain c where "homotopic_with_canon P S U (f \ h) (\x. c)" by (metis hom) then have \
: "homotopic_with_canon Q t U (f \ h \ k) ((\x. c) \ k)" proof (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono]) - show "\h. \continuous_map (top_of_set s) (top_of_set U) h; P h\ \ Q (h \ k)" + show "\h. \continuous_map (top_of_set S) (top_of_set U) h; P h\ \ Q (h \ k)" using Q by auto qed (auto simp: contk imk) moreover have "homotopic_with_canon Q t U f (\x. c)" using homotopic_with_eq [OF \
] feq Qeq by fastforce ultimately show ?thesis using that by blast qed end lemma simply_connected_retraction_gen: shows "\simply_connected S; continuous_on S h; h ` S = T; continuous_on T k; k ` T \ S; \y. y \ T \ h(k y) = y\ \ 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 _ "\p. pathfinish p = pathstart p" "\p. pathfinish p = pathstart p"]) apply (simp_all add: Retracts_def pathfinish_def pathstart_def) done lemma homeomorphic_simply_connected: "\S homeomorphic T; simply_connected S\ \ simply_connected T" by (auto simp: homeomorphic_def homeomorphism_def intro: simply_connected_retraction_gen) lemma homeomorphic_simply_connected_eq: "S homeomorphic T \ (simply_connected S \ simply_connected T)" by (metis homeomorphic_simply_connected homeomorphic_sym) subsection\Homotopy equivalence\ subsection\Homotopy equivalence of topological spaces.\ definition\<^marker>\tag important\ homotopy_equivalent_space (infix "homotopy'_equivalent'_space" 50) where "X homotopy_equivalent_space Y \ (\f g. continuous_map X Y f \ continuous_map Y X g \ homotopic_with (\x. True) X X (g \ f) id \ homotopic_with (\x. True) Y Y (f \ g) id)" lemma homeomorphic_imp_homotopy_equivalent_space: "X homeomorphic_space Y \ X homotopy_equivalent_space Y" unfolding homeomorphic_space_def homotopy_equivalent_space_def apply (erule ex_forward)+ by (simp add: homotopic_with_equal homotopic_with_sym homeomorphic_maps_def) lemma homotopy_equivalent_space_refl: "X homotopy_equivalent_space X" by (simp add: homeomorphic_imp_homotopy_equivalent_space homeomorphic_space_refl) lemma homotopy_equivalent_space_sym: "X homotopy_equivalent_space Y \ Y homotopy_equivalent_space X" by (meson homotopy_equivalent_space_def) lemma homotopy_eqv_trans [trans]: assumes 1: "X homotopy_equivalent_space Y" and 2: "Y homotopy_equivalent_space U" shows "X homotopy_equivalent_space U" proof - obtain f1 g1 where f1: "continuous_map X Y f1" and g1: "continuous_map Y X g1" and hom1: "homotopic_with (\x. True) X X (g1 \ f1) id" "homotopic_with (\x. True) Y Y (f1 \ g1) id" using 1 by (auto simp: homotopy_equivalent_space_def) obtain f2 g2 where f2: "continuous_map Y U f2" and g2: "continuous_map U Y g2" and hom2: "homotopic_with (\x. True) Y Y (g2 \ f2) id" "homotopic_with (\x. True) U U (f2 \ g2) id" using 2 by (auto simp: homotopy_equivalent_space_def) have "homotopic_with (\f. True) X Y (g2 \ f2 \ f1) (id \ f1)" using f1 hom2(1) homotopic_with_compose_continuous_map_right by metis then have "homotopic_with (\f. True) X Y (g2 \ (f2 \ f1)) (id \ f1)" by (simp add: o_assoc) then have "homotopic_with (\x. True) X X (g1 \ (g2 \ (f2 \ f1))) (g1 \ (id \ f1))" by (simp add: g1 homotopic_with_compose_continuous_map_left) moreover have "homotopic_with (\x. True) X X (g1 \ id \ f1) id" using hom1 by simp ultimately have SS: "homotopic_with (\x. True) X X (g1 \ g2 \ (f2 \ f1)) id" by (metis comp_assoc homotopic_with_trans id_comp) have "homotopic_with (\f. True) U Y (f1 \ g1 \ g2) (id \ g2)" using g2 hom1(2) homotopic_with_compose_continuous_map_right by fastforce then have "homotopic_with (\f. True) U Y (f1 \ (g1 \ g2)) (id \ g2)" by (simp add: o_assoc) then have "homotopic_with (\x. True) U U (f2 \ (f1 \ (g1 \ g2))) (f2 \ (id \ g2))" by (simp add: f2 homotopic_with_compose_continuous_map_left) moreover have "homotopic_with (\x. True) U U (f2 \ id \ g2) id" using hom2 by simp ultimately have UU: "homotopic_with (\x. True) U U (f2 \ f1 \ (g1 \ g2)) id" by (simp add: fun.map_comp hom2(2) homotopic_with_trans) show ?thesis unfolding homotopy_equivalent_space_def by (blast intro: f1 f2 g1 g2 continuous_map_compose SS UU) qed lemma deformation_retraction_imp_homotopy_equivalent_space: - "\homotopic_with (\x. True) X X (s \ r) id; retraction_maps X Y r s\ + "\homotopic_with (\x. True) X X (S \ r) id; retraction_maps X Y r S\ \ X homotopy_equivalent_space Y" unfolding homotopy_equivalent_space_def retraction_maps_def using homotopic_with_id2 by fastforce lemma deformation_retract_imp_homotopy_equivalent_space: "\homotopic_with (\x. True) X X r id; retraction_maps X Y r id\ \ X homotopy_equivalent_space Y" using deformation_retraction_imp_homotopy_equivalent_space by force lemma deformation_retract_of_space: "S \ topspace X \ (\r. homotopic_with (\x. True) X X id r \ retraction_maps X (subtopology X S) r id) \ S retract_of_space X \ (\f. homotopic_with (\x. True) X X id f \ f ` (topspace X) \ S)" proof (cases "S \ topspace X") case True moreover have "(\r. homotopic_with (\x. True) X X id r \ retraction_maps X (subtopology X S) r id) \ (S retract_of_space X \ (\f. homotopic_with (\x. True) X X id f \ f ` topspace X \ S))" unfolding retract_of_space_def proof safe fix f r assume f: "homotopic_with (\x. True) X X id f" and fS: "f ` topspace X \ S" and r: "continuous_map X (subtopology X S) r" and req: "\x\S. r x = x" show "\r. homotopic_with (\x. True) X X id r \ retraction_maps X (subtopology X S) r id" proof (intro exI conjI) have "homotopic_with (\x. True) X X f r" proof (rule homotopic_with_eq) show "homotopic_with (\x. True) X X (r \ f) (r \ id)" by (metis continuous_map_into_fulltopology f homotopic_with_compose_continuous_map_left homotopic_with_symD r) show "f x = (r \ f) x" if "x \ topspace X" for x using that fS req by auto qed auto then show "homotopic_with (\x. True) X X id r" by (rule homotopic_with_trans [OF f]) next show "retraction_maps X (subtopology X S) r id" by (simp add: r req retraction_maps_def) qed qed (use True in \auto simp: retraction_maps_def topspace_subtopology_subset continuous_map_in_subtopology\) ultimately show ?thesis by simp qed (auto simp: retract_of_space_def retraction_maps_def) subsection\Contractible spaces\ text\The definition (which agrees with "contractible" on subsets of Euclidean space) is a little cryptic because we don't in fact assume that the constant "a" is in the space. This forces the convention that the empty space / set is contractible, avoiding some special cases. \ definition contractible_space where "contractible_space X \ \a. homotopic_with (\x. True) X X id (\x. a)" lemma contractible_space_top_of_set [simp]:"contractible_space (top_of_set S) \ contractible S" by (auto simp: contractible_space_def contractible_def) lemma contractible_space_empty: "topspace X = {} \ contractible_space X" unfolding contractible_space_def homotopic_with_def apply (rule_tac x=undefined in exI) apply (rule_tac x="\(t,x). if t = 0 then x else undefined" in exI) apply (auto simp: continuous_map_on_empty) done lemma contractible_space_singleton: "topspace X = {a} \ contractible_space X" unfolding contractible_space_def homotopic_with_def apply (rule_tac x=a in exI) apply (rule_tac x="\(t,x). if t = 0 then x else a" in exI) apply (auto intro: continuous_map_eq [where f = "\z. a"]) done lemma contractible_space_subset_singleton: "topspace X \ {a} \ contractible_space X" by (meson contractible_space_empty contractible_space_singleton subset_singletonD) lemma contractible_space_subtopology_singleton: "contractible_space(subtopology X {a})" by (meson contractible_space_subset_singleton insert_subset path_connectedin_singleton path_connectedin_subtopology subsetI) lemma contractible_space: "contractible_space X \ topspace X = {} \ (\a \ topspace X. homotopic_with (\x. True) X X id (\x. a))" proof (cases "topspace X = {}") case False then show ?thesis using homotopic_with_imp_continuous_maps by (fastforce simp: contractible_space_def) qed (simp add: contractible_space_empty) lemma contractible_imp_path_connected_space: assumes "contractible_space X" shows "path_connected_space X" proof (cases "topspace X = {}") case False have *: "path_connected_space X" if "a \ topspace X" and conth: "continuous_map (prod_topology (top_of_set {0..1}) X) X h" and h: "\x. h (0, x) = x" "\x. h (1, x) = a" for a and h :: "real \ 'a \ 'a" proof - have "path_component_of X b a" if "b \ topspace X" for b unfolding path_component_of_def proof (intro exI conjI) let ?g = "h \ (\x. (x,b))" show "pathin X ?g" unfolding pathin_def proof (rule continuous_map_compose [OF _ conth]) show "continuous_map (top_of_set {0..1}) (prod_topology (top_of_set {0..1}) X) (\x. (x, b))" using that by (auto intro!: continuous_intros) qed qed (use h in auto) then show ?thesis by (metis path_component_of_equiv path_connected_space_iff_path_component) qed show ?thesis using assms False by (auto simp: contractible_space homotopic_with_def *) qed (simp add: path_connected_space_topspace_empty) lemma contractible_imp_connected_space: "contractible_space X \ connected_space X" by (simp add: contractible_imp_path_connected_space path_connected_imp_connected_space) lemma contractible_space_alt: "contractible_space X \ (\a \ topspace X. homotopic_with (\x. True) X X id (\x. a))" (is "?lhs = ?rhs") proof assume X: ?lhs then obtain a where a: "homotopic_with (\x. True) X X id (\x. a)" by (auto simp: contractible_space_def) show ?rhs proof show "homotopic_with (\x. True) X X id (\x. b)" if "b \ topspace X" for b proof (rule homotopic_with_trans [OF a]) show "homotopic_with (\x. True) X X (\x. a) (\x. b)" using homotopic_constant_maps path_connected_space_imp_path_component_of by (metis (full_types) X a continuous_map_const contractible_imp_path_connected_space homotopic_with_imp_continuous_maps that) qed qed next assume R: ?rhs then show ?lhs unfolding contractible_space_def by (metis equals0I homotopic_on_emptyI) qed lemma compose_const [simp]: "f \ (\x. a) = (\x. f a)" "(\x. a) \ g = (\x. a)" by (simp_all add: o_def) lemma nullhomotopic_through_contractible_space: assumes f: "continuous_map X Y f" and g: "continuous_map Y Z g" and Y: "contractible_space Y" obtains c where "homotopic_with (\h. True) X Z (g \ f) (\x. c)" proof - obtain b where b: "homotopic_with (\x. True) Y Y id (\x. b)" using Y by (auto simp: contractible_space_def) show thesis using homotopic_with_compose_continuous_map_right [OF homotopic_with_compose_continuous_map_left [OF b g] f] by (force simp add: that) qed lemma nullhomotopic_into_contractible_space: assumes f: "continuous_map X Y f" and Y: "contractible_space Y" obtains c where "homotopic_with (\h. True) X Y f (\x. c)" using nullhomotopic_through_contractible_space [OF f _ Y] by (metis continuous_map_id id_comp) lemma nullhomotopic_from_contractible_space: assumes f: "continuous_map X Y f" and X: "contractible_space X" obtains c where "homotopic_with (\h. True) X Y f (\x. c)" using nullhomotopic_through_contractible_space [OF _ f X] by (metis comp_id continuous_map_id) lemma homotopy_dominated_contractibility: assumes f: "continuous_map X Y f" and g: "continuous_map Y X g" and hom: "homotopic_with (\x. True) Y Y (f \ g) id" and X: "contractible_space X" shows "contractible_space Y" proof - obtain c where c: "homotopic_with (\h. True) X Y f (\x. c)" using nullhomotopic_from_contractible_space [OF f X] . have "homotopic_with (\x. True) Y Y (f \ g) (\x. c)" using homotopic_with_compose_continuous_map_right [OF c g] by fastforce then have "homotopic_with (\x. True) Y Y id (\x. c)" using homotopic_with_trans [OF _ hom] homotopic_with_symD by blast then show ?thesis unfolding contractible_space_def .. qed lemma homotopy_equivalent_space_contractibility: "X homotopy_equivalent_space Y \ (contractible_space X \ contractible_space Y)" unfolding homotopy_equivalent_space_def by (blast intro: homotopy_dominated_contractibility) lemma homeomorphic_space_contractibility: "X homeomorphic_space Y \ (contractible_space X \ contractible_space Y)" by (simp add: homeomorphic_imp_homotopy_equivalent_space homotopy_equivalent_space_contractibility) lemma contractible_eq_homotopy_equivalent_singleton_subtopology: "contractible_space X \ topspace X = {} \ (\a \ topspace X. X homotopy_equivalent_space (subtopology X {a}))"(is "?lhs = ?rhs") proof (cases "topspace X = {}") case False show ?thesis proof assume ?lhs then obtain a where a: "homotopic_with (\x. True) X X id (\x. a)" by (auto simp: contractible_space_def) then have "a \ topspace X" by (metis False continuous_map_const homotopic_with_imp_continuous_maps) then have "homotopic_with (\x. True) (subtopology X {a}) (subtopology X {a}) id (\x. a)" using connectedin_absolute connectedin_sing contractible_space_alt contractible_space_subtopology_singleton by fastforce then have "X homotopy_equivalent_space subtopology X {a}" unfolding homotopy_equivalent_space_def using \a \ topspace X\ by (metis (full_types) a comp_id continuous_map_const continuous_map_id_subt empty_subsetI homotopic_with_symD id_comp insertI1 insert_subset topspace_subtopology_subset) with \a \ topspace X\ show ?rhs by blast next assume ?rhs then show ?lhs by (meson False contractible_space_subtopology_singleton homotopy_equivalent_space_contractibility) qed qed (simp add: contractible_space_empty) lemma contractible_space_retraction_map_image: assumes "retraction_map X Y f" and X: "contractible_space X" shows "contractible_space Y" proof - obtain g where f: "continuous_map X Y f" and g: "continuous_map Y X g" and fg: "\y \ topspace Y. f(g y) = y" using assms by (auto simp: retraction_map_def retraction_maps_def) obtain a where a: "homotopic_with (\x. True) X X id (\x. a)" using X by (auto simp: contractible_space_def) have "homotopic_with (\x. True) Y Y id (\x. f a)" proof (rule homotopic_with_eq) show "homotopic_with (\x. True) Y Y (f \ id \ g) (f \ (\x. a) \ g)" using f g a homotopic_with_compose_continuous_map_left homotopic_with_compose_continuous_map_right by metis qed (use fg in auto) then show ?thesis unfolding contractible_space_def by blast qed lemma contractible_space_prod_topology: "contractible_space(prod_topology X Y) \ topspace X = {} \ topspace Y = {} \ contractible_space X \ contractible_space Y" proof (cases "topspace X = {} \ topspace Y = {}") case True then have "topspace (prod_topology X Y) = {}" by simp then show ?thesis by (auto simp: contractible_space_empty) next case False have "contractible_space(prod_topology X Y) \ contractible_space X \ contractible_space Y" proof safe assume XY: "contractible_space (prod_topology X Y)" with False have "retraction_map (prod_topology X Y) X fst" by (auto simp: contractible_space False retraction_map_fst) then show "contractible_space X" by (rule contractible_space_retraction_map_image [OF _ XY]) have "retraction_map (prod_topology X Y) Y snd" using False XY by (auto simp: contractible_space False retraction_map_snd) then show "contractible_space Y" by (rule contractible_space_retraction_map_image [OF _ XY]) next assume "contractible_space X" and "contractible_space Y" with False obtain a b where "a \ topspace X" and a: "homotopic_with (\x. True) X X id (\x. a)" and "b \ topspace Y" and b: "homotopic_with (\x. True) Y Y id (\x. b)" by (auto simp: contractible_space) with False show "contractible_space (prod_topology X Y)" apply (simp add: contractible_space) apply (rule_tac x=a in bexI) apply (rule_tac x=b in bexI) using homotopic_with_prod_topology [OF a b] apply (metis (no_types, lifting) case_prod_Pair case_prod_beta' eq_id_iff) apply auto done qed with False show ?thesis by auto qed lemma contractible_space_product_topology: "contractible_space(product_topology X I) \ topspace (product_topology X I) = {} \ (\i \ I. contractible_space(X i))" proof (cases "topspace (product_topology X I) = {}") case False have 1: "contractible_space (X i)" if XI: "contractible_space (product_topology X I)" and "i \ I" for i proof (rule contractible_space_retraction_map_image [OF _ XI]) show "retraction_map (product_topology X I) (X i) (\x. x i)" using False by (simp add: retraction_map_product_projection \i \ I\) qed have 2: "contractible_space (product_topology X I)" if "x \ topspace (product_topology X I)" and cs: "\i\I. contractible_space (X i)" for x :: "'a \ 'b" proof - obtain f where f: "\i. i\I \ homotopic_with (\x. True) (X i) (X i) id (\x. f i)" using cs unfolding contractible_space_def by metis have "homotopic_with (\x. True) (product_topology X I) (product_topology X I) id (\x. restrict f I)" by (rule homotopic_with_eq [OF homotopic_with_product_topology [OF f]]) (auto) then show ?thesis by (auto simp: contractible_space_def) qed show ?thesis using False 1 2 by blast qed (simp add: contractible_space_empty) lemma contractible_space_subtopology_euclideanreal [simp]: "contractible_space(subtopology euclideanreal S) \ is_interval S" (is "?lhs = ?rhs") proof assume ?lhs then have "path_connectedin (subtopology euclideanreal S) S" using contractible_imp_path_connected_space path_connectedin_topspace path_connectedin_absolute by (simp add: contractible_imp_path_connected) then show ?rhs by (simp add: is_interval_path_connected_1) next assume ?rhs then have "convex S" by (simp add: is_interval_convex_1) show ?lhs proof (cases "S = {}") case False then obtain z where "z \ S" by blast show ?thesis unfolding contractible_space_def homotopic_with_def proof (intro exI conjI allI) note \
= convexD [OF \convex S\, simplified] show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set S)) (top_of_set S) (\(t,x). (1 - t) * x + t * z)" using \z \ S\ by (auto simp add: case_prod_unfold intro!: continuous_intros \
) qed auto qed (simp add: contractible_space_empty) qed corollary contractible_space_euclideanreal: "contractible_space euclideanreal" proof - have "contractible_space (subtopology euclideanreal UNIV)" using contractible_space_subtopology_euclideanreal by blast then show ?thesis by simp qed abbreviation\<^marker>\tag important\ homotopy_eqv :: "'a::topological_space set \ 'b::topological_space set \ bool" (infix "homotopy'_eqv" 50) where "S homotopy_eqv T \ top_of_set S homotopy_equivalent_space top_of_set T" lemma homeomorphic_imp_homotopy_eqv: "S homeomorphic T \ S homotopy_eqv T" unfolding homeomorphic_def homeomorphism_def homotopy_equivalent_space_def by (metis continuous_map_subtopology_eu homotopic_with_id2 openin_imp_subset openin_subtopology_self topspace_euclidean_subtopology) lemma homotopy_eqv_inj_linear_image: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "linear f" "inj f" shows "(f ` S) homotopy_eqv S" by (metis assms homeomorphic_sym homeomorphic_imp_homotopy_eqv linear_homeomorphic_image) lemma homotopy_eqv_translation: fixes S :: "'a::real_normed_vector set" shows "(+) a ` S homotopy_eqv S" using homeomorphic_imp_homotopy_eqv homeomorphic_translation homeomorphic_sym by blast lemma homotopy_eqv_homotopic_triviality_imp: fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" and U :: "'c::real_normed_vector set" assumes "S homotopy_eqv T" and f: "continuous_on U f" "f ` U \ T" and g: "continuous_on U g" "g ` U \ T" and homUS: "\f g. \continuous_on U f; f ` U \ S; continuous_on U g; g ` U \ S\ \ homotopic_with_canon (\x. True) U S f g" shows "homotopic_with_canon (\x. True) U T f g" proof - obtain h k where h: "continuous_on S h" "h ` S \ T" and k: "continuous_on T k" "k ` T \ S" and hom: "homotopic_with_canon (\x. True) S S (k \ h) id" "homotopic_with_canon (\x. True) T T (h \ k) id" using assms by (auto simp: homotopy_equivalent_space_def) have "homotopic_with_canon (\f. True) U S (k \ f) (k \ g)" proof (rule homUS) show "continuous_on U (k \ f)" "continuous_on U (k \ g)" using continuous_on_compose continuous_on_subset f g k by blast+ qed (use f g k in \(force simp: o_def)+\ ) then have "homotopic_with_canon (\x. True) U T (h \ (k \ f)) (h \ (k \ g))" by (rule homotopic_with_compose_continuous_left; simp add: h) moreover have "homotopic_with_canon (\x. True) U T (h \ k \ f) (id \ f)" by (rule homotopic_with_compose_continuous_right [where X=T and Y=T]; simp add: hom f) moreover have "homotopic_with_canon (\x. True) U T (h \ k \ g) (id \ g)" by (rule homotopic_with_compose_continuous_right [where X=T and Y=T]; simp add: hom g) ultimately show "homotopic_with_canon (\x. True) U T f g" unfolding o_assoc by (metis homotopic_with_trans homotopic_with_sym id_comp) qed lemma homotopy_eqv_homotopic_triviality: fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" and U :: "'c::real_normed_vector set" assumes "S homotopy_eqv T" shows "(\f g. continuous_on U f \ f ` U \ S \ continuous_on U g \ g ` U \ S \ homotopic_with_canon (\x. True) U S f g) \ (\f g. continuous_on U f \ f ` U \ T \ continuous_on U g \ g ` U \ T \ homotopic_with_canon (\x. True) U T f g)" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (metis assms homotopy_eqv_homotopic_triviality_imp) next assume ?rhs moreover have "T homotopy_eqv S" using assms homotopy_equivalent_space_sym by blast ultimately show ?lhs by (blast intro: homotopy_eqv_homotopic_triviality_imp) qed lemma homotopy_eqv_cohomotopic_triviality_null_imp: fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" and U :: "'c::real_normed_vector set" assumes "S homotopy_eqv T" and f: "continuous_on T f" "f ` T \ U" and homSU: "\f. \continuous_on S f; f ` S \ U\ \ \c. homotopic_with_canon (\x. True) S U f (\x. c)" obtains c where "homotopic_with_canon (\x. True) T U f (\x. c)" proof - obtain h k where h: "continuous_on S h" "h ` S \ T" and k: "continuous_on T k" "k ` T \ S" and hom: "homotopic_with_canon (\x. True) S S (k \ h) id" "homotopic_with_canon (\x. True) T T (h \ k) id" using assms by (auto simp: homotopy_equivalent_space_def) obtain c where "homotopic_with_canon (\x. True) S U (f \ h) (\x. c)" proof (rule exE [OF homSU]) show "continuous_on S (f \ h)" using continuous_on_compose continuous_on_subset f h by blast qed (use f h in force) then have "homotopic_with_canon (\x. True) T U ((f \ h) \ k) ((\x. c) \ k)" by (rule homotopic_with_compose_continuous_right [where X=S]) (use k in auto) moreover have "homotopic_with_canon (\x. True) T U (f \ id) (f \ (h \ k))" by (rule homotopic_with_compose_continuous_left [where Y=T]) (use f in \auto simp add: hom homotopic_with_symD\) ultimately show ?thesis using that homotopic_with_trans by (fastforce simp add: o_def) qed lemma homotopy_eqv_cohomotopic_triviality_null: fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" and U :: "'c::real_normed_vector set" assumes "S homotopy_eqv T" shows "(\f. continuous_on S f \ f ` S \ U \ (\c. homotopic_with_canon (\x. True) S U f (\x. c))) \ (\f. continuous_on T f \ f ` T \ U \ (\c. homotopic_with_canon (\x. True) T U f (\x. c)))" by (rule iffI; metis assms homotopy_eqv_cohomotopic_triviality_null_imp homotopy_equivalent_space_sym) text \Similar to the proof above\ lemma homotopy_eqv_homotopic_triviality_null_imp: fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" and U :: "'c::real_normed_vector set" assumes "S homotopy_eqv T" and f: "continuous_on U f" "f ` U \ T" and homSU: "\f. \continuous_on U f; f ` U \ S\ \ \c. homotopic_with_canon (\x. True) U S f (\x. c)" shows "\c. homotopic_with_canon (\x. True) U T f (\x. c)" proof - obtain h k where h: "continuous_on S h" "h ` S \ T" and k: "continuous_on T k" "k ` T \ S" and hom: "homotopic_with_canon (\x. True) S S (k \ h) id" "homotopic_with_canon (\x. True) T T (h \ k) id" using assms by (auto simp: homotopy_equivalent_space_def) obtain c::'a where "homotopic_with_canon (\x. True) U S (k \ f) (\x. c)" proof (rule exE [OF homSU [of "k \ f"]]) show "continuous_on U (k \ f)" using continuous_on_compose continuous_on_subset f k by blast qed (use f k in force) then have "homotopic_with_canon (\x. True) U T (h \ (k \ f)) (h \ (\x. c))" by (rule homotopic_with_compose_continuous_left [where Y=S]) (use h in auto) moreover have "homotopic_with_canon (\x. True) U T (id \ f) ((h \ k) \ f)" by (rule homotopic_with_compose_continuous_right [where X=T]) (use f in \auto simp add: hom homotopic_with_symD\) ultimately show ?thesis using homotopic_with_trans by (fastforce simp add: o_def) qed lemma homotopy_eqv_homotopic_triviality_null: fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" and U :: "'c::real_normed_vector set" assumes "S homotopy_eqv T" shows "(\f. continuous_on U f \ f ` U \ S \ (\c. homotopic_with_canon (\x. True) U S f (\x. c))) \ (\f. continuous_on U f \ f ` U \ T \ (\c. homotopic_with_canon (\x. True) U T f (\x. c)))" by (rule iffI; metis assms homotopy_eqv_homotopic_triviality_null_imp homotopy_equivalent_space_sym) lemma homotopy_eqv_contractible_sets: fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" assumes "contractible S" "contractible T" "S = {} \ T = {}" shows "S homotopy_eqv T" proof (cases "S = {}") case True with assms show ?thesis by (simp add: homeomorphic_imp_homotopy_eqv) next case False with assms obtain a b where "a \ S" "b \ T" by auto then show ?thesis unfolding homotopy_equivalent_space_def apply (rule_tac x="\x. b" in exI, rule_tac x="\x. a" in exI) apply (intro assms conjI continuous_on_id' homotopic_into_contractible; force) done qed lemma homotopy_eqv_empty1 [simp]: fixes S :: "'a::real_normed_vector set" shows "S homotopy_eqv ({}::'b::real_normed_vector set) \ S = {}" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (metis continuous_map_subtopology_eu empty_iff equalityI homotopy_equivalent_space_def image_subset_iff subsetI) qed (simp add: homotopy_eqv_contractible_sets) lemma homotopy_eqv_empty2 [simp]: fixes S :: "'a::real_normed_vector set" shows "({}::'b::real_normed_vector set) homotopy_eqv S \ S = {}" using homotopy_equivalent_space_sym homotopy_eqv_empty1 by blast lemma homotopy_eqv_contractibility: fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" shows "S homotopy_eqv T \ (contractible S \ contractible T)" by (meson contractible_space_top_of_set homotopy_equivalent_space_contractibility) lemma homotopy_eqv_sing: fixes S :: "'a::real_normed_vector set" and a :: "'b::real_normed_vector" shows "S homotopy_eqv {a} \ S \ {} \ contractible S" proof (cases "S = {}") case False then show ?thesis by (metis contractible_sing empty_not_insert homotopy_eqv_contractibility homotopy_eqv_contractible_sets) qed simp lemma homeomorphic_contractible_eq: fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" shows "S homeomorphic T \ (contractible S \ contractible T)" by (simp add: homeomorphic_imp_homotopy_eqv homotopy_eqv_contractibility) lemma homeomorphic_contractible: fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" shows "\contractible S; S homeomorphic T\ \ contractible T" by (metis homeomorphic_contractible_eq) subsection\<^marker>\tag unimportant\\Misc other results\ lemma bounded_connected_Compl_real: fixes S :: "real set" assumes "bounded S" and conn: "connected(- S)" shows "S = {}" proof - obtain a b where "S \ box a b" by (meson assms bounded_subset_box_symmetric) then have "a \ S" "b \ S" by auto then have "\x. a \ x \ x \ b \ x \ - S" by (meson Compl_iff conn connected_iff_interval) then show ?thesis using \S \ box a b\ by auto qed corollary bounded_path_connected_Compl_real: fixes S :: "real set" assumes "bounded S" "path_connected(- S)" shows "S = {}" by (simp add: assms bounded_connected_Compl_real path_connected_imp_connected) lemma bounded_connected_Compl_1: fixes S :: "'a::{euclidean_space} set" assumes "bounded S" and conn: "connected(- S)" and 1: "DIM('a) = 1" shows "S = {}" proof - have "DIM('a) = DIM(real)" by (simp add: "1") then obtain f::"'a \ real" and g where "linear f" "\x. norm(f x) = norm x" and fg: "\x. g(f x) = x" "\y. f(g y) = y" by (rule isomorphisms_UNIV_UNIV) blast with \bounded S\ have "bounded (f ` S)" using bounded_linear_image linear_linear by blast have "bij f" by (metis fg bijI') have "connected (f ` (-S))" using connected_linear_image assms \linear f\ by blast moreover have "f ` (-S) = - (f ` S)" by (simp add: \bij f\ bij_image_Compl_eq) finally have "connected (- (f ` S))" by simp then have "f ` S = {}" using \bounded (f ` S)\ bounded_connected_Compl_real by blast then show ?thesis by blast qed lemma connected_card_eq_iff_nontrivial: fixes S :: "'a::metric_space set" shows "connected S \ uncountable S \ \(\a. S \ {a})" by (metis connected_uncountable finite.emptyI finite.insertI rev_finite_subset singleton_iff subsetI uncountable_infinite) lemma connected_finite_iff_sing: fixes S :: "'a::metric_space set" assumes "connected S" shows "finite S \ S = {} \ (\a. S = {a})" using assms connected_uncountable countable_finite by blast subsection\<^marker>\tag unimportant\\ Some simple positive connection theorems\ proposition path_connected_convex_diff_countable: fixes U :: "'a::euclidean_space set" assumes "convex U" "\ collinear U" "countable S" shows "path_connected(U - S)" proof (clarsimp simp add: path_connected_def) fix a b assume "a \ U" "a \ S" "b \ U" "b \ S" let ?m = "midpoint a b" show "\g. path g \ path_image g \ U - S \ pathstart g = a \ pathfinish g = b" proof (cases "a = b") case True then show ?thesis by (metis DiffI \a \ U\ \a \ S\ path_component_def path_component_refl) next case False then have "a \ ?m" "b \ ?m" using midpoint_eq_endpoint by fastforce+ have "?m \ U" using \a \ U\ \b \ U\ \convex U\ convex_contains_segment by force obtain c where "c \ U" and nc_abc: "\ collinear {a,b,c}" by (metis False \a \ U\ \b \ U\ \\ collinear U\ collinear_triples insert_absorb) have ncoll_mca: "\ collinear {?m,c,a}" by (metis (full_types) \a \ ?m\ collinear_3_trans collinear_midpoint insert_commute nc_abc) have ncoll_mcb: "\ collinear {?m,c,b}" by (metis (full_types) \b \ ?m\ collinear_3_trans collinear_midpoint insert_commute nc_abc) have "c \ ?m" by (metis collinear_midpoint insert_commute nc_abc) then have "closed_segment ?m c \ U" by (simp add: \c \ U\ \?m \ U\ \convex U\ closed_segment_subset) then obtain z where z: "z \ closed_segment ?m c" and disjS: "(closed_segment a z \ closed_segment z b) \ S = {}" proof - have False if "closed_segment ?m c \ {z. (closed_segment a z \ closed_segment z b) \ S \ {}}" proof - have closb: "closed_segment ?m c \ {z \ closed_segment ?m c. closed_segment a z \ S \ {}} \ {z \ closed_segment ?m c. closed_segment z b \ S \ {}}" using that by blast have *: "countable {z \ closed_segment ?m c. closed_segment z u \ S \ {}}" if "u \ U" "u \ S" and ncoll: "\ collinear {?m, c, u}" for u proof - have **: False if x1: "x1 \ closed_segment ?m c" and x2: "x2 \ closed_segment ?m c" and "x1 \ x2" "x1 \ u" and w: "w \ closed_segment x1 u" "w \ closed_segment x2 u" and "w \ S" for x1 x2 w proof - have "x1 \ affine hull {?m,c}" "x2 \ affine hull {?m,c}" using segment_as_ball x1 x2 by auto then have coll_x1: "collinear {x1, ?m, c}" and coll_x2: "collinear {?m, c, x2}" by (simp_all add: affine_hull_3_imp_collinear) (metis affine_hull_3_imp_collinear insert_commute) have "\ collinear {x1, u, x2}" proof assume "collinear {x1, u, x2}" then have "collinear {?m, c, u}" by (metis (full_types) \c \ ?m\ coll_x1 coll_x2 collinear_3_trans insert_commute ncoll \x1 \ x2\) with ncoll show False .. qed then have "closed_segment x1 u \ closed_segment u x2 = {u}" by (blast intro!: Int_closed_segment) then have "w = u" using closed_segment_commute w by auto show ?thesis using \u \ S\ \w = u\ that(7) by auto qed then have disj: "disjoint ((\z\closed_segment ?m c. {closed_segment z u \ S}))" by (fastforce simp: pairwise_def disjnt_def) have cou: "countable ((\z \ closed_segment ?m c. {closed_segment z u \ S}) - {{}})" apply (rule pairwise_disjnt_countable_Union [OF _ pairwise_subset [OF disj]]) apply (rule countable_subset [OF _ \countable S\], auto) done define f where "f \ \X. (THE z. z \ closed_segment ?m c \ X = closed_segment z u \ S)" show ?thesis proof (rule countable_subset [OF _ countable_image [OF cou, where f=f]], clarify) fix x assume x: "x \ closed_segment ?m c" "closed_segment x u \ S \ {}" show "x \ f ` ((\z\closed_segment ?m c. {closed_segment z u \ S}) - {{}})" proof (rule_tac x="closed_segment x u \ S" in image_eqI) show "x = f (closed_segment x u \ S)" unfolding f_def by (rule the_equality [symmetric]) (use x in \auto dest: **\) qed (use x in auto) qed qed have "uncountable (closed_segment ?m c)" by (metis \c \ ?m\ uncountable_closed_segment) then show False using closb * [OF \a \ U\ \a \ S\ ncoll_mca] * [OF \b \ U\ \b \ S\ ncoll_mcb] by (simp add: closed_segment_commute countable_subset) qed then show ?thesis by (force intro: that) qed show ?thesis proof (intro exI conjI) have "path_image (linepath a z +++ linepath z b) \ U" by (metis \a \ U\ \b \ U\ \closed_segment ?m c \ U\ z \convex U\ closed_segment_subset contra_subsetD path_image_linepath subset_path_image_join) with disjS show "path_image (linepath a z +++ linepath z b) \ U - S" by (force simp: path_image_join) qed auto qed qed corollary connected_convex_diff_countable: fixes U :: "'a::euclidean_space set" assumes "convex U" "\ collinear U" "countable S" shows "connected(U - S)" by (simp add: assms path_connected_convex_diff_countable path_connected_imp_connected) lemma path_connected_punctured_convex: assumes "convex S" and aff: "aff_dim S \ 1" shows "path_connected(S - {a})" proof - consider "aff_dim S = -1" | "aff_dim S = 0" | "aff_dim S \ 2" using assms aff_dim_geq [of S] by linarith then show ?thesis proof cases assume "aff_dim S = -1" then show ?thesis by (metis aff_dim_empty empty_Diff path_connected_empty) next assume "aff_dim S = 0" then show ?thesis by (metis aff_dim_eq_0 Diff_cancel Diff_empty Diff_insert0 convex_empty convex_imp_path_connected path_connected_singleton singletonD) next assume ge2: "aff_dim S \ 2" then have "\ collinear S" proof (clarsimp simp add: collinear_affine_hull) fix u v assume "S \ affine hull {u, v}" then have "aff_dim S \ aff_dim {u, v}" by (metis (no_types) aff_dim_affine_hull aff_dim_subset) with ge2 show False by (metis (no_types) aff_dim_2 antisym aff not_numeral_le_zero one_le_numeral order_trans) qed moreover have "countable {a}" by simp ultimately show ?thesis by (metis path_connected_convex_diff_countable [OF \convex S\]) qed qed lemma connected_punctured_convex: shows "\convex S; aff_dim S \ 1\ \ connected(S - {a})" using path_connected_imp_connected path_connected_punctured_convex by blast lemma path_connected_complement_countable: fixes S :: "'a::euclidean_space set" assumes "2 \ DIM('a)" "countable S" shows "path_connected(- S)" proof - have "\ collinear (UNIV::'a set)" using assms by (auto simp: collinear_aff_dim [of "UNIV :: 'a set"]) then have "path_connected(UNIV - S)" by (simp add: \countable S\ path_connected_convex_diff_countable) then show ?thesis by (simp add: Compl_eq_Diff_UNIV) qed proposition path_connected_openin_diff_countable: fixes S :: "'a::euclidean_space set" assumes "connected S" and ope: "openin (top_of_set (affine hull S)) S" and "\ collinear S" "countable T" shows "path_connected(S - T)" proof (clarsimp simp add: path_connected_component) fix x y assume xy: "x \ S" "x \ T" "y \ S" "y \ T" show "path_component (S - T) x y" proof (rule connected_equivalence_relation_gen [OF \connected S\, where P = "\x. x \ T"]) show "\z. z \ U \ z \ T" if opeU: "openin (top_of_set S) U" and "x \ U" for U x proof - have "openin (top_of_set (affine hull S)) U" using opeU ope openin_trans by blast with \x \ U\ obtain r where Usub: "U \ affine hull S" and "r > 0" and subU: "ball x r \ affine hull S \ U" by (auto simp: openin_contains_ball) with \x \ U\ have x: "x \ ball x r \ affine hull S" by auto have "\ S \ {x}" using \\ collinear S\ collinear_subset by blast then obtain x' where "x' \ x" "x' \ S" by blast obtain y where y: "y \ x" "y \ ball x r \ affine hull S" proof show "x + (r / 2 / norm(x' - x)) *\<^sub>R (x' - x) \ x" using \x' \ x\ \r > 0\ by auto show "x + (r / 2 / norm (x' - x)) *\<^sub>R (x' - x) \ ball x r \ affine hull S" using \x' \ x\ \r > 0\ \x' \ S\ x by (simp add: dist_norm mem_affine_3_minus hull_inc) qed have "convex (ball x r \ affine hull S)" by (simp add: affine_imp_convex convex_Int) with x y subU have "uncountable U" by (meson countable_subset uncountable_convex) then have "\ U \ T" using \countable T\ countable_subset by blast then show ?thesis by blast qed show "\U. openin (top_of_set S) U \ x \ U \ (\x\U. \y\U. x \ T \ y \ T \ path_component (S - T) x y)" if "x \ S" for x proof - obtain r where Ssub: "S \ affine hull S" and "r > 0" and subS: "ball x r \ affine hull S \ S" using ope \x \ S\ by (auto simp: openin_contains_ball) then have conv: "convex (ball x r \ affine hull S)" by (simp add: affine_imp_convex convex_Int) have "\ aff_dim (affine hull S) \ 1" using \\ collinear S\ collinear_aff_dim by auto then have "\ aff_dim (ball x r \ affine hull S) \ 1" by (metis (no_types, opaque_lifting) aff_dim_convex_Int_open IntI open_ball \0 < r\ aff_dim_affine_hull affine_affine_hull affine_imp_convex centre_in_ball empty_iff hull_subset inf_commute subsetCE that) then have "\ collinear (ball x r \ affine hull S)" by (simp add: collinear_aff_dim) then have *: "path_connected ((ball x r \ affine hull S) - T)" by (rule path_connected_convex_diff_countable [OF conv _ \countable T\]) have ST: "ball x r \ affine hull S - T \ S - T" using subS by auto show ?thesis proof (intro exI conjI) show "x \ ball x r \ affine hull S" using \x \ S\ \r > 0\ by (simp add: hull_inc) have "openin (top_of_set (affine hull S)) (ball x r \ affine hull S)" by (subst inf.commute) (simp add: openin_Int_open) then show "openin (top_of_set S) (ball x r \ affine hull S)" by (rule openin_subset_trans [OF _ subS Ssub]) qed (use * path_component_trans in \auto simp: path_connected_component path_component_of_subset [OF ST]\) qed qed (use xy path_component_trans in auto) qed corollary connected_openin_diff_countable: fixes S :: "'a::euclidean_space set" assumes "connected S" and ope: "openin (top_of_set (affine hull S)) S" and "\ collinear S" "countable T" shows "connected(S - T)" by (metis path_connected_imp_connected path_connected_openin_diff_countable [OF assms]) corollary path_connected_open_diff_countable: fixes S :: "'a::euclidean_space set" assumes "2 \ DIM('a)" "open S" "connected S" "countable T" shows "path_connected(S - T)" proof (cases "S = {}") case True then show ?thesis by (simp) next case False show ?thesis proof (rule path_connected_openin_diff_countable) show "openin (top_of_set (affine hull S)) S" by (simp add: assms hull_subset open_subset) show "\ collinear S" using assms False by (simp add: collinear_aff_dim aff_dim_open) qed (simp_all add: assms) qed corollary connected_open_diff_countable: fixes S :: "'a::euclidean_space set" assumes "2 \ DIM('a)" "open S" "connected S" "countable T" shows "connected(S - T)" by (simp add: assms path_connected_imp_connected path_connected_open_diff_countable) subsection\<^marker>\tag unimportant\ \Self-homeomorphisms shuffling points about\ subsubsection\<^marker>\tag unimportant\\The theorem \homeomorphism_moving_points_exists\\ lemma homeomorphism_moving_point_1: fixes a :: "'a::euclidean_space" assumes "affine T" "a \ T" and u: "u \ ball a r \ T" obtains f g where "homeomorphism (cball a r \ T) (cball a r \ T) f g" "f a = u" "\x. x \ sphere a r \ f x = x" proof - have nou: "norm (u - a) < r" and "u \ T" using u by (auto simp: dist_norm norm_minus_commute) then have "0 < r" by (metis DiffD1 Diff_Diff_Int ball_eq_empty centre_in_ball not_le u) define f where "f \ \x. (1 - norm(x - a) / r) *\<^sub>R (u - a) + x" have *: "False" if eq: "x + (norm y / r) *\<^sub>R u = y + (norm x / r) *\<^sub>R u" and nou: "norm u < r" and yx: "norm y < norm x" for x y and u::'a proof - have "x = y + (norm x / r - (norm y / r)) *\<^sub>R u" using eq by (simp add: algebra_simps) then have "norm x = norm (y + ((norm x - norm y) / r) *\<^sub>R u)" by (metis diff_divide_distrib) also have "\ \ norm y + norm(((norm x - norm y) / r) *\<^sub>R u)" using norm_triangle_ineq by blast also have "\ = norm y + (norm x - norm y) * (norm u / r)" using yx \r > 0\ by (simp add: field_split_simps) also have "\ < norm y + (norm x - norm y) * 1" proof (subst add_less_cancel_left) show "(norm x - norm y) * (norm u / r) < (norm x - norm y) * 1" proof (rule mult_strict_left_mono) show "norm u / r < 1" using \0 < r\ divide_less_eq_1_pos nou by blast qed (simp add: yx) qed also have "\ = norm x" by simp finally show False by simp qed have "inj f" unfolding f_def proof (clarsimp simp: inj_on_def) fix x y assume "(1 - norm (x - a) / r) *\<^sub>R (u - a) + x = (1 - norm (y - a) / r) *\<^sub>R (u - a) + y" then have eq: "(x - a) + (norm (y - a) / r) *\<^sub>R (u - a) = (y - a) + (norm (x - a) / r) *\<^sub>R (u - a)" by (auto simp: algebra_simps) show "x=y" proof (cases "norm (x - a) = norm (y - a)") case True then show ?thesis using eq by auto next case False then consider "norm (x - a) < norm (y - a)" | "norm (x - a) > norm (y - a)" by linarith then have "False" proof cases case 1 show False using * [OF _ nou 1] eq by simp next case 2 with * [OF eq nou] show False by auto qed then show "x=y" .. qed qed then have inj_onf: "inj_on f (cball a r \ T)" using inj_on_Int by fastforce have contf: "continuous_on (cball a r \ T) f" unfolding f_def using \0 < r\ by (intro continuous_intros) blast have fim: "f ` (cball a r \ T) = cball a r \ T" proof have *: "norm (y + (1 - norm y / r) *\<^sub>R u) \ r" if "norm y \ r" "norm u < r" for y u::'a proof - have "norm (y + (1 - norm y / r) *\<^sub>R u) \ norm y + norm((1 - norm y / r) *\<^sub>R u)" using norm_triangle_ineq by blast also have "\ = norm y + abs(1 - norm y / r) * norm u" by simp also have "\ \ r" proof - have "(r - norm u) * (r - norm y) \ 0" using that by auto then have "r * norm u + r * norm y \ r * r + norm u * norm y" by (simp add: algebra_simps) then show ?thesis using that \0 < r\ by (simp add: abs_if field_simps) qed finally show ?thesis . qed have "f ` (cball a r) \ cball a r" using * nou apply (clarsimp simp: dist_norm norm_minus_commute f_def) by (metis diff_add_eq diff_diff_add diff_diff_eq2 norm_minus_commute) moreover have "f ` T \ T" unfolding f_def using \affine T\ \a \ T\ \u \ T\ by (force simp: add.commute mem_affine_3_minus) ultimately show "f ` (cball a r \ T) \ cball a r \ T" by blast next show "cball a r \ T \ f ` (cball a r \ T)" proof (clarsimp simp add: dist_norm norm_minus_commute) fix x assume x: "norm (x - a) \ r" and "x \ T" have "\v \ {0..1}. ((1 - v) * r - norm ((x - a) - v *\<^sub>R (u - a))) \ 1 = 0" by (rule ivt_decreasing_component_on_1) (auto simp: x continuous_intros) then obtain v where "0 \ v" "v \ 1" and v: "(1 - v) * r = norm ((x - a) - v *\<^sub>R (u - a))" by auto then have n: "norm (a - (x - v *\<^sub>R (u - a))) = r - r * v" by (simp add: field_simps norm_minus_commute) show "x \ f ` (cball a r \ T)" proof (rule image_eqI) show "x = f (x - v *\<^sub>R (u - a))" using \r > 0\ v by (simp add: f_def) (simp add: field_simps) have "x - v *\<^sub>R (u - a) \ cball a r" using \r > 0\\0 \ v\ by (simp add: dist_norm n) moreover have "x - v *\<^sub>R (u - a) \ T" by (simp add: f_def \u \ T\ \x \ T\ assms mem_affine_3_minus2) ultimately show "x - v *\<^sub>R (u - a) \ cball a r \ T" by blast qed qed qed have "compact (cball a r \ T)" by (simp add: affine_closed compact_Int_closed \affine T\) then obtain g where "homeomorphism (cball a r \ T) (cball a r \ T) f g" by (metis homeomorphism_compact [OF _ contf fim inj_onf]) then show thesis apply (rule_tac f=f in that) using \r > 0\ by (simp_all add: f_def dist_norm norm_minus_commute) qed corollary\<^marker>\tag unimportant\ homeomorphism_moving_point_2: fixes a :: "'a::euclidean_space" assumes "affine T" "a \ T" and u: "u \ ball a r \ T" and v: "v \ ball a r \ T" obtains f g where "homeomorphism (cball a r \ T) (cball a r \ T) f g" "f u = v" "\x. \x \ sphere a r; x \ T\ \ f x = x" proof - have "0 < r" by (metis DiffD1 Diff_Diff_Int ball_eq_empty centre_in_ball not_le u) obtain f1 g1 where hom1: "homeomorphism (cball a r \ T) (cball a r \ T) f1 g1" and "f1 a = u" and f1: "\x. x \ sphere a r \ f1 x = x" using homeomorphism_moving_point_1 [OF \affine T\ \a \ T\ u] by blast obtain f2 g2 where hom2: "homeomorphism (cball a r \ T) (cball a r \ T) f2 g2" and "f2 a = v" and f2: "\x. x \ sphere a r \ f2 x = x" using homeomorphism_moving_point_1 [OF \affine T\ \a \ T\ v] by blast show ?thesis proof show "homeomorphism (cball a r \ T) (cball a r \ T) (f2 \ g1) (f1 \ g2)" by (metis homeomorphism_compose homeomorphism_symD hom1 hom2) have "g1 u = a" using \0 < r\ \f1 a = u\ assms hom1 homeomorphism_apply1 by fastforce then show "(f2 \ g1) u = v" by (simp add: \f2 a = v\) show "\x. \x \ sphere a r; x \ T\ \ (f2 \ g1) x = x" using f1 f2 hom1 homeomorphism_apply1 by fastforce qed qed corollary\<^marker>\tag unimportant\ homeomorphism_moving_point_3: fixes a :: "'a::euclidean_space" assumes "affine T" "a \ T" and ST: "ball a r \ T \ S" "S \ T" and u: "u \ ball a r \ T" and v: "v \ ball a r \ T" obtains f g where "homeomorphism S S f g" "f u = v" "{x. \ (f x = x \ g x = x)} \ ball a r \ T" proof - obtain f g where hom: "homeomorphism (cball a r \ T) (cball a r \ T) f g" and "f u = v" and fid: "\x. \x \ sphere a r; x \ T\ \ f x = x" using homeomorphism_moving_point_2 [OF \affine T\ \a \ T\ u v] by blast have gid: "\x. \x \ sphere a r; x \ T\ \ g x = x" using fid hom homeomorphism_apply1 by fastforce define ff where "ff \ \x. if x \ ball a r \ T then f x else x" define gg where "gg \ \x. if x \ ball a r \ T then g x else x" show ?thesis proof show "homeomorphism S S ff gg" proof (rule homeomorphismI) have "continuous_on ((cball a r \ T) \ (T - ball a r)) ff" unfolding ff_def using homeomorphism_cont1 [OF hom] by (intro continuous_on_cases) (auto simp: affine_closed \affine T\ fid) then show "continuous_on S ff" by (rule continuous_on_subset) (use ST in auto) have "continuous_on ((cball a r \ T) \ (T - ball a r)) gg" unfolding gg_def using homeomorphism_cont2 [OF hom] by (intro continuous_on_cases) (auto simp: affine_closed \affine T\ gid) then show "continuous_on S gg" by (rule continuous_on_subset) (use ST in auto) show "ff ` S \ S" proof (clarsimp simp add: ff_def) fix x assume "x \ S" and x: "dist a x < r" and "x \ T" then have "f x \ cball a r \ T" using homeomorphism_image1 [OF hom] by force then show "f x \ S" using ST(1) \x \ T\ gid hom homeomorphism_def x by fastforce qed show "gg ` S \ S" proof (clarsimp simp add: gg_def) fix x assume "x \ S" and x: "dist a x < r" and "x \ T" then have "g x \ cball a r \ T" using homeomorphism_image2 [OF hom] by force then have "g x \ ball a r" using homeomorphism_apply2 [OF hom] by (metis Diff_Diff_Int Diff_iff \x \ T\ cball_def fid le_less mem_Collect_eq mem_ball mem_sphere x) then show "g x \ S" using ST(1) \g x \ cball a r \ T\ by force qed show "\x. x \ S \ gg (ff x) = x" unfolding ff_def gg_def using homeomorphism_apply1 [OF hom] homeomorphism_image1 [OF hom] by simp (metis Int_iff homeomorphism_apply1 [OF hom] fid image_eqI less_eq_real_def mem_cball mem_sphere) show "\x. x \ S \ ff (gg x) = x" unfolding ff_def gg_def using homeomorphism_apply2 [OF hom] homeomorphism_image2 [OF hom] by simp (metis Int_iff fid image_eqI less_eq_real_def mem_cball mem_sphere) qed show "ff u = v" using u by (auto simp: ff_def \f u = v\) show "{x. \ (ff x = x \ gg x = x)} \ ball a r \ T" by (auto simp: ff_def gg_def) qed qed proposition\<^marker>\tag unimportant\ homeomorphism_moving_point: fixes a :: "'a::euclidean_space" assumes ope: "openin (top_of_set (affine hull S)) S" and "S \ T" and TS: "T \ affine hull S" and S: "connected S" "a \ S" "b \ S" obtains f g where "homeomorphism T T f g" "f a = b" "{x. \ (f x = x \ g x = x)} \ S" "bounded {x. \ (f x = x \ g x = x)}" proof - have 1: "\h k. homeomorphism T T h k \ h (f d) = d \ {x. \ (h x = x \ k x = x)} \ S \ bounded {x. \ (h x = x \ k x = x)}" if "d \ S" "f d \ S" and homfg: "homeomorphism T T f g" and S: "{x. \ (f x = x \ g x = x)} \ S" and bo: "bounded {x. \ (f x = x \ g x = x)}" for d f g proof (intro exI conjI) show homgf: "homeomorphism T T g f" by (metis homeomorphism_symD homfg) then show "g (f d) = d" by (meson \S \ T\ homeomorphism_def subsetD \d \ S\) show "{x. \ (g x = x \ f x = x)} \ S" using S by blast show "bounded {x. \ (g x = x \ f x = x)}" using bo by (simp add: conj_commute) qed have 2: "\f g. homeomorphism T T f g \ f x = f2 (f1 x) \ {x. \ (f x = x \ g x = x)} \ S \ bounded {x. \ (f x = x \ g x = x)}" if "x \ S" "f1 x \ S" "f2 (f1 x) \ S" and hom: "homeomorphism T T f1 g1" "homeomorphism T T f2 g2" and sub: "{x. \ (f1 x = x \ g1 x = x)} \ S" "{x. \ (f2 x = x \ g2 x = x)} \ S" and bo: "bounded {x. \ (f1 x = x \ g1 x = x)}" "bounded {x. \ (f2 x = x \ g2 x = x)}" for x f1 f2 g1 g2 proof (intro exI conjI) show homgf: "homeomorphism T T (f2 \ f1) (g1 \ g2)" by (metis homeomorphism_compose hom) then show "(f2 \ f1) x = f2 (f1 x)" by force show "{x. \ ((f2 \ f1) x = x \ (g1 \ g2) x = x)} \ S" using sub by force have "bounded ({x. \(f1 x = x \ g1 x = x)} \ {x. \(f2 x = x \ g2 x = x)})" using bo by simp then show "bounded {x. \ ((f2 \ f1) x = x \ (g1 \ g2) x = x)}" by (rule bounded_subset) auto qed have 3: "\U. openin (top_of_set S) U \ d \ U \ (\x\U. \f g. homeomorphism T T f g \ f d = x \ {x. \ (f x = x \ g x = x)} \ S \ bounded {x. \ (f x = x \ g x = x)})" if "d \ S" for d proof - obtain r where "r > 0" and r: "ball d r \ affine hull S \ S" by (metis \d \ S\ ope openin_contains_ball) have *: "\f g. homeomorphism T T f g \ f d = e \ {x. \ (f x = x \ g x = x)} \ S \ bounded {x. \ (f x = x \ g x = x)}" if "e \ S" "e \ ball d r" for e apply (rule homeomorphism_moving_point_3 [of "affine hull S" d r T d e]) using r \S \ T\ TS that apply (auto simp: \d \ S\ \0 < r\ hull_inc) using bounded_subset by blast show ?thesis by (rule_tac x="S \ ball d r" in exI) (fastforce simp: openin_open_Int \0 < r\ that intro: *) qed have "\f g. homeomorphism T T f g \ f a = b \ {x. \ (f x = x \ g x = x)} \ S \ bounded {x. \ (f x = x \ g x = x)}" by (rule connected_equivalence_relation [OF S]; blast intro: 1 2 3) then show ?thesis using that by auto qed lemma homeomorphism_moving_points_exists_gen: assumes K: "finite K" "\i. i \ K \ x i \ S \ y i \ S" "pairwise (\i j. (x i \ x j) \ (y i \ y j)) K" and "2 \ aff_dim S" and ope: "openin (top_of_set (affine hull S)) S" and "S \ T" "T \ affine hull S" "connected S" shows "\f g. homeomorphism T T f g \ (\i \ K. f(x i) = y i) \ {x. \ (f x = x \ g x = x)} \ S \ bounded {x. \ (f x = x \ g x = x)}" using assms proof (induction K) case empty then show ?case by (force simp: homeomorphism_ident) next case (insert i K) then have xney: "\j. \j \ K; j \ i\ \ x i \ x j \ y i \ y j" and pw: "pairwise (\i j. x i \ x j \ y i \ y j) K" and "x i \ S" "y i \ S" and xyS: "\i. i \ K \ x i \ S \ y i \ S" by (simp_all add: pairwise_insert) obtain f g where homfg: "homeomorphism T T f g" and feq: "\i. i \ K \ f(x i) = y i" and fg_sub: "{x. \ (f x = x \ g x = x)} \ S" and bo_fg: "bounded {x. \ (f x = x \ g x = x)}" using insert.IH [OF xyS pw] insert.prems by (blast intro: that) then have "\f g. homeomorphism T T f g \ (\i \ K. f(x i) = y i) \ {x. \ (f x = x \ g x = x)} \ S \ bounded {x. \ (f x = x \ g x = x)}" using insert by blast have aff_eq: "affine hull (S - y ` K) = affine hull S" proof (rule affine_hull_Diff [OF ope]) show "finite (y ` K)" by (simp add: insert.hyps(1)) show "y ` K \ S" using \y i \ S\ insert.hyps(2) xney xyS by fastforce qed have f_in_S: "f x \ S" if "x \ S" for x using homfg fg_sub homeomorphism_apply1 \S \ T\ proof - have "(f (f x) \ f x \ g (f x) \ f x) \ f x \ S" by (metis \S \ T\ homfg subsetD homeomorphism_apply1 that) then show ?thesis using fg_sub by force qed obtain h k where homhk: "homeomorphism T T h k" and heq: "h (f (x i)) = y i" and hk_sub: "{x. \ (h x = x \ k x = x)} \ S - y ` K" and bo_hk: "bounded {x. \ (h x = x \ k x = x)}" proof (rule homeomorphism_moving_point [of "S - y`K" T "f(x i)" "y i"]) show "openin (top_of_set (affine hull (S - y ` K))) (S - y ` K)" by (simp add: aff_eq openin_diff finite_imp_closedin image_subset_iff hull_inc insert xyS) show "S - y ` K \ T" using \S \ T\ by auto show "T \ affine hull (S - y ` K)" using insert by (simp add: aff_eq) show "connected (S - y ` K)" proof (rule connected_openin_diff_countable [OF \connected S\ ope]) show "\ collinear S" using collinear_aff_dim \2 \ aff_dim S\ by force show "countable (y ` K)" using countable_finite insert.hyps(1) by blast qed have "\k. \f (x i) = y k; k \ K\ \ False" by (metis feq homfg \x i \ S\ homeomorphism_def \S \ T\ \i \ K\ subsetCE xney xyS) then show "f (x i) \ S - y ` K" by (auto simp: f_in_S \x i \ S\) show "y i \ S - y ` K" using insert.hyps xney by (auto simp: \y i \ S\) qed blast show ?case proof (intro exI conjI) show "homeomorphism T T (h \ f) (g \ k)" using homfg homhk homeomorphism_compose by blast show "\i \ insert i K. (h \ f) (x i) = y i" using feq hk_sub by (auto simp: heq) show "{x. \ ((h \ f) x = x \ (g \ k) x = x)} \ S" using fg_sub hk_sub by force have "bounded ({x. \(f x = x \ g x = x)} \ {x. \(h x = x \ k x = x)})" using bo_fg bo_hk bounded_Un by blast then show "bounded {x. \ ((h \ f) x = x \ (g \ k) x = x)}" by (rule bounded_subset) auto qed qed proposition\<^marker>\tag unimportant\ homeomorphism_moving_points_exists: fixes S :: "'a::euclidean_space set" assumes 2: "2 \ DIM('a)" "open S" "connected S" "S \ T" "finite K" and KS: "\i. i \ K \ x i \ S \ y i \ S" and pw: "pairwise (\i j. (x i \ x j) \ (y i \ y j)) K" and S: "S \ T" "T \ affine hull S" "connected S" obtains f g where "homeomorphism T T f g" "\i. i \ K \ f(x i) = y i" "{x. \ (f x = x \ g x = x)} \ S" "bounded {x. (\ (f x = x \ g x = x))}" proof (cases "S = {}") case True then show ?thesis using KS homeomorphism_ident that by fastforce next case False then have affS: "affine hull S = UNIV" by (simp add: affine_hull_open \open S\) then have ope: "openin (top_of_set (affine hull S)) S" using \open S\ open_openin by auto have "2 \ DIM('a)" by (rule 2) also have "\ = aff_dim (UNIV :: 'a set)" by simp also have "\ \ aff_dim S" by (metis aff_dim_UNIV aff_dim_affine_hull aff_dim_le_DIM affS) finally have "2 \ aff_dim S" by linarith then show ?thesis using homeomorphism_moving_points_exists_gen [OF \finite K\ KS pw _ ope S] that by fastforce qed subsubsection\<^marker>\tag unimportant\\The theorem \homeomorphism_grouping_points_exists\\ lemma homeomorphism_grouping_point_1: fixes a::real and c::real assumes "a < b" "c < d" obtains f g where "homeomorphism (cbox a b) (cbox c d) f g" "f a = c" "f b = d" proof - define f where "f \ \x. ((d - c) / (b - a)) * x + (c - a * ((d - c) / (b - a)))" have "\g. homeomorphism (cbox a b) (cbox c d) f g" proof (rule homeomorphism_compact) show "continuous_on (cbox a b) f" unfolding f_def by (intro continuous_intros) have "f ` {a..b} = {c..d}" unfolding f_def image_affinity_atLeastAtMost using assms sum_sqs_eq by (auto simp: field_split_simps) then show "f ` cbox a b = cbox c d" by auto show "inj_on f (cbox a b)" unfolding f_def inj_on_def using assms by auto qed auto then obtain g where "homeomorphism (cbox a b) (cbox c d) f g" .. then show ?thesis proof show "f a = c" by (simp add: f_def) show "f b = d" using assms sum_sqs_eq [of a b] by (auto simp: f_def field_split_simps) qed qed lemma homeomorphism_grouping_point_2: fixes a::real and w::real assumes hom_ab: "homeomorphism (cbox a b) (cbox u v) f1 g1" and hom_bc: "homeomorphism (cbox b c) (cbox v w) f2 g2" and "b \ cbox a c" "v \ cbox u w" and eq: "f1 a = u" "f1 b = v" "f2 b = v" "f2 c = w" obtains f g where "homeomorphism (cbox a c) (cbox u w) f g" "f a = u" "f c = w" "\x. x \ cbox a b \ f x = f1 x" "\x. x \ cbox b c \ f x = f2 x" proof - have le: "a \ b" "b \ c" "u \ v" "v \ w" using assms by simp_all then have ac: "cbox a c = cbox a b \ cbox b c" and uw: "cbox u w = cbox u v \ cbox v w" by auto define f where "f \ \x. if x \ b then f1 x else f2 x" have "\g. homeomorphism (cbox a c) (cbox u w) f g" proof (rule homeomorphism_compact) have cf1: "continuous_on (cbox a b) f1" using hom_ab homeomorphism_cont1 by blast have cf2: "continuous_on (cbox b c) f2" using hom_bc homeomorphism_cont1 by blast show "continuous_on (cbox a c) f" unfolding f_def using le eq by (force intro: continuous_on_cases_le [OF continuous_on_subset [OF cf1] continuous_on_subset [OF cf2]]) have "f ` cbox a b = f1 ` cbox a b" "f ` cbox b c = f2 ` cbox b c" unfolding f_def using eq by force+ then show "f ` cbox a c = cbox u w" unfolding ac uw image_Un by (metis hom_ab hom_bc homeomorphism_def) have neq12: "f1 x \ f2 y" if x: "a \ x" "x \ b" and y: "b < y" "y \ c" for x y proof - have "f1 x \ cbox u v" by (metis hom_ab homeomorphism_def image_eqI mem_box_real(2) x) moreover have "f2 y \ cbox v w" by (metis (full_types) hom_bc homeomorphism_def image_subset_iff mem_box_real(2) not_le not_less_iff_gr_or_eq order_refl y) moreover have "f2 y \ f2 b" by (metis cancel_comm_monoid_add_class.diff_cancel diff_gt_0_iff_gt hom_bc homeomorphism_def le(2) less_imp_le less_numeral_extra(3) mem_box_real(2) order_refl y) ultimately show ?thesis using le eq by simp qed have "inj_on f1 (cbox a b)" by (metis (full_types) hom_ab homeomorphism_def inj_onI) moreover have "inj_on f2 (cbox b c)" by (metis (full_types) hom_bc homeomorphism_def inj_onI) ultimately show "inj_on f (cbox a c)" apply (simp (no_asm) add: inj_on_def) apply (simp add: f_def inj_on_eq_iff) using neq12 by force qed auto then obtain g where "homeomorphism (cbox a c) (cbox u w) f g" .. then show ?thesis using eq f_def le that by force qed lemma homeomorphism_grouping_point_3: fixes a::real assumes cbox_sub: "cbox c d \ box a b" "cbox u v \ box a b" and box_ne: "box c d \ {}" "box u v \ {}" obtains f g where "homeomorphism (cbox a b) (cbox a b) f g" "f a = a" "f b = b" "\x. x \ cbox c d \ f x \ cbox u v" proof - have less: "a < c" "a < u" "d < b" "v < b" "c < d" "u < v" "cbox c d \ {}" using assms by (simp_all add: cbox_sub subset_eq) obtain f1 g1 where 1: "homeomorphism (cbox a c) (cbox a u) f1 g1" and f1_eq: "f1 a = a" "f1 c = u" using homeomorphism_grouping_point_1 [OF \a < c\ \a < u\] . obtain f2 g2 where 2: "homeomorphism (cbox c d) (cbox u v) f2 g2" and f2_eq: "f2 c = u" "f2 d = v" using homeomorphism_grouping_point_1 [OF \c < d\ \u < v\] . obtain f3 g3 where 3: "homeomorphism (cbox d b) (cbox v b) f3 g3" and f3_eq: "f3 d = v" "f3 b = b" using homeomorphism_grouping_point_1 [OF \d < b\ \v < b\] . obtain f4 g4 where 4: "homeomorphism (cbox a d) (cbox a v) f4 g4" and "f4 a = a" "f4 d = v" and f4_eq: "\x. x \ cbox a c \ f4 x = f1 x" "\x. x \ cbox c d \ f4 x = f2 x" using homeomorphism_grouping_point_2 [OF 1 2] less by (auto simp: f1_eq f2_eq) obtain f g where fg: "homeomorphism (cbox a b) (cbox a b) f g" "f a = a" "f b = b" and f_eq: "\x. x \ cbox a d \ f x = f4 x" "\x. x \ cbox d b \ f x = f3 x" using homeomorphism_grouping_point_2 [OF 4 3] less by (auto simp: f4_eq f3_eq f2_eq f1_eq) show ?thesis proof (rule that [OF fg]) show "f x \ cbox u v" if "x \ cbox c d" for x using that f4_eq f_eq homeomorphism_image1 [OF 2] by (metis atLeastAtMost_iff box_real(2) image_eqI less(1) less_eq_real_def order_trans) qed qed lemma homeomorphism_grouping_point_4: fixes T :: "real set" assumes "open U" "open S" "connected S" "U \ {}" "finite K" "K \ S" "U \ S" "S \ T" obtains f g where "homeomorphism T T f g" "\x. x \ K \ f x \ U" "{x. (\ (f x = x \ g x = x))} \ S" "bounded {x. (\ (f x = x \ g x = x))}" proof - obtain c d where "box c d \ {}" "cbox c d \ U" proof - obtain u where "u \ U" using \U \ {}\ by blast then obtain e where "e > 0" "cball u e \ U" using \open U\ open_contains_cball by blast then show ?thesis by (rule_tac c=u and d="u+e" in that) (auto simp: dist_norm subset_iff) qed have "compact K" by (simp add: \finite K\ finite_imp_compact) obtain a b where "box a b \ {}" "K \ cbox a b" "cbox a b \ S" proof (cases "K = {}") case True then show ?thesis using \box c d \ {}\ \cbox c d \ U\ \U \ S\ that by blast next case False then obtain a b where "a \ K" "b \ K" and a: "\x. x \ K \ a \ x" and b: "\x. x \ K \ x \ b" using compact_attains_inf compact_attains_sup by (metis \compact K\)+ obtain e where "e > 0" "cball b e \ S" using \open S\ open_contains_cball by (metis \b \ K\ \K \ S\ subsetD) show ?thesis proof show "box a (b + e) \ {}" using \0 < e\ \b \ K\ a by force show "K \ cbox a (b + e)" using \0 < e\ a b by fastforce have "a \ S" using \a \ K\ assms(6) by blast have "b + e \ S" using \0 < e\ \cball b e \ S\ by (force simp: dist_norm) show "cbox a (b + e) \ S" using \a \ S\ \b + e \ S\ \connected S\ connected_contains_Icc by auto qed qed obtain w z where "cbox w z \ S" and sub_wz: "cbox a b \ cbox c d \ box w z" proof - have "a \ S" "b \ S" using \box a b \ {}\ \cbox a b \ S\ by auto moreover have "c \ S" "d \ S" using \box c d \ {}\ \cbox c d \ U\ \U \ S\ by force+ ultimately have "min a c \ S" "max b d \ S" by linarith+ then obtain e1 e2 where "e1 > 0" "cball (min a c) e1 \ S" "e2 > 0" "cball (max b d) e2 \ S" using \open S\ open_contains_cball by metis then have *: "min a c - e1 \ S" "max b d + e2 \ S" by (auto simp: dist_norm) show ?thesis proof show "cbox (min a c - e1) (max b d+ e2) \ S" using * \connected S\ connected_contains_Icc by auto show "cbox a b \ cbox c d \ box (min a c - e1) (max b d + e2)" using \0 < e1\ \0 < e2\ by auto qed qed then obtain f g where hom: "homeomorphism (cbox w z) (cbox w z) f g" and "f w = w" "f z = z" and fin: "\x. x \ cbox a b \ f x \ cbox c d" using homeomorphism_grouping_point_3 [of a b w z c d] using \box a b \ {}\ \box c d \ {}\ by blast have contfg: "continuous_on (cbox w z) f" "continuous_on (cbox w z) g" using hom homeomorphism_def by blast+ define f' where "f' \ \x. if x \ cbox w z then f x else x" define g' where "g' \ \x. if x \ cbox w z then g x else x" show ?thesis proof have T: "cbox w z \ (T - box w z) = T" using \cbox w z \ S\ \S \ T\ by auto show "homeomorphism T T f' g'" proof have clo: "closedin (top_of_set (cbox w z \ (T - box w z))) (T - box w z)" by (metis Diff_Diff_Int Diff_subset T closedin_def open_box openin_open_Int topspace_euclidean_subtopology) have "\x. \w \ x \ x \ z; w < x \ \ x < z\ \ f x = x" using \f w = w\ \f z = z\ by auto moreover have "\x. \w \ x \ x \ z; w < x \ \ x < z\ \ g x = x" using \f w = w\ \f z = z\ hom homeomorphism_apply1 by fastforce ultimately have "continuous_on (cbox w z \ (T - box w z)) f'" "continuous_on (cbox w z \ (T - box w z)) g'" unfolding f'_def g'_def by (intro continuous_on_cases_local contfg continuous_on_id clo; auto simp: closed_subset)+ then show "continuous_on T f'" "continuous_on T g'" by (simp_all only: T) show "f' ` T \ T" unfolding f'_def by clarsimp (metis \cbox w z \ S\ \S \ T\ subsetD hom homeomorphism_def imageI mem_box_real(2)) show "g' ` T \ T" unfolding g'_def by clarsimp (metis \cbox w z \ S\ \S \ T\ subsetD hom homeomorphism_def imageI mem_box_real(2)) show "\x. x \ T \ g' (f' x) = x" unfolding f'_def g'_def using homeomorphism_apply1 [OF hom] homeomorphism_image1 [OF hom] by fastforce show "\y. y \ T \ f' (g' y) = y" unfolding f'_def g'_def using homeomorphism_apply2 [OF hom] homeomorphism_image2 [OF hom] by fastforce qed show "\x. x \ K \ f' x \ U" using fin sub_wz \K \ cbox a b\ \cbox c d \ U\ by (force simp: f'_def) show "{x. \ (f' x = x \ g' x = x)} \ S" using \cbox w z \ S\ by (auto simp: f'_def g'_def) show "bounded {x. \ (f' x = x \ g' x = x)}" proof (rule bounded_subset [of "cbox w z"]) show "bounded (cbox w z)" using bounded_cbox by blast show "{x. \ (f' x = x \ g' x = x)} \ cbox w z" by (auto simp: f'_def g'_def) qed qed qed proposition\<^marker>\tag unimportant\ homeomorphism_grouping_points_exists: fixes S :: "'a::euclidean_space set" assumes "open U" "open S" "connected S" "U \ {}" "finite K" "K \ S" "U \ S" "S \ T" obtains f g where "homeomorphism T T f g" "{x. (\ (f x = x \ g x = x))} \ S" "bounded {x. (\ (f x = x \ g x = x))}" "\x. x \ K \ f x \ U" proof (cases "2 \ DIM('a)") case True have TS: "T \ affine hull S" using affine_hull_open assms by blast have "infinite U" using \open U\ \U \ {}\ finite_imp_not_open by blast then obtain P where "P \ U" "finite P" "card K = card P" using infinite_arbitrarily_large by metis then obtain \ where \: "bij_betw \ K P" using \finite K\ finite_same_card_bij by blast obtain f g where "homeomorphism T T f g" "\i. i \ K \ f (id i) = \ i" "{x. \ (f x = x \ g x = x)} \ S" "bounded {x. \ (f x = x \ g x = x)}" proof (rule homeomorphism_moving_points_exists [OF True \open S\ \connected S\ \S \ T\ \finite K\]) show "\i. i \ K \ id i \ S \ \ i \ S" using \P \ U\ \bij_betw \ K P\ \K \ S\ \U \ S\ bij_betwE by blast show "pairwise (\i j. id i \ id j \ \ i \ \ j) K" using \ by (auto simp: pairwise_def bij_betw_def inj_on_def) qed (use affine_hull_open assms that in auto) then show ?thesis using \ \P \ U\ bij_betwE by (fastforce simp add: intro!: that) next case False with DIM_positive have "DIM('a) = 1" by (simp add: dual_order.antisym) then obtain h::"'a \real" and j where "linear h" "linear j" and noh: "\x. norm(h x) = norm x" and noj: "\y. norm(j y) = norm y" and hj: "\x. j(h x) = x" "\y. h(j y) = y" and ranh: "surj h" using isomorphisms_UNIV_UNIV by (metis (mono_tags, opaque_lifting) DIM_real UNIV_eq_I range_eqI) obtain f g where hom: "homeomorphism (h ` T) (h ` T) f g" and f: "\x. x \ h ` K \ f x \ h ` U" and sub: "{x. \ (f x = x \ g x = x)} \ h ` S" and bou: "bounded {x. \ (f x = x \ g x = x)}" apply (rule homeomorphism_grouping_point_4 [of "h ` U" "h ` S" "h ` K" "h ` T"]) by (simp_all add: assms image_mono \linear h\ open_surjective_linear_image connected_linear_image ranh) have jf: "j (f (h x)) = x \ f (h x) = h x" for x by (metis hj) have jg: "j (g (h x)) = x \ g (h x) = h x" for x by (metis hj) have cont_hj: "continuous_on X h" "continuous_on Y j" for X Y by (simp_all add: \linear h\ \linear j\ linear_linear linear_continuous_on) show ?thesis proof show "homeomorphism T T (j \ f \ h) (j \ g \ h)" proof show "continuous_on T (j \ f \ h)" "continuous_on T (j \ g \ h)" using hom homeomorphism_def by (blast intro: continuous_on_compose cont_hj)+ show "(j \ f \ h) ` T \ T" "(j \ g \ h) ` T \ T" by auto (metis (mono_tags, opaque_lifting) hj(1) hom homeomorphism_def imageE imageI)+ show "\x. x \ T \ (j \ g \ h) ((j \ f \ h) x) = x" using hj hom homeomorphism_apply1 by fastforce show "\y. y \ T \ (j \ f \ h) ((j \ g \ h) y) = y" using hj hom homeomorphism_apply2 by fastforce qed show "{x. \ ((j \ f \ h) x = x \ (j \ g \ h) x = x)} \ S" proof (clarsimp simp: jf jg hj) show "f (h x) = h x \ g (h x) \ h x \ x \ S" for x using sub [THEN subsetD, of "h x"] hj by simp (metis imageE) qed have "bounded (j ` {x. (\ (f x = x \ g x = x))})" by (rule bounded_linear_image [OF bou]) (use \linear j\ linear_conv_bounded_linear in auto) moreover have *: "{x. \((j \ f \ h) x = x \ (j \ g \ h) x = x)} = j ` {x. (\ (f x = x \ g x = x))}" using hj by (auto simp: jf jg image_iff, metis+) ultimately show "bounded {x. \ ((j \ f \ h) x = x \ (j \ g \ h) x = x)}" by metis show "\x. x \ K \ (j \ f \ h) x \ U" using f hj by fastforce qed qed proposition\<^marker>\tag unimportant\ homeomorphism_grouping_points_exists_gen: fixes S :: "'a::euclidean_space set" assumes opeU: "openin (top_of_set S) U" and opeS: "openin (top_of_set (affine hull S)) S" and "U \ {}" "finite K" "K \ S" and S: "S \ T" "T \ affine hull S" "connected S" obtains f g where "homeomorphism T T f g" "{x. (\ (f x = x \ g x = x))} \ S" "bounded {x. (\ (f x = x \ g x = x))}" "\x. x \ K \ f x \ U" proof (cases "2 \ aff_dim S") case True have opeU': "openin (top_of_set (affine hull S)) U" using opeS opeU openin_trans by blast obtain u where "u \ U" "u \ S" using \U \ {}\ opeU openin_imp_subset by fastforce+ have "infinite U" proof (rule infinite_openin [OF opeU \u \ U\]) show "u islimpt S" using True \u \ S\ assms(8) connected_imp_perfect_aff_dim by fastforce qed then obtain P where "P \ U" "finite P" "card K = card P" using infinite_arbitrarily_large by metis then obtain \ where \: "bij_betw \ K P" using \finite K\ finite_same_card_bij by blast have "\f g. homeomorphism T T f g \ (\i \ K. f(id i) = \ i) \ {x. \ (f x = x \ g x = x)} \ S \ bounded {x. \ (f x = x \ g x = x)}" proof (rule homeomorphism_moving_points_exists_gen [OF \finite K\ _ _ True opeS S]) show "\i. i \ K \ id i \ S \ \ i \ S" by (metis id_apply opeU openin_contains_cball subsetCE \P \ U\ \bij_betw \ K P\ \K \ S\ bij_betwE) show "pairwise (\i j. id i \ id j \ \ i \ \ j) K" using \ by (auto simp: pairwise_def bij_betw_def inj_on_def) qed then show ?thesis using \ \P \ U\ bij_betwE by (fastforce simp add: intro!: that) next case False with aff_dim_geq [of S] consider "aff_dim S = -1" | "aff_dim S = 0" | "aff_dim S = 1" by linarith then show ?thesis proof cases assume "aff_dim S = -1" then have "S = {}" using aff_dim_empty by blast then have "False" using \U \ {}\ \K \ S\ openin_imp_subset [OF opeU] by blast then show ?thesis .. next assume "aff_dim S = 0" then obtain a where "S = {a}" using aff_dim_eq_0 by blast then have "K \ U" using \U \ {}\ \K \ S\ openin_imp_subset [OF opeU] by blast show ?thesis using \K \ U\ by (intro that [of id id]) (auto intro: homeomorphismI) next assume "aff_dim S = 1" then have "affine hull S homeomorphic (UNIV :: real set)" by (auto simp: homeomorphic_affine_sets) then obtain h::"'a\real" and j where homhj: "homeomorphism (affine hull S) UNIV h j" using homeomorphic_def by blast then have h: "\x. x \ affine hull S \ j(h(x)) = x" and j: "\y. j y \ affine hull S \ h(j y) = y" by (auto simp: homeomorphism_def) have connh: "connected (h ` S)" by (meson Topological_Spaces.connected_continuous_image \connected S\ homeomorphism_cont1 homeomorphism_of_subsets homhj hull_subset top_greatest) have hUS: "h ` U \ h ` S" by (meson homeomorphism_imp_open_map homeomorphism_of_subsets homhj hull_subset opeS opeU open_UNIV openin_open_eq) have opn: "openin (top_of_set (affine hull S)) U \ open (h ` U)" for U using homeomorphism_imp_open_map [OF homhj] by simp have "open (h ` U)" "open (h ` S)" by (auto intro: opeS opeU openin_trans opn) then obtain f g where hom: "homeomorphism (h ` T) (h ` T) f g" and f: "\x. x \ h ` K \ f x \ h ` U" and sub: "{x. \ (f x = x \ g x = x)} \ h ` S" and bou: "bounded {x. \ (f x = x \ g x = x)}" apply (rule homeomorphism_grouping_points_exists [of "h ` U" "h ` S" "h ` K" "h ` T"]) using assms by (auto simp: connh hUS) have jf: "\x. x \ affine hull S \ j (f (h x)) = x \ f (h x) = h x" by (metis h j) have jg: "\x. x \ affine hull S \ j (g (h x)) = x \ g (h x) = h x" by (metis h j) have cont_hj: "continuous_on T h" "continuous_on Y j" for Y proof (rule continuous_on_subset [OF _ \T \ affine hull S\]) show "continuous_on (affine hull S) h" using homeomorphism_def homhj by blast qed (meson continuous_on_subset homeomorphism_def homhj top_greatest) define f' where "f' \ \x. if x \ affine hull S then (j \ f \ h) x else x" define g' where "g' \ \x. if x \ affine hull S then (j \ g \ h) x else x" show ?thesis proof show "homeomorphism T T f' g'" proof have "continuous_on T (j \ f \ h)" using hom homeomorphism_def by (intro continuous_on_compose cont_hj) blast then show "continuous_on T f'" apply (rule continuous_on_eq) using \T \ affine hull S\ f'_def by auto have "continuous_on T (j \ g \ h)" using hom homeomorphism_def by (intro continuous_on_compose cont_hj) blast then show "continuous_on T g'" apply (rule continuous_on_eq) using \T \ affine hull S\ g'_def by auto show "f' ` T \ T" proof (clarsimp simp: f'_def) fix x assume "x \ T" then have "f (h x) \ h ` T" by (metis (no_types) hom homeomorphism_def image_subset_iff subset_refl) then show "j (f (h x)) \ T" using \T \ affine hull S\ h by auto qed show "g' ` T \ T" proof (clarsimp simp: g'_def) fix x assume "x \ T" then have "g (h x) \ h ` T" by (metis (no_types) hom homeomorphism_def image_subset_iff subset_refl) then show "j (g (h x)) \ T" using \T \ affine hull S\ h by auto qed show "\x. x \ T \ g' (f' x) = x" using h j hom homeomorphism_apply1 by (fastforce simp add: f'_def g'_def) show "\y. y \ T \ f' (g' y) = y" using h j hom homeomorphism_apply2 by (fastforce simp add: f'_def g'_def) qed next have \
: "\x y. \x \ affine hull S; h x = h y; y \ S\ \ x \ S" by (metis h hull_inc) show "{x. \ (f' x = x \ g' x = x)} \ S" using sub by (simp add: f'_def g'_def jf jg) (force elim: \
) next have "compact (j ` closure {x. \ (f x = x \ g x = x)})" using bou by (auto simp: compact_continuous_image cont_hj) then have "bounded (j ` {x. \ (f x = x \ g x = x)})" by (rule bounded_closure_image [OF compact_imp_bounded]) moreover have *: "{x \ affine hull S. j (f (h x)) \ x \ j (g (h x)) \ x} = j ` {x. (\ (f x = x \ g x = x))}" using h j by (auto simp: image_iff; metis) ultimately have "bounded {x \ affine hull S. j (f (h x)) \ x \ j (g (h x)) \ x}" by metis then show "bounded {x. \ (f' x = x \ g' x = x)}" by (simp add: f'_def g'_def Collect_mono bounded_subset) next show "f' x \ U" if "x \ K" for x proof - have "U \ S" using opeU openin_imp_subset by blast then have "j (f (h x)) \ U" using f h hull_subset that by fastforce then show "f' x \ U" using \K \ S\ S f'_def that by auto qed qed qed qed subsection\Nullhomotopic mappings\ text\ A mapping out of a sphere is nullhomotopic iff it extends to the ball. This even works out in the degenerate cases when the radius is \\\ 0, and we also don't need to explicitly assume continuity since it's already implicit in both sides of the equivalence.\ lemma nullhomotopic_from_lemma: assumes contg: "continuous_on (cball a r - {a}) g" and fa: "\e. 0 < e \ \d. 0 < d \ (\x. x \ a \ norm(x - a) < d \ norm(g x - f a) < e)" and r: "\x. x \ cball a r \ x \ a \ f x = g x" shows "continuous_on (cball a r) f" proof (clarsimp simp: continuous_on_eq_continuous_within Ball_def) fix x assume x: "dist a x \ r" show "continuous (at x within cball a r) f" proof (cases "x=a") case True then show ?thesis by (metis continuous_within_eps_delta fa dist_norm dist_self r) next case False show ?thesis proof (rule continuous_transform_within [where f=g and d = "norm(x-a)"]) have "\d>0. \x'\cball a r. dist x' x < d \ dist (g x') (g x) < e" if "e>0" for e proof - obtain d where "d > 0" and d: "\x'. \dist x' a \ r; x' \ a; dist x' x < d\ \ dist (g x') (g x) < e" using contg False x \e>0\ unfolding continuous_on_iff by (fastforce simp add: dist_commute intro: that) show ?thesis using \d > 0\ \x \ a\ by (rule_tac x="min d (norm(x - a))" in exI) (auto simp: dist_commute dist_norm [symmetric] intro!: d) qed then show "continuous (at x within cball a r) g" using contg False by (auto simp: continuous_within_eps_delta) show "0 < norm (x - a)" using False by force show "x \ cball a r" by (simp add: x) show "\x'. \x' \ cball a r; dist x' x < norm (x - a)\ \ g x' = f x'" by (metis dist_commute dist_norm less_le r) qed qed qed proposition nullhomotopic_from_sphere_extension: fixes f :: "'M::euclidean_space \ 'a::real_normed_vector" shows "(\c. homotopic_with_canon (\x. True) (sphere a r) S f (\x. c)) \ (\g. continuous_on (cball a r) g \ g ` (cball a r) \ S \ (\x \ sphere a r. g x = f x))" (is "?lhs = ?rhs") proof (cases r "0::real" rule: linorder_cases) case less then show ?thesis by (simp add: homotopic_on_emptyI) next case equal show ?thesis proof assume L: ?lhs with equal have [simp]: "f a \ S" using homotopic_with_imp_subset1 by fastforce obtain h:: "real \ 'M \ 'a" where h: "continuous_on ({0..1} \ {a}) h" "h ` ({0..1} \ {a}) \ S" "h (0, a) = f a" using L equal by (auto simp: homotopic_with) then have "continuous_on (cball a r) (\x. h (0, a))" "(\x. h (0, a)) ` cball a r \ S" by (auto simp: equal) then show ?rhs using h(3) local.equal by force next assume ?rhs then show ?lhs using equal continuous_on_const by (force simp add: homotopic_with) qed next case greater let ?P = "continuous_on {x. norm(x - a) = r} f \ f ` {x. norm(x - a) = r} \ S" have ?P if ?lhs using that proof fix c assume c: "homotopic_with_canon (\x. True) (sphere a r) S f (\x. c)" then have contf: "continuous_on (sphere a r) f" by (metis homotopic_with_imp_continuous) moreover have fim: "f ` sphere a r \ S" by (meson continuous_map_subtopology_eu c homotopic_with_imp_continuous_maps) show ?P using contf fim by (auto simp: sphere_def dist_norm norm_minus_commute) qed moreover have ?P if ?rhs using that proof fix g assume g: "continuous_on (cball a r) g \ g ` cball a r \ S \ (\xa\sphere a r. g xa = f xa)" then have "f ` {x. norm (x - a) = r} \ S" using sphere_cball [of a r] unfolding image_subset_iff sphere_def by (metis dist_commute dist_norm mem_Collect_eq subset_eq) with g show ?P by (auto simp: dist_norm norm_minus_commute elim!: continuous_on_eq [OF continuous_on_subset]) qed moreover have ?thesis if ?P proof assume ?lhs then obtain c where "homotopic_with_canon (\x. True) (sphere a r) S (\x. c) f" using homotopic_with_sym by blast then obtain h where conth: "continuous_on ({0..1::real} \ sphere a r) h" and him: "h ` ({0..1} \ sphere a r) \ S" and h: "\x. h(0, x) = c" "\x. h(1, x) = f x" by (auto simp: homotopic_with_def) obtain b1::'M where "b1 \ Basis" using SOME_Basis by auto have "c \ h ` ({0..1} \ sphere a r)" proof show "c = h (0, a + r *\<^sub>R b1)" by (simp add: h) show "(0, a + r *\<^sub>R b1) \ {0..1::real} \ sphere a r" using greater \b1 \ Basis\ by (auto simp: dist_norm) qed then have "c \ S" using him by blast have uconth: "uniformly_continuous_on ({0..1::real} \ (sphere a r)) h" by (force intro: compact_Times conth compact_uniformly_continuous) let ?g = "\x. h (norm (x - a)/r, a + (if x = a then r *\<^sub>R b1 else (r / norm(x - a)) *\<^sub>R (x - a)))" let ?g' = "\x. h (norm (x - a)/r, a + (r / norm(x - a)) *\<^sub>R (x - a))" show ?rhs proof (intro exI conjI) have "continuous_on (cball a r - {a}) ?g'" using greater by (force simp: dist_norm norm_minus_commute intro: continuous_on_compose2 [OF conth] continuous_intros) then show "continuous_on (cball a r) ?g" proof (rule nullhomotopic_from_lemma) show "\d>0. \x. x \ a \ norm (x - a) < d \ norm (?g' x - ?g a) < e" if "0 < e" for e proof - obtain d where "0 < d" and d: "\x x'. \x \ {0..1} \ sphere a r; x' \ {0..1} \ sphere a r; norm ( x' - x) < d\ \ norm (h x' - h x) < e" using uniformly_continuous_onE [OF uconth \0 < e\] by (auto simp: dist_norm) have *: "norm (h (norm (x - a) / r, a + (r / norm (x - a)) *\<^sub>R (x - a)) - h (0, a + r *\<^sub>R b1)) < e" (is "norm (?ha - ?hb) < e") if "x \ a" "norm (x - a) < r" "norm (x - a) < d * r" for x proof - have "norm (?ha - ?hb) = norm (?ha - h (0, a + (r / norm (x - a)) *\<^sub>R (x - a)))" by (simp add: h) also have "\ < e" using greater \0 < d\ \b1 \ Basis\ that by (intro d) (simp_all add: dist_norm, simp add: field_simps) finally show ?thesis . qed show ?thesis using greater \0 < d\ by (rule_tac x = "min r (d * r)" in exI) (auto simp: *) qed show "\x. x \ cball a r \ x \ a \ ?g x = ?g' x" by auto qed next show "?g ` cball a r \ S" using greater him \c \ S\ by (force simp: h dist_norm norm_minus_commute) next show "\x\sphere a r. ?g x = f x" using greater by (auto simp: h dist_norm norm_minus_commute) qed next assume ?rhs then obtain g where contg: "continuous_on (cball a r) g" and gim: "g ` cball a r \ S" and gf: "\x \ sphere a r. g x = f x" by auto let ?h = "\y. g (a + (fst y) *\<^sub>R (snd y - a))" have "continuous_on ({0..1} \ sphere a r) ?h" proof (rule continuous_on_compose2 [OF contg]) show "continuous_on ({0..1} \ sphere a r) (\x. a + fst x *\<^sub>R (snd x - a))" by (intro continuous_intros) qed (auto simp: dist_norm norm_minus_commute mult_left_le_one_le) moreover have "?h ` ({0..1} \ sphere a r) \ S" by (auto simp: dist_norm norm_minus_commute mult_left_le_one_le gim [THEN subsetD]) moreover have "\x\sphere a r. ?h (0, x) = g a" "\x\sphere a r. ?h (1, x) = f x" by (auto simp: dist_norm norm_minus_commute mult_left_le_one_le gf) ultimately have "homotopic_with_canon (\x. True) (sphere a r) S (\x. g a) f" by (auto simp: homotopic_with) then show ?lhs using homotopic_with_symD by blast qed ultimately show ?thesis by meson qed end \ No newline at end of file