src/HOL/Analysis/Homeomorphism.thy
 author paulson Thu Apr 19 16:10:06 2018 +0100 (16 months ago) changeset 68006 a1a023f08c8f parent 67399 eab6ce8368fa child 68069 36209dfb981e permissions -rw-r--r--
tuning of a proof
 hoelzl@63627 ` 1` ```(* Title: HOL/Analysis/Homeomorphism.thy ``` lp15@63130 ` 2` ``` Author: LC Paulson (ported from HOL Light) ``` lp15@63130 ` 3` ```*) ``` lp15@63130 ` 4` lp15@63130 ` 5` ```section \Homeomorphism Theorems\ ``` lp15@63130 ` 6` lp15@63130 ` 7` ```theory Homeomorphism ``` lp15@63130 ` 8` ```imports Path_Connected ``` lp15@63130 ` 9` ```begin ``` lp15@63130 ` 10` lp15@64789 ` 11` ```lemma homeomorphic_spheres': ``` lp15@64789 ` 12` ``` fixes a ::"'a::euclidean_space" and b ::"'b::euclidean_space" ``` lp15@64789 ` 13` ``` assumes "0 < \" and dimeq: "DIM('a) = DIM('b)" ``` lp15@64789 ` 14` ``` shows "(sphere a \) homeomorphic (sphere b \)" ``` lp15@64789 ` 15` ```proof - ``` lp15@64789 ` 16` ``` obtain f :: "'a\'b" and g where "linear f" "linear g" ``` lp15@64789 ` 17` ``` and fg: "\x. norm(f x) = norm x" "\y. norm(g y) = norm y" "\x. g(f x) = x" "\y. f(g y) = y" ``` lp15@64789 ` 18` ``` by (blast intro: isomorphisms_UNIV_UNIV [OF dimeq]) ``` lp15@64789 ` 19` ``` then have "continuous_on UNIV f" "continuous_on UNIV g" ``` lp15@64789 ` 20` ``` using linear_continuous_on linear_linear by blast+ ``` lp15@64789 ` 21` ``` then show ?thesis ``` lp15@64789 ` 22` ``` unfolding homeomorphic_minimal ``` lp15@64789 ` 23` ``` apply(rule_tac x="\x. b + f(x - a)" in exI) ``` lp15@64789 ` 24` ``` apply(rule_tac x="\x. a + g(x - b)" in exI) ``` lp15@64789 ` 25` ``` using assms ``` lp15@64789 ` 26` ``` apply (force intro: continuous_intros ``` lp15@64789 ` 27` ``` continuous_on_compose2 [of _ f] continuous_on_compose2 [of _ g] simp: dist_commute dist_norm fg) ``` lp15@64789 ` 28` ``` done ``` lp15@64789 ` 29` ```qed ``` lp15@64789 ` 30` lp15@64789 ` 31` ```lemma homeomorphic_spheres_gen: ``` lp15@64789 ` 32` ``` fixes a :: "'a::euclidean_space" and b :: "'b::euclidean_space" ``` lp15@64789 ` 33` ``` assumes "0 < r" "0 < s" "DIM('a::euclidean_space) = DIM('b::euclidean_space)" ``` lp15@64789 ` 34` ``` shows "(sphere a r homeomorphic sphere b s)" ``` lp15@64789 ` 35` ``` apply (rule homeomorphic_trans [OF homeomorphic_spheres homeomorphic_spheres']) ``` lp15@64789 ` 36` ``` using assms apply auto ``` lp15@64789 ` 37` ``` done ``` lp15@64789 ` 38` lp15@63130 ` 39` ```subsection \Homeomorphism of all convex compact sets with nonempty interior\ ``` lp15@63130 ` 40` lp15@63130 ` 41` ```proposition ray_to_rel_frontier: ``` lp15@63130 ` 42` ``` fixes a :: "'a::real_inner" ``` lp15@63130 ` 43` ``` assumes "bounded S" ``` lp15@63130 ` 44` ``` and a: "a \ rel_interior S" ``` lp15@63130 ` 45` ``` and aff: "(a + l) \ affine hull S" ``` lp15@63130 ` 46` ``` and "l \ 0" ``` lp15@63130 ` 47` ``` obtains d where "0 < d" "(a + d *\<^sub>R l) \ rel_frontier S" ``` lp15@63130 ` 48` ``` "\e. \0 \ e; e < d\ \ (a + e *\<^sub>R l) \ rel_interior S" ``` lp15@63130 ` 49` ```proof - ``` lp15@63130 ` 50` ``` have aaff: "a \ affine hull S" ``` lp15@63130 ` 51` ``` by (meson a hull_subset rel_interior_subset rev_subsetD) ``` lp15@63130 ` 52` ``` let ?D = "{d. 0 < d \ a + d *\<^sub>R l \ rel_interior S}" ``` lp15@63130 ` 53` ``` obtain B where "B > 0" and B: "S \ ball a B" ``` lp15@63130 ` 54` ``` using bounded_subset_ballD [OF \bounded S\] by blast ``` lp15@63130 ` 55` ``` have "a + (B / norm l) *\<^sub>R l \ ball a B" ``` lp15@63130 ` 56` ``` by (simp add: dist_norm \l \ 0\) ``` lp15@63130 ` 57` ``` with B have "a + (B / norm l) *\<^sub>R l \ rel_interior S" ``` lp15@63130 ` 58` ``` using rel_interior_subset subsetCE by blast ``` lp15@63130 ` 59` ``` with \B > 0\ \l \ 0\ have nonMT: "?D \ {}" ``` lp15@63130 ` 60` ``` using divide_pos_pos zero_less_norm_iff by fastforce ``` lp15@63130 ` 61` ``` have bdd: "bdd_below ?D" ``` lp15@63130 ` 62` ``` by (metis (no_types, lifting) bdd_belowI le_less mem_Collect_eq) ``` lp15@63130 ` 63` ``` have relin_Ex: "\x. x \ rel_interior S \ ``` lp15@63130 ` 64` ``` \e>0. \x'\affine hull S. dist x' x < e \ x' \ rel_interior S" ``` lp15@63130 ` 65` ``` using openin_rel_interior [of S] by (simp add: openin_euclidean_subtopology_iff) ``` lp15@63130 ` 66` ``` define d where "d = Inf ?D" ``` lp15@63130 ` 67` ``` obtain \ where "0 < \" and \: "\\. \0 \ \; \ < \\ \ (a + \ *\<^sub>R l) \ rel_interior S" ``` lp15@63130 ` 68` ``` proof - ``` lp15@63130 ` 69` ``` obtain e where "e>0" ``` lp15@63130 ` 70` ``` and e: "\x'. x' \ affine hull S \ dist x' a < e \ x' \ rel_interior S" ``` lp15@63130 ` 71` ``` using relin_Ex a by blast ``` lp15@63130 ` 72` ``` show thesis ``` lp15@63130 ` 73` ``` proof (rule_tac \ = "e / norm l" in that) ``` lp15@63130 ` 74` ``` show "0 < e / norm l" by (simp add: \0 < e\ \l \ 0\) ``` lp15@63130 ` 75` ``` next ``` lp15@63130 ` 76` ``` show "a + \ *\<^sub>R l \ rel_interior S" if "0 \ \" "\ < e / norm l" for \ ``` lp15@63130 ` 77` ``` proof (rule e) ``` lp15@63130 ` 78` ``` show "a + \ *\<^sub>R l \ affine hull S" ``` lp15@63130 ` 79` ``` by (metis (no_types) add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff) ``` lp15@63130 ` 80` ``` show "dist (a + \ *\<^sub>R l) a < e" ``` lp15@63130 ` 81` ``` using that by (simp add: \l \ 0\ dist_norm pos_less_divide_eq) ``` lp15@63130 ` 82` ``` qed ``` lp15@63130 ` 83` ``` qed ``` lp15@63130 ` 84` ``` qed ``` lp15@63130 ` 85` ``` have inint: "\e. \0 \ e; e < d\ \ a + e *\<^sub>R l \ rel_interior S" ``` lp15@63130 ` 86` ``` unfolding d_def using cInf_lower [OF _ bdd] ``` lp15@63130 ` 87` ``` by (metis (no_types, lifting) a add.right_neutral le_less mem_Collect_eq not_less real_vector.scale_zero_left) ``` lp15@63130 ` 88` ``` have "\ \ d" ``` lp15@63130 ` 89` ``` unfolding d_def ``` lp15@63130 ` 90` ``` apply (rule cInf_greatest [OF nonMT]) ``` lp15@63130 ` 91` ``` using \ dual_order.strict_implies_order le_less_linear by blast ``` lp15@63130 ` 92` ``` with \0 < \\ have "0 < d" by simp ``` lp15@63130 ` 93` ``` have "a + d *\<^sub>R l \ rel_interior S" ``` lp15@63130 ` 94` ``` proof ``` lp15@63130 ` 95` ``` assume adl: "a + d *\<^sub>R l \ rel_interior S" ``` lp15@63130 ` 96` ``` obtain e where "e > 0" ``` lp15@63130 ` 97` ``` and e: "\x'. x' \ affine hull S \ dist x' (a + d *\<^sub>R l) < e \ x' \ rel_interior S" ``` lp15@63130 ` 98` ``` using relin_Ex adl by blast ``` lp15@63130 ` 99` ``` have "d + e / norm l \ Inf {d. 0 < d \ a + d *\<^sub>R l \ rel_interior S}" ``` lp15@63130 ` 100` ``` proof (rule cInf_greatest [OF nonMT], clarsimp) ``` lp15@63130 ` 101` ``` fix x::real ``` lp15@63130 ` 102` ``` assume "0 < x" and nonrel: "a + x *\<^sub>R l \ rel_interior S" ``` lp15@63130 ` 103` ``` show "d + e / norm l \ x" ``` lp15@63130 ` 104` ``` proof (cases "x < d") ``` lp15@63130 ` 105` ``` case True with inint nonrel \0 < x\ ``` lp15@63130 ` 106` ``` show ?thesis by auto ``` lp15@63130 ` 107` ``` next ``` lp15@63130 ` 108` ``` case False ``` lp15@63130 ` 109` ``` then have dle: "x < d + e / norm l \ dist (a + x *\<^sub>R l) (a + d *\<^sub>R l) < e" ``` lp15@63130 ` 110` ``` by (simp add: field_simps \l \ 0\) ``` lp15@63130 ` 111` ``` have ain: "a + x *\<^sub>R l \ affine hull S" ``` lp15@63130 ` 112` ``` by (metis add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff) ``` lp15@63130 ` 113` ``` show ?thesis ``` lp15@63130 ` 114` ``` using e [OF ain] nonrel dle by force ``` lp15@63130 ` 115` ``` qed ``` lp15@63130 ` 116` ``` qed ``` lp15@63130 ` 117` ``` then show False ``` lp15@63130 ` 118` ``` using \0 < e\ \l \ 0\ by (simp add: d_def [symmetric] divide_simps) ``` lp15@63130 ` 119` ``` qed ``` lp15@63130 ` 120` ``` moreover have "a + d *\<^sub>R l \ closure S" ``` lp15@63130 ` 121` ``` proof (clarsimp simp: closure_approachable) ``` lp15@63130 ` 122` ``` fix \::real assume "0 < \" ``` lp15@63130 ` 123` ``` have 1: "a + (d - min d (\ / 2 / norm l)) *\<^sub>R l \ S" ``` lp15@63130 ` 124` ``` apply (rule subsetD [OF rel_interior_subset inint]) ``` lp15@63130 ` 125` ``` using \l \ 0\ \0 < d\ \0 < \\ by auto ``` lp15@63130 ` 126` ``` have "norm l * min d (\ / (norm l * 2)) \ norm l * (\ / (norm l * 2))" ``` lp15@63130 ` 127` ``` by (metis min_def mult_left_mono norm_ge_zero order_refl) ``` lp15@63130 ` 128` ``` also have "... < \" ``` lp15@63130 ` 129` ``` using \l \ 0\ \0 < \\ by (simp add: divide_simps) ``` lp15@63130 ` 130` ``` finally have 2: "norm l * min d (\ / (norm l * 2)) < \" . ``` lp15@63130 ` 131` ``` show "\y\S. dist y (a + d *\<^sub>R l) < \" ``` lp15@63130 ` 132` ``` apply (rule_tac x="a + (d - min d (\ / 2 / norm l)) *\<^sub>R l" in bexI) ``` lp15@63130 ` 133` ``` using 1 2 \0 < d\ \0 < \\ apply (auto simp: algebra_simps) ``` lp15@63130 ` 134` ``` done ``` lp15@63130 ` 135` ``` qed ``` lp15@63130 ` 136` ``` ultimately have infront: "a + d *\<^sub>R l \ rel_frontier S" ``` lp15@63130 ` 137` ``` by (simp add: rel_frontier_def) ``` lp15@63130 ` 138` ``` show ?thesis ``` lp15@63130 ` 139` ``` by (rule that [OF \0 < d\ infront inint]) ``` lp15@63130 ` 140` ```qed ``` lp15@63130 ` 141` lp15@63130 ` 142` ```corollary ray_to_frontier: ``` lp15@63130 ` 143` ``` fixes a :: "'a::euclidean_space" ``` lp15@63130 ` 144` ``` assumes "bounded S" ``` lp15@63130 ` 145` ``` and a: "a \ interior S" ``` lp15@63130 ` 146` ``` and "l \ 0" ``` lp15@63130 ` 147` ``` obtains d where "0 < d" "(a + d *\<^sub>R l) \ frontier S" ``` lp15@63130 ` 148` ``` "\e. \0 \ e; e < d\ \ (a + e *\<^sub>R l) \ interior S" ``` lp15@63130 ` 149` ```proof - ``` lp15@63130 ` 150` ``` have "interior S = rel_interior S" ``` lp15@63130 ` 151` ``` using a rel_interior_nonempty_interior by auto ``` lp15@63130 ` 152` ``` then have "a \ rel_interior S" ``` lp15@63130 ` 153` ``` using a by simp ``` lp15@63130 ` 154` ``` then show ?thesis ``` lp15@63130 ` 155` ``` apply (rule ray_to_rel_frontier [OF \bounded S\ _ _ \l \ 0\]) ``` lp15@63130 ` 156` ``` using a affine_hull_nonempty_interior apply blast ``` lp15@63130 ` 157` ``` by (simp add: \interior S = rel_interior S\ frontier_def rel_frontier_def that) ``` lp15@63130 ` 158` ```qed ``` lp15@63130 ` 159` lp15@66287 ` 160` lp15@66287 ` 161` ```lemma segment_to_rel_frontier_aux: ``` lp15@66287 ` 162` ``` fixes x :: "'a::euclidean_space" ``` lp15@66287 ` 163` ``` assumes "convex S" "bounded S" and x: "x \ rel_interior S" and y: "y \ S" and xy: "x \ y" ``` lp15@66287 ` 164` ``` obtains z where "z \ rel_frontier S" "y \ closed_segment x z" ``` lp15@66287 ` 165` ``` "open_segment x z \ rel_interior S" ``` lp15@66287 ` 166` ```proof - ``` lp15@66287 ` 167` ``` have "x + (y - x) \ affine hull S" ``` lp15@66287 ` 168` ``` using hull_inc [OF y] by auto ``` lp15@66287 ` 169` ``` then obtain d where "0 < d" and df: "(x + d *\<^sub>R (y-x)) \ rel_frontier S" ``` lp15@66287 ` 170` ``` and di: "\e. \0 \ e; e < d\ \ (x + e *\<^sub>R (y-x)) \ rel_interior S" ``` lp15@66287 ` 171` ``` by (rule ray_to_rel_frontier [OF \bounded S\ x]) (use xy in auto) ``` lp15@66287 ` 172` ``` show ?thesis ``` lp15@66287 ` 173` ``` proof ``` lp15@66287 ` 174` ``` show "x + d *\<^sub>R (y - x) \ rel_frontier S" ``` lp15@66287 ` 175` ``` by (simp add: df) ``` lp15@66287 ` 176` ``` next ``` lp15@66287 ` 177` ``` have "open_segment x y \ rel_interior S" ``` lp15@66287 ` 178` ``` using rel_interior_closure_convex_segment [OF \convex S\ x] closure_subset y by blast ``` lp15@66287 ` 179` ``` moreover have "x + d *\<^sub>R (y - x) \ open_segment x y" if "d < 1" ``` lp15@66287 ` 180` ``` using xy ``` lp15@66287 ` 181` ``` apply (auto simp: in_segment) ``` lp15@66287 ` 182` ``` apply (rule_tac x="d" in exI) ``` lp15@66287 ` 183` ``` using \0 < d\ that apply (auto simp: divide_simps algebra_simps) ``` lp15@66287 ` 184` ``` done ``` lp15@66287 ` 185` ``` ultimately have "1 \ d" ``` lp15@66287 ` 186` ``` using df rel_frontier_def by fastforce ``` lp15@66287 ` 187` ``` moreover have "x = (1 / d) *\<^sub>R x + ((d - 1) / d) *\<^sub>R x" ``` lp15@66287 ` 188` ``` by (metis \0 < d\ add.commute add_divide_distrib diff_add_cancel divide_self_if less_irrefl scaleR_add_left scaleR_one) ``` lp15@66287 ` 189` ``` ultimately show "y \ closed_segment x (x + d *\<^sub>R (y - x))" ``` lp15@66287 ` 190` ``` apply (auto simp: in_segment) ``` lp15@66287 ` 191` ``` apply (rule_tac x="1/d" in exI) ``` lp15@66287 ` 192` ``` apply (auto simp: divide_simps algebra_simps) ``` lp15@66287 ` 193` ``` done ``` lp15@66287 ` 194` ``` next ``` lp15@66287 ` 195` ``` show "open_segment x (x + d *\<^sub>R (y - x)) \ rel_interior S" ``` lp15@66287 ` 196` ``` apply (rule rel_interior_closure_convex_segment [OF \convex S\ x]) ``` lp15@66287 ` 197` ``` using df rel_frontier_def by auto ``` lp15@66287 ` 198` ``` qed ``` lp15@66287 ` 199` ```qed ``` lp15@66287 ` 200` lp15@66287 ` 201` ```lemma segment_to_rel_frontier: ``` lp15@66287 ` 202` ``` fixes x :: "'a::euclidean_space" ``` lp15@66287 ` 203` ``` assumes S: "convex S" "bounded S" and x: "x \ rel_interior S" ``` lp15@66287 ` 204` ``` and y: "y \ S" and xy: "~(x = y \ S = {x})" ``` lp15@66287 ` 205` ``` obtains z where "z \ rel_frontier S" "y \ closed_segment x z" ``` lp15@66287 ` 206` ``` "open_segment x z \ rel_interior S" ``` lp15@66287 ` 207` ```proof (cases "x=y") ``` lp15@66287 ` 208` ``` case True ``` lp15@66287 ` 209` ``` with xy have "S \ {x}" ``` lp15@66287 ` 210` ``` by blast ``` lp15@66287 ` 211` ``` with True show ?thesis ``` lp15@66287 ` 212` ``` by (metis Set.set_insert all_not_in_conv ends_in_segment(1) insert_iff segment_to_rel_frontier_aux[OF S x] that y) ``` lp15@66287 ` 213` ```next ``` lp15@66287 ` 214` ``` case False ``` lp15@66287 ` 215` ``` then show ?thesis ``` lp15@66287 ` 216` ``` using segment_to_rel_frontier_aux [OF S x y] that by blast ``` lp15@66287 ` 217` ```qed ``` lp15@66287 ` 218` lp15@64394 ` 219` ```proposition rel_frontier_not_sing: ``` lp15@64394 ` 220` ``` fixes a :: "'a::euclidean_space" ``` lp15@64394 ` 221` ``` assumes "bounded S" ``` lp15@64394 ` 222` ``` shows "rel_frontier S \ {a}" ``` lp15@64394 ` 223` ```proof (cases "S = {}") ``` lp15@64394 ` 224` ``` case True then show ?thesis by simp ``` lp15@64394 ` 225` ```next ``` lp15@64394 ` 226` ``` case False ``` lp15@64394 ` 227` ``` then obtain z where "z \ S" ``` lp15@64394 ` 228` ``` by blast ``` lp15@64394 ` 229` ``` then show ?thesis ``` lp15@64394 ` 230` ``` proof (cases "S = {z}") ``` lp15@64394 ` 231` ``` case True then show ?thesis by simp ``` lp15@64394 ` 232` ``` next ``` lp15@64394 ` 233` ``` case False ``` lp15@64394 ` 234` ``` then obtain w where "w \ S" "w \ z" ``` lp15@64394 ` 235` ``` using \z \ S\ by blast ``` lp15@64394 ` 236` ``` show ?thesis ``` lp15@64394 ` 237` ``` proof ``` lp15@64394 ` 238` ``` assume "rel_frontier S = {a}" ``` lp15@64394 ` 239` ``` then consider "w \ rel_frontier S" | "z \ rel_frontier S" ``` lp15@64394 ` 240` ``` using \w \ z\ by auto ``` lp15@64394 ` 241` ``` then show False ``` lp15@64394 ` 242` ``` proof cases ``` lp15@64394 ` 243` ``` case 1 ``` lp15@64394 ` 244` ``` then have w: "w \ rel_interior S" ``` lp15@64394 ` 245` ``` using \w \ S\ closure_subset rel_frontier_def by fastforce ``` lp15@64394 ` 246` ``` have "w + (w - z) \ affine hull S" ``` lp15@64394 ` 247` ``` by (metis \w \ S\ \z \ S\ affine_affine_hull hull_inc mem_affine_3_minus scaleR_one) ``` lp15@64394 ` 248` ``` then obtain e where "0 < e" "(w + e *\<^sub>R (w - z)) \ rel_frontier S" ``` lp15@64394 ` 249` ``` using \w \ z\ \z \ S\ by (metis assms ray_to_rel_frontier right_minus_eq w) ``` lp15@64394 ` 250` ``` moreover obtain d where "0 < d" "(w + d *\<^sub>R (z - w)) \ rel_frontier S" ``` lp15@64394 ` 251` ``` using ray_to_rel_frontier [OF \bounded S\ w, of "1 *\<^sub>R (z - w)"] \w \ z\ \z \ S\ ``` lp15@64394 ` 252` ``` by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one) ``` lp15@64394 ` 253` ``` ultimately have "d *\<^sub>R (z - w) = e *\<^sub>R (w - z)" ``` lp15@64394 ` 254` ``` using \rel_frontier S = {a}\ by force ``` lp15@64394 ` 255` ``` moreover have "e \ -d " ``` lp15@64394 ` 256` ``` using \0 < e\ \0 < d\ by force ``` lp15@64394 ` 257` ``` ultimately show False ``` lp15@64394 ` 258` ``` by (metis (no_types, lifting) \w \ z\ eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus) ``` lp15@64394 ` 259` ``` next ``` lp15@64394 ` 260` ``` case 2 ``` lp15@64394 ` 261` ``` then have z: "z \ rel_interior S" ``` lp15@64394 ` 262` ``` using \z \ S\ closure_subset rel_frontier_def by fastforce ``` lp15@64394 ` 263` ``` have "z + (z - w) \ affine hull S" ``` lp15@64394 ` 264` ``` by (metis \z \ S\ \w \ S\ affine_affine_hull hull_inc mem_affine_3_minus scaleR_one) ``` lp15@64394 ` 265` ``` then obtain e where "0 < e" "(z + e *\<^sub>R (z - w)) \ rel_frontier S" ``` lp15@64394 ` 266` ``` using \w \ z\ \w \ S\ by (metis assms ray_to_rel_frontier right_minus_eq z) ``` lp15@64394 ` 267` ``` moreover obtain d where "0 < d" "(z + d *\<^sub>R (w - z)) \ rel_frontier S" ``` lp15@64394 ` 268` ``` using ray_to_rel_frontier [OF \bounded S\ z, of "1 *\<^sub>R (w - z)"] \w \ z\ \w \ S\ ``` lp15@64394 ` 269` ``` by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one) ``` lp15@64394 ` 270` ``` ultimately have "d *\<^sub>R (w - z) = e *\<^sub>R (z - w)" ``` lp15@64394 ` 271` ``` using \rel_frontier S = {a}\ by force ``` lp15@64394 ` 272` ``` moreover have "e \ -d " ``` lp15@64394 ` 273` ``` using \0 < e\ \0 < d\ by force ``` lp15@64394 ` 274` ``` ultimately show False ``` lp15@64394 ` 275` ``` by (metis (no_types, lifting) \w \ z\ eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus) ``` lp15@64394 ` 276` ``` qed ``` lp15@64394 ` 277` ``` qed ``` lp15@64394 ` 278` ``` qed ``` lp15@64394 ` 279` ```qed ``` lp15@64394 ` 280` lp15@63130 ` 281` ```proposition ``` lp15@63130 ` 282` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63130 ` 283` ``` assumes "compact S" and 0: "0 \ rel_interior S" ``` lp15@63130 ` 284` ``` and star: "\x. x \ S \ open_segment 0 x \ rel_interior S" ``` lp15@63130 ` 285` ``` shows starlike_compact_projective1_0: ``` lp15@63130 ` 286` ``` "S - rel_interior S homeomorphic sphere 0 1 \ affine hull S" ``` lp15@63130 ` 287` ``` (is "?SMINUS homeomorphic ?SPHER") ``` lp15@63130 ` 288` ``` and starlike_compact_projective2_0: ``` lp15@63130 ` 289` ``` "S homeomorphic cball 0 1 \ affine hull S" ``` lp15@63130 ` 290` ``` (is "S homeomorphic ?CBALL") ``` lp15@63130 ` 291` ```proof - ``` lp15@63130 ` 292` ``` have starI: "(u *\<^sub>R x) \ rel_interior S" if "x \ S" "0 \ u" "u < 1" for x u ``` lp15@63130 ` 293` ``` proof (cases "x=0 \ u=0") ``` lp15@63130 ` 294` ``` case True with 0 show ?thesis by force ``` lp15@63130 ` 295` ``` next ``` lp15@63130 ` 296` ``` case False with that show ?thesis ``` lp15@63130 ` 297` ``` by (auto simp: in_segment intro: star [THEN subsetD]) ``` lp15@63130 ` 298` ``` qed ``` lp15@63130 ` 299` ``` have "0 \ S" using assms rel_interior_subset by auto ``` lp15@63130 ` 300` ``` define proj where "proj \ \x::'a. x /\<^sub>R norm x" ``` lp15@63130 ` 301` ``` have eqI: "x = y" if "proj x = proj y" "norm x = norm y" for x y ``` lp15@63130 ` 302` ``` using that by (force simp: proj_def) ``` lp15@63130 ` 303` ``` then have iff_eq: "\x y. (proj x = proj y \ norm x = norm y) \ x = y" ``` lp15@63130 ` 304` ``` by blast ``` lp15@63130 ` 305` ``` have projI: "x \ affine hull S \ proj x \ affine hull S" for x ``` lp15@63130 ` 306` ``` by (metis \0 \ S\ affine_hull_span_0 hull_inc span_mul proj_def) ``` lp15@63130 ` 307` ``` have nproj1 [simp]: "x \ 0 \ norm(proj x) = 1" for x ``` lp15@63130 ` 308` ``` by (simp add: proj_def) ``` lp15@63130 ` 309` ``` have proj0_iff [simp]: "proj x = 0 \ x = 0" for x ``` lp15@63130 ` 310` ``` by (simp add: proj_def) ``` lp15@63130 ` 311` ``` have cont_proj: "continuous_on (UNIV - {0}) proj" ``` lp15@63130 ` 312` ``` unfolding proj_def by (rule continuous_intros | force)+ ``` lp15@63130 ` 313` ``` have proj_spherI: "\x. \x \ affine hull S; x \ 0\ \ proj x \ ?SPHER" ``` lp15@63130 ` 314` ``` by (simp add: projI) ``` lp15@63130 ` 315` ``` have "bounded S" "closed S" ``` lp15@63130 ` 316` ``` using \compact S\ compact_eq_bounded_closed by blast+ ``` lp15@63130 ` 317` ``` have inj_on_proj: "inj_on proj (S - rel_interior S)" ``` lp15@63130 ` 318` ``` proof ``` lp15@63130 ` 319` ``` fix x y ``` lp15@63130 ` 320` ``` assume x: "x \ S - rel_interior S" ``` lp15@63130 ` 321` ``` and y: "y \ S - rel_interior S" and eq: "proj x = proj y" ``` lp15@63130 ` 322` ``` then have xynot: "x \ 0" "y \ 0" "x \ S" "y \ S" "x \ rel_interior S" "y \ rel_interior S" ``` lp15@63130 ` 323` ``` using 0 by auto ``` lp15@63130 ` 324` ``` consider "norm x = norm y" | "norm x < norm y" | "norm x > norm y" by linarith ``` lp15@63130 ` 325` ``` then show "x = y" ``` lp15@63130 ` 326` ``` proof cases ``` lp15@63130 ` 327` ``` assume "norm x = norm y" ``` lp15@63130 ` 328` ``` with iff_eq eq show "x = y" by blast ``` lp15@63130 ` 329` ``` next ``` lp15@63130 ` 330` ``` assume *: "norm x < norm y" ``` lp15@63130 ` 331` ``` have "x /\<^sub>R norm x = norm x *\<^sub>R (x /\<^sub>R norm x) /\<^sub>R norm (norm x *\<^sub>R (x /\<^sub>R norm x))" ``` lp15@63130 ` 332` ``` by force ``` lp15@63130 ` 333` ``` then have "proj ((norm x / norm y) *\<^sub>R y) = proj x" ``` lp15@63130 ` 334` ``` by (metis (no_types) divide_inverse local.proj_def eq scaleR_scaleR) ``` lp15@63130 ` 335` ``` then have [simp]: "(norm x / norm y) *\<^sub>R y = x" ``` lp15@63130 ` 336` ``` by (rule eqI) (simp add: \y \ 0\) ``` lp15@63130 ` 337` ``` have no: "0 \ norm x / norm y" "norm x / norm y < 1" ``` lp15@63130 ` 338` ``` using * by (auto simp: divide_simps) ``` lp15@63130 ` 339` ``` then show "x = y" ``` lp15@63130 ` 340` ``` using starI [OF \y \ S\ no] xynot by auto ``` lp15@63130 ` 341` ``` next ``` lp15@63130 ` 342` ``` assume *: "norm x > norm y" ``` lp15@63130 ` 343` ``` have "y /\<^sub>R norm y = norm y *\<^sub>R (y /\<^sub>R norm y) /\<^sub>R norm (norm y *\<^sub>R (y /\<^sub>R norm y))" ``` lp15@63130 ` 344` ``` by force ``` lp15@63130 ` 345` ``` then have "proj ((norm y / norm x) *\<^sub>R x) = proj y" ``` lp15@63130 ` 346` ``` by (metis (no_types) divide_inverse local.proj_def eq scaleR_scaleR) ``` lp15@63130 ` 347` ``` then have [simp]: "(norm y / norm x) *\<^sub>R x = y" ``` lp15@63130 ` 348` ``` by (rule eqI) (simp add: \x \ 0\) ``` lp15@63130 ` 349` ``` have no: "0 \ norm y / norm x" "norm y / norm x < 1" ``` lp15@63130 ` 350` ``` using * by (auto simp: divide_simps) ``` lp15@63130 ` 351` ``` then show "x = y" ``` lp15@63130 ` 352` ``` using starI [OF \x \ S\ no] xynot by auto ``` lp15@63130 ` 353` ``` qed ``` lp15@63130 ` 354` ``` qed ``` lp15@63130 ` 355` ``` have "\surf. homeomorphism (S - rel_interior S) ?SPHER proj surf" ``` lp15@63130 ` 356` ``` proof (rule homeomorphism_compact) ``` lp15@63130 ` 357` ``` show "compact (S - rel_interior S)" ``` lp15@63130 ` 358` ``` using \compact S\ compact_rel_boundary by blast ``` lp15@63130 ` 359` ``` show "continuous_on (S - rel_interior S) proj" ``` lp15@63130 ` 360` ``` using 0 by (blast intro: continuous_on_subset [OF cont_proj]) ``` lp15@63130 ` 361` ``` show "proj ` (S - rel_interior S) = ?SPHER" ``` lp15@63130 ` 362` ``` proof ``` lp15@63130 ` 363` ``` show "proj ` (S - rel_interior S) \ ?SPHER" ``` lp15@63130 ` 364` ``` using 0 by (force simp: hull_inc projI intro: nproj1) ``` lp15@63130 ` 365` ``` show "?SPHER \ proj ` (S - rel_interior S)" ``` lp15@63130 ` 366` ``` proof (clarsimp simp: proj_def) ``` lp15@63130 ` 367` ``` fix x ``` lp15@63130 ` 368` ``` assume "x \ affine hull S" and nox: "norm x = 1" ``` lp15@63130 ` 369` ``` then have "x \ 0" by auto ``` lp15@63130 ` 370` ``` obtain d where "0 < d" and dx: "(d *\<^sub>R x) \ rel_frontier S" ``` lp15@63130 ` 371` ``` and ri: "\e. \0 \ e; e < d\ \ (e *\<^sub>R x) \ rel_interior S" ``` lp15@63130 ` 372` ``` using ray_to_rel_frontier [OF \bounded S\ 0] \x \ affine hull S\ \x \ 0\ by auto ``` lp15@63130 ` 373` ``` show "x \ (\x. x /\<^sub>R norm x) ` (S - rel_interior S)" ``` lp15@63130 ` 374` ``` apply (rule_tac x="d *\<^sub>R x" in image_eqI) ``` lp15@63130 ` 375` ``` using \0 < d\ ``` lp15@63130 ` 376` ``` using dx \closed S\ apply (auto simp: rel_frontier_def divide_simps nox) ``` lp15@63130 ` 377` ``` done ``` lp15@63130 ` 378` ``` qed ``` lp15@63130 ` 379` ``` qed ``` lp15@63130 ` 380` ``` qed (rule inj_on_proj) ``` lp15@63130 ` 381` ``` then obtain surf where surf: "homeomorphism (S - rel_interior S) ?SPHER proj surf" ``` lp15@63130 ` 382` ``` by blast ``` lp15@63130 ` 383` ``` then have cont_surf: "continuous_on (proj ` (S - rel_interior S)) surf" ``` lp15@63130 ` 384` ``` by (auto simp: homeomorphism_def) ``` lp15@63130 ` 385` ``` have surf_nz: "\x. x \ ?SPHER \ surf x \ 0" ``` lp15@63130 ` 386` ``` by (metis "0" DiffE homeomorphism_def imageI surf) ``` lp15@63130 ` 387` ``` have cont_nosp: "continuous_on (?SPHER) (\x. norm x *\<^sub>R ((surf o proj) x))" ``` lp15@63130 ` 388` ``` apply (rule continuous_intros)+ ``` lp15@63130 ` 389` ``` apply (rule continuous_on_subset [OF cont_proj], force) ``` lp15@63130 ` 390` ``` apply (rule continuous_on_subset [OF cont_surf]) ``` lp15@63130 ` 391` ``` apply (force simp: homeomorphism_image1 [OF surf] dest: proj_spherI) ``` lp15@63130 ` 392` ``` done ``` lp15@63130 ` 393` ``` have surfpS: "\x. \norm x = 1; x \ affine hull S\ \ surf (proj x) \ S" ``` lp15@63130 ` 394` ``` by (metis (full_types) DiffE \0 \ S\ homeomorphism_def image_eqI norm_zero proj_spherI real_vector.scale_zero_left scaleR_one surf) ``` lp15@63130 ` 395` ``` have *: "\y. norm y = 1 \ y \ affine hull S \ x = surf (proj y)" ``` lp15@63130 ` 396` ``` if "x \ S" "x \ rel_interior S" for x ``` lp15@63130 ` 397` ``` proof - ``` lp15@63130 ` 398` ``` have "proj x \ ?SPHER" ``` lp15@63130 ` 399` ``` by (metis (full_types) "0" hull_inc proj_spherI that) ``` lp15@63130 ` 400` ``` moreover have "surf (proj x) = x" ``` lp15@63130 ` 401` ``` by (metis Diff_iff homeomorphism_def surf that) ``` lp15@63130 ` 402` ``` ultimately show ?thesis ``` lp15@63130 ` 403` ``` by (metis \\x. x \ ?SPHER \ surf x \ 0\ hull_inc inverse_1 local.proj_def norm_sgn projI scaleR_one sgn_div_norm that(1)) ``` lp15@63130 ` 404` ``` qed ``` lp15@63130 ` 405` ``` have surfp_notin: "\x. \norm x = 1; x \ affine hull S\ \ surf (proj x) \ rel_interior S" ``` lp15@63130 ` 406` ``` by (metis (full_types) DiffE one_neq_zero homeomorphism_def image_eqI norm_zero proj_spherI surf) ``` lp15@63130 ` 407` ``` have no_sp_im: "(\x. norm x *\<^sub>R surf (proj x)) ` (?SPHER) = S - rel_interior S" ``` lp15@63130 ` 408` ``` by (auto simp: surfpS image_def Bex_def surfp_notin *) ``` lp15@63130 ` 409` ``` have inj_spher: "inj_on (\x. norm x *\<^sub>R surf (proj x)) ?SPHER" ``` lp15@63130 ` 410` ``` proof ``` lp15@63130 ` 411` ``` fix x y ``` lp15@63130 ` 412` ``` assume xy: "x \ ?SPHER" "y \ ?SPHER" ``` lp15@63130 ` 413` ``` and eq: " norm x *\<^sub>R surf (proj x) = norm y *\<^sub>R surf (proj y)" ``` lp15@63130 ` 414` ``` then have "norm x = 1" "norm y = 1" "x \ affine hull S" "y \ affine hull S" ``` lp15@63130 ` 415` ``` using 0 by auto ``` lp15@63130 ` 416` ``` with eq show "x = y" ``` lp15@63130 ` 417` ``` by (simp add: proj_def) (metis surf xy homeomorphism_def) ``` lp15@63130 ` 418` ``` qed ``` lp15@63130 ` 419` ``` have co01: "compact ?SPHER" ``` lp15@63130 ` 420` ``` by (simp add: closed_affine_hull compact_Int_closed) ``` lp15@63130 ` 421` ``` show "?SMINUS homeomorphic ?SPHER" ``` lp15@63130 ` 422` ``` apply (subst homeomorphic_sym) ``` lp15@63130 ` 423` ``` apply (rule homeomorphic_compact [OF co01 cont_nosp [unfolded o_def] no_sp_im inj_spher]) ``` lp15@63130 ` 424` ``` done ``` lp15@63130 ` 425` ``` have proj_scaleR: "\a x. 0 < a \ proj (a *\<^sub>R x) = proj x" ``` lp15@63130 ` 426` ``` by (simp add: proj_def) ``` lp15@63130 ` 427` ``` have cont_sp0: "continuous_on (affine hull S - {0}) (surf o proj)" ``` lp15@63130 ` 428` ``` apply (rule continuous_on_compose [OF continuous_on_subset [OF cont_proj]], force) ``` lp15@63130 ` 429` ``` apply (rule continuous_on_subset [OF cont_surf]) ``` lp15@63130 ` 430` ``` using homeomorphism_image1 proj_spherI surf by fastforce ``` lp15@63130 ` 431` ``` obtain B where "B>0" and B: "\x. x \ S \ norm x \ B" ``` lp15@63130 ` 432` ``` by (metis compact_imp_bounded \compact S\ bounded_pos_less less_eq_real_def) ``` lp15@63130 ` 433` ``` have cont_nosp: "continuous (at x within ?CBALL) (\x. norm x *\<^sub>R surf (proj x))" ``` lp15@63130 ` 434` ``` if "norm x \ 1" "x \ affine hull S" for x ``` lp15@63130 ` 435` ``` proof (cases "x=0") ``` lp15@63130 ` 436` ``` case True ``` lp15@63130 ` 437` ``` show ?thesis using True ``` lp15@63130 ` 438` ``` apply (simp add: continuous_within) ``` lp15@63130 ` 439` ``` apply (rule lim_null_scaleR_bounded [where B=B]) ``` lp15@63130 ` 440` ``` apply (simp_all add: tendsto_norm_zero eventually_at) ``` lp15@63130 ` 441` ``` apply (rule_tac x=B in exI) ``` lp15@63130 ` 442` ``` using B surfpS proj_def projI apply (auto simp: \B > 0\) ``` lp15@63130 ` 443` ``` done ``` lp15@63130 ` 444` ``` next ``` lp15@63130 ` 445` ``` case False ``` lp15@63130 ` 446` ``` then have "\\<^sub>F x in at x. (x \ affine hull S - {0}) = (x \ affine hull S)" ``` lp15@63130 ` 447` ``` apply (simp add: eventually_at) ``` lp15@63130 ` 448` ``` apply (rule_tac x="norm x" in exI) ``` lp15@63130 ` 449` ``` apply (auto simp: False) ``` lp15@63130 ` 450` ``` done ``` lp15@63130 ` 451` ``` with cont_sp0 have *: "continuous (at x within affine hull S) (\x. surf (proj x))" ``` lp15@63130 ` 452` ``` apply (simp add: continuous_on_eq_continuous_within) ``` lp15@63130 ` 453` ``` apply (drule_tac x=x in bspec, force simp: False that) ``` lp15@63130 ` 454` ``` apply (simp add: continuous_within Lim_transform_within_set) ``` lp15@63130 ` 455` ``` done ``` lp15@63130 ` 456` ``` show ?thesis ``` lp15@63130 ` 457` ``` apply (rule continuous_within_subset [where s = "affine hull S", OF _ Int_lower2]) ``` lp15@63130 ` 458` ``` apply (rule continuous_intros *)+ ``` lp15@63130 ` 459` ``` done ``` lp15@63130 ` 460` ``` qed ``` lp15@63130 ` 461` ``` have cont_nosp2: "continuous_on ?CBALL (\x. norm x *\<^sub>R ((surf o proj) x))" ``` lp15@63130 ` 462` ``` by (simp add: continuous_on_eq_continuous_within cont_nosp) ``` lp15@63130 ` 463` ``` have "norm y *\<^sub>R surf (proj y) \ S" if "y \ cball 0 1" and yaff: "y \ affine hull S" for y ``` lp15@63130 ` 464` ``` proof (cases "y=0") ``` lp15@63130 ` 465` ``` case True then show ?thesis ``` lp15@63130 ` 466` ``` by (simp add: \0 \ S\) ``` lp15@63130 ` 467` ``` next ``` lp15@63130 ` 468` ``` case False ``` lp15@63130 ` 469` ``` then have "norm y *\<^sub>R surf (proj y) = norm y *\<^sub>R surf (proj (y /\<^sub>R norm y))" ``` lp15@63130 ` 470` ``` by (simp add: proj_def) ``` lp15@63130 ` 471` ``` have "norm y \ 1" using that by simp ``` lp15@63130 ` 472` ``` have "surf (proj (y /\<^sub>R norm y)) \ S" ``` lp15@63130 ` 473` ``` apply (rule surfpS) ``` lp15@63130 ` 474` ``` using proj_def projI yaff ``` lp15@63130 ` 475` ``` by (auto simp: False) ``` lp15@63130 ` 476` ``` then have "surf (proj y) \ S" ``` lp15@63130 ` 477` ``` by (simp add: False proj_def) ``` lp15@63130 ` 478` ``` then show "norm y *\<^sub>R surf (proj y) \ S" ``` lp15@63130 ` 479` ``` by (metis dual_order.antisym le_less_linear norm_ge_zero rel_interior_subset scaleR_one ``` lp15@63130 ` 480` ``` starI subset_eq \norm y \ 1\) ``` lp15@63130 ` 481` ``` qed ``` lp15@63130 ` 482` ``` moreover have "x \ (\x. norm x *\<^sub>R surf (proj x)) ` (?CBALL)" if "x \ S" for x ``` lp15@63130 ` 483` ``` proof (cases "x=0") ``` lp15@63130 ` 484` ``` case True with that hull_inc show ?thesis by fastforce ``` lp15@63130 ` 485` ``` next ``` lp15@63130 ` 486` ``` case False ``` lp15@63130 ` 487` ``` then have psp: "proj (surf (proj x)) = proj x" ``` lp15@63130 ` 488` ``` by (metis homeomorphism_def hull_inc proj_spherI surf that) ``` lp15@63130 ` 489` ``` have nxx: "norm x *\<^sub>R proj x = x" ``` lp15@63130 ` 490` ``` by (simp add: False local.proj_def) ``` lp15@63130 ` 491` ``` have affineI: "(1 / norm (surf (proj x))) *\<^sub>R x \ affine hull S" ``` lp15@63130 ` 492` ``` by (metis \0 \ S\ affine_hull_span_0 hull_inc span_clauses(4) that) ``` lp15@63130 ` 493` ``` have sproj_nz: "surf (proj x) \ 0" ``` lp15@63130 ` 494` ``` by (metis False proj0_iff psp) ``` lp15@63130 ` 495` ``` then have "proj x = proj (proj x)" ``` lp15@63130 ` 496` ``` by (metis False nxx proj_scaleR zero_less_norm_iff) ``` lp15@63130 ` 497` ``` moreover have scaleproj: "\a r. r *\<^sub>R proj a = (r / norm a) *\<^sub>R a" ``` lp15@63130 ` 498` ``` by (simp add: divide_inverse local.proj_def) ``` lp15@63130 ` 499` ``` ultimately have "(norm (surf (proj x)) / norm x) *\<^sub>R x \ rel_interior S" ``` lp15@63130 ` 500` ``` by (metis (no_types) sproj_nz divide_self_if hull_inc norm_eq_zero nproj1 projI psp scaleR_one surfp_notin that) ``` lp15@63130 ` 501` ``` then have "(norm (surf (proj x)) / norm x) \ 1" ``` lp15@63130 ` 502` ``` using starI [OF that] by (meson starI [OF that] le_less_linear norm_ge_zero zero_le_divide_iff) ``` lp15@63130 ` 503` ``` then have nole: "norm x \ norm (surf (proj x))" ``` lp15@63130 ` 504` ``` by (simp add: le_divide_eq_1) ``` lp15@63130 ` 505` ``` show ?thesis ``` lp15@63130 ` 506` ``` apply (rule_tac x="inverse(norm(surf (proj x))) *\<^sub>R x" in image_eqI) ``` lp15@63130 ` 507` ``` apply (metis (no_types, hide_lams) mult.commute scaleproj abs_inverse abs_norm_cancel divide_inverse norm_scaleR nxx positive_imp_inverse_positive proj_scaleR psp sproj_nz zero_less_norm_iff) ``` lp15@63130 ` 508` ``` apply (auto simp: divide_simps nole affineI) ``` lp15@63130 ` 509` ``` done ``` lp15@63130 ` 510` ``` qed ``` lp15@63130 ` 511` ``` ultimately have im_cball: "(\x. norm x *\<^sub>R surf (proj x)) ` ?CBALL = S" ``` lp15@63130 ` 512` ``` by blast ``` lp15@63130 ` 513` ``` have inj_cball: "inj_on (\x. norm x *\<^sub>R surf (proj x)) ?CBALL" ``` lp15@63130 ` 514` ``` proof ``` lp15@63130 ` 515` ``` fix x y ``` lp15@63130 ` 516` ``` assume "x \ ?CBALL" "y \ ?CBALL" ``` lp15@63130 ` 517` ``` and eq: "norm x *\<^sub>R surf (proj x) = norm y *\<^sub>R surf (proj y)" ``` lp15@63130 ` 518` ``` then have x: "x \ affine hull S" and y: "y \ affine hull S" ``` lp15@63130 ` 519` ``` using 0 by auto ``` lp15@63130 ` 520` ``` show "x = y" ``` lp15@63130 ` 521` ``` proof (cases "x=0 \ y=0") ``` lp15@63130 ` 522` ``` case True then show "x = y" using eq proj_spherI surf_nz x y by force ``` lp15@63130 ` 523` ``` next ``` lp15@63130 ` 524` ``` case False ``` lp15@63130 ` 525` ``` with x y have speq: "surf (proj x) = surf (proj y)" ``` lp15@63130 ` 526` ``` by (metis eq homeomorphism_apply2 proj_scaleR proj_spherI surf zero_less_norm_iff) ``` lp15@63130 ` 527` ``` then have "norm x = norm y" ``` lp15@63130 ` 528` ``` by (metis \x \ affine hull S\ \y \ affine hull S\ eq proj_spherI real_vector.scale_cancel_right surf_nz) ``` lp15@63130 ` 529` ``` moreover have "proj x = proj y" ``` lp15@63130 ` 530` ``` by (metis (no_types) False speq homeomorphism_apply2 proj_spherI surf x y) ``` lp15@63130 ` 531` ``` ultimately show "x = y" ``` lp15@63130 ` 532` ``` using eq eqI by blast ``` lp15@63130 ` 533` ``` qed ``` lp15@63130 ` 534` ``` qed ``` lp15@63130 ` 535` ``` have co01: "compact ?CBALL" ``` lp15@63130 ` 536` ``` by (simp add: closed_affine_hull compact_Int_closed) ``` lp15@63130 ` 537` ``` show "S homeomorphic ?CBALL" ``` lp15@63130 ` 538` ``` apply (subst homeomorphic_sym) ``` lp15@63130 ` 539` ``` apply (rule homeomorphic_compact [OF co01 cont_nosp2 [unfolded o_def] im_cball inj_cball]) ``` lp15@63130 ` 540` ``` done ``` lp15@63130 ` 541` ```qed ``` lp15@63130 ` 542` lp15@63130 ` 543` ```corollary ``` lp15@63130 ` 544` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63130 ` 545` ``` assumes "compact S" and a: "a \ rel_interior S" ``` lp15@63130 ` 546` ``` and star: "\x. x \ S \ open_segment a x \ rel_interior S" ``` lp15@63130 ` 547` ``` shows starlike_compact_projective1: ``` lp15@63130 ` 548` ``` "S - rel_interior S homeomorphic sphere a 1 \ affine hull S" ``` lp15@63130 ` 549` ``` and starlike_compact_projective2: ``` lp15@63130 ` 550` ``` "S homeomorphic cball a 1 \ affine hull S" ``` lp15@63130 ` 551` ```proof - ``` nipkow@67399 ` 552` ``` have 1: "compact ((+) (-a) ` S)" by (meson assms compact_translation) ``` nipkow@67399 ` 553` ``` have 2: "0 \ rel_interior ((+) (-a) ` S)" ``` lp15@63130 ` 554` ``` by (simp add: a rel_interior_translation) ``` nipkow@67399 ` 555` ``` have 3: "open_segment 0 x \ rel_interior ((+) (-a) ` S)" if "x \ ((+) (-a) ` S)" for x ``` lp15@63130 ` 556` ``` proof - ``` lp15@63130 ` 557` ``` have "x+a \ S" using that by auto ``` lp15@63130 ` 558` ``` then have "open_segment a (x+a) \ rel_interior S" by (metis star) ``` lp15@63130 ` 559` ``` then show ?thesis using open_segment_translation ``` lp15@63130 ` 560` ``` using rel_interior_translation by fastforce ``` lp15@63130 ` 561` ``` qed ``` nipkow@67399 ` 562` ``` have "S - rel_interior S homeomorphic ((+) (-a) ` S) - rel_interior ((+) (-a) ` S)" ``` lp15@63130 ` 563` ``` by (metis rel_interior_translation translation_diff homeomorphic_translation) ``` nipkow@67399 ` 564` ``` also have "... homeomorphic sphere 0 1 \ affine hull ((+) (-a) ` S)" ``` lp15@63130 ` 565` ``` by (rule starlike_compact_projective1_0 [OF 1 2 3]) ``` nipkow@67399 ` 566` ``` also have "... = (+) (-a) ` (sphere a 1 \ affine hull S)" ``` lp15@63130 ` 567` ``` by (metis affine_hull_translation left_minus sphere_translation translation_Int) ``` lp15@63130 ` 568` ``` also have "... homeomorphic sphere a 1 \ affine hull S" ``` lp15@63130 ` 569` ``` using homeomorphic_translation homeomorphic_sym by blast ``` lp15@63130 ` 570` ``` finally show "S - rel_interior S homeomorphic sphere a 1 \ affine hull S" . ``` lp15@63130 ` 571` nipkow@67399 ` 572` ``` have "S homeomorphic ((+) (-a) ` S)" ``` lp15@63130 ` 573` ``` by (metis homeomorphic_translation) ``` nipkow@67399 ` 574` ``` also have "... homeomorphic cball 0 1 \ affine hull ((+) (-a) ` S)" ``` lp15@63130 ` 575` ``` by (rule starlike_compact_projective2_0 [OF 1 2 3]) ``` nipkow@67399 ` 576` ``` also have "... = (+) (-a) ` (cball a 1 \ affine hull S)" ``` lp15@63130 ` 577` ``` by (metis affine_hull_translation left_minus cball_translation translation_Int) ``` lp15@63130 ` 578` ``` also have "... homeomorphic cball a 1 \ affine hull S" ``` lp15@63130 ` 579` ``` using homeomorphic_translation homeomorphic_sym by blast ``` lp15@63130 ` 580` ``` finally show "S homeomorphic cball a 1 \ affine hull S" . ``` lp15@63130 ` 581` ```qed ``` lp15@63130 ` 582` lp15@63130 ` 583` ```corollary starlike_compact_projective_special: ``` lp15@63130 ` 584` ``` assumes "compact S" ``` lp15@63130 ` 585` ``` and cb01: "cball (0::'a::euclidean_space) 1 \ S" ``` lp15@63130 ` 586` ``` and scale: "\x u. \x \ S; 0 \ u; u < 1\ \ u *\<^sub>R x \ S - frontier S" ``` lp15@63130 ` 587` ``` shows "S homeomorphic (cball (0::'a::euclidean_space) 1)" ``` lp15@63130 ` 588` ```proof - ``` lp15@63130 ` 589` ``` have "ball 0 1 \ interior S" ``` lp15@63130 ` 590` ``` using cb01 interior_cball interior_mono by blast ``` lp15@63130 ` 591` ``` then have 0: "0 \ rel_interior S" ``` lp15@63130 ` 592` ``` by (meson centre_in_ball subsetD interior_subset_rel_interior le_numeral_extra(2) not_le) ``` lp15@63130 ` 593` ``` have [simp]: "affine hull S = UNIV" ``` lp15@63130 ` 594` ``` using \ball 0 1 \ interior S\ by (auto intro!: affine_hull_nonempty_interior) ``` lp15@63130 ` 595` ``` have star: "open_segment 0 x \ rel_interior S" if "x \ S" for x ``` hoelzl@63627 ` 596` ``` proof ``` lp15@63130 ` 597` ``` fix p assume "p \ open_segment 0 x" ``` lp15@63130 ` 598` ``` then obtain u where "x \ 0" and u: "0 \ u" "u < 1" and p: "u *\<^sub>R x = p" ``` hoelzl@63627 ` 599` ``` by (auto simp: in_segment) ``` lp15@63130 ` 600` ``` then show "p \ rel_interior S" ``` lp15@63130 ` 601` ``` using scale [OF that u] closure_subset frontier_def interior_subset_rel_interior by fastforce ``` lp15@63130 ` 602` ``` qed ``` lp15@63130 ` 603` ``` show ?thesis ``` lp15@63130 ` 604` ``` using starlike_compact_projective2_0 [OF \compact S\ 0 star] by simp ``` lp15@63130 ` 605` ```qed ``` lp15@63130 ` 606` lp15@63130 ` 607` ```lemma homeomorphic_convex_lemma: ``` lp15@63130 ` 608` ``` fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" ``` lp15@63130 ` 609` ``` assumes "convex S" "compact S" "convex T" "compact T" ``` lp15@63130 ` 610` ``` and affeq: "aff_dim S = aff_dim T" ``` lp15@63130 ` 611` ``` shows "(S - rel_interior S) homeomorphic (T - rel_interior T) \ ``` lp15@63130 ` 612` ``` S homeomorphic T" ``` lp15@63130 ` 613` ```proof (cases "rel_interior S = {} \ rel_interior T = {}") ``` lp15@63130 ` 614` ``` case True ``` lp15@63130 ` 615` ``` then show ?thesis ``` lp15@63130 ` 616` ``` by (metis Diff_empty affeq \convex S\ \convex T\ aff_dim_empty homeomorphic_empty rel_interior_eq_empty aff_dim_empty) ``` lp15@63130 ` 617` ```next ``` lp15@63130 ` 618` ``` case False ``` lp15@63130 ` 619` ``` then obtain a b where a: "a \ rel_interior S" and b: "b \ rel_interior T" by auto ``` lp15@63130 ` 620` ``` have starS: "\x. x \ S \ open_segment a x \ rel_interior S" ``` lp15@63130 ` 621` ``` using rel_interior_closure_convex_segment ``` lp15@63130 ` 622` ``` a \convex S\ closure_subset subsetCE by blast ``` lp15@63130 ` 623` ``` have starT: "\x. x \ T \ open_segment b x \ rel_interior T" ``` lp15@63130 ` 624` ``` using rel_interior_closure_convex_segment ``` lp15@63130 ` 625` ``` b \convex T\ closure_subset subsetCE by blast ``` nipkow@67399 ` 626` ``` let ?aS = "(+) (-a) ` S" and ?bT = "(+) (-b) ` T" ``` lp15@63130 ` 627` ``` have 0: "0 \ affine hull ?aS" "0 \ affine hull ?bT" ``` lp15@63130 ` 628` ``` by (metis a b subsetD hull_inc image_eqI left_minus rel_interior_subset)+ ``` lp15@63130 ` 629` ``` have subs: "subspace (span ?aS)" "subspace (span ?bT)" ``` lp15@63130 ` 630` ``` by (rule subspace_span)+ ``` lp15@63130 ` 631` ``` moreover ``` nipkow@67399 ` 632` ``` have "dim (span ((+) (- a) ` S)) = dim (span ((+) (- b) ` T))" ``` lp15@63130 ` 633` ``` by (metis 0 aff_dim_translation_eq aff_dim_zero affeq dim_span nat_int) ``` lp15@63130 ` 634` ``` ultimately obtain f g where "linear f" "linear g" ``` lp15@63130 ` 635` ``` and fim: "f ` span ?aS = span ?bT" ``` lp15@63130 ` 636` ``` and gim: "g ` span ?bT = span ?aS" ``` lp15@63130 ` 637` ``` and fno: "\x. x \ span ?aS \ norm(f x) = norm x" ``` lp15@63130 ` 638` ``` and gno: "\x. x \ span ?bT \ norm(g x) = norm x" ``` lp15@63130 ` 639` ``` and gf: "\x. x \ span ?aS \ g(f x) = x" ``` lp15@63130 ` 640` ``` and fg: "\x. x \ span ?bT \ f(g x) = x" ``` lp15@63130 ` 641` ``` by (rule isometries_subspaces) blast ``` lp15@63130 ` 642` ``` have [simp]: "continuous_on A f" for A ``` lp15@63130 ` 643` ``` using \linear f\ linear_conv_bounded_linear linear_continuous_on by blast ``` lp15@63130 ` 644` ``` have [simp]: "continuous_on B g" for B ``` lp15@63130 ` 645` ``` using \linear g\ linear_conv_bounded_linear linear_continuous_on by blast ``` lp15@63130 ` 646` ``` have eqspanS: "affine hull ?aS = span ?aS" ``` lp15@63130 ` 647` ``` by (metis a affine_hull_span_0 subsetD hull_inc image_eqI left_minus rel_interior_subset) ``` lp15@63130 ` 648` ``` have eqspanT: "affine hull ?bT = span ?bT" ``` lp15@63130 ` 649` ``` by (metis b affine_hull_span_0 subsetD hull_inc image_eqI left_minus rel_interior_subset) ``` lp15@63130 ` 650` ``` have "S homeomorphic cball a 1 \ affine hull S" ``` lp15@63130 ` 651` ``` by (rule starlike_compact_projective2 [OF \compact S\ a starS]) ``` nipkow@67399 ` 652` ``` also have "... homeomorphic (+) (-a) ` (cball a 1 \ affine hull S)" ``` lp15@63130 ` 653` ``` by (metis homeomorphic_translation) ``` nipkow@67399 ` 654` ``` also have "... = cball 0 1 \ (+) (-a) ` (affine hull S)" ``` lp15@63130 ` 655` ``` by (auto simp: dist_norm) ``` lp15@63130 ` 656` ``` also have "... = cball 0 1 \ span ?aS" ``` lp15@63130 ` 657` ``` using eqspanS affine_hull_translation by blast ``` lp15@63130 ` 658` ``` also have "... homeomorphic cball 0 1 \ span ?bT" ``` lp15@63130 ` 659` ``` proof (rule homeomorphicI [where f=f and g=g]) ``` lp15@63130 ` 660` ``` show fim1: "f ` (cball 0 1 \ span ?aS) = cball 0 1 \ span ?bT" ``` lp15@63130 ` 661` ``` apply (rule subset_antisym) ``` lp15@63130 ` 662` ``` using fim fno apply (force simp:, clarify) ``` lp15@63130 ` 663` ``` by (metis IntI fg gim gno image_eqI mem_cball_0) ``` lp15@63130 ` 664` ``` show "g ` (cball 0 1 \ span ?bT) = cball 0 1 \ span ?aS" ``` lp15@63130 ` 665` ``` apply (rule subset_antisym) ``` lp15@63130 ` 666` ``` using gim gno apply (force simp:, clarify) ``` lp15@63130 ` 667` ``` by (metis IntI fim1 gf image_eqI) ``` lp15@63130 ` 668` ``` qed (auto simp: fg gf) ``` nipkow@67399 ` 669` ``` also have "... = cball 0 1 \ (+) (-b) ` (affine hull T)" ``` lp15@63130 ` 670` ``` using eqspanT affine_hull_translation by blast ``` nipkow@67399 ` 671` ``` also have "... = (+) (-b) ` (cball b 1 \ affine hull T)" ``` lp15@63130 ` 672` ``` by (auto simp: dist_norm) ``` lp15@63130 ` 673` ``` also have "... homeomorphic (cball b 1 \ affine hull T)" ``` lp15@63130 ` 674` ``` by (metis homeomorphic_translation homeomorphic_sym) ``` lp15@63130 ` 675` ``` also have "... homeomorphic T" ``` lp15@63130 ` 676` ``` by (metis starlike_compact_projective2 [OF \compact T\ b starT] homeomorphic_sym) ``` lp15@63130 ` 677` ``` finally have 1: "S homeomorphic T" . ``` lp15@63130 ` 678` lp15@63130 ` 679` ``` have "S - rel_interior S homeomorphic sphere a 1 \ affine hull S" ``` lp15@63130 ` 680` ``` by (rule starlike_compact_projective1 [OF \compact S\ a starS]) ``` nipkow@67399 ` 681` ``` also have "... homeomorphic (+) (-a) ` (sphere a 1 \ affine hull S)" ``` lp15@63130 ` 682` ``` by (metis homeomorphic_translation) ``` nipkow@67399 ` 683` ``` also have "... = sphere 0 1 \ (+) (-a) ` (affine hull S)" ``` lp15@63130 ` 684` ``` by (auto simp: dist_norm) ``` lp15@63130 ` 685` ``` also have "... = sphere 0 1 \ span ?aS" ``` lp15@63130 ` 686` ``` using eqspanS affine_hull_translation by blast ``` lp15@63130 ` 687` ``` also have "... homeomorphic sphere 0 1 \ span ?bT" ``` lp15@63130 ` 688` ``` proof (rule homeomorphicI [where f=f and g=g]) ``` lp15@63130 ` 689` ``` show fim1: "f ` (sphere 0 1 \ span ?aS) = sphere 0 1 \ span ?bT" ``` lp15@63130 ` 690` ``` apply (rule subset_antisym) ``` lp15@63130 ` 691` ``` using fim fno apply (force simp:, clarify) ``` lp15@63130 ` 692` ``` by (metis IntI fg gim gno image_eqI mem_sphere_0) ``` lp15@63130 ` 693` ``` show "g ` (sphere 0 1 \ span ?bT) = sphere 0 1 \ span ?aS" ``` lp15@63130 ` 694` ``` apply (rule subset_antisym) ``` lp15@63130 ` 695` ``` using gim gno apply (force simp:, clarify) ``` lp15@63130 ` 696` ``` by (metis IntI fim1 gf image_eqI) ``` lp15@63130 ` 697` ``` qed (auto simp: fg gf) ``` nipkow@67399 ` 698` ``` also have "... = sphere 0 1 \ (+) (-b) ` (affine hull T)" ``` lp15@63130 ` 699` ``` using eqspanT affine_hull_translation by blast ``` nipkow@67399 ` 700` ``` also have "... = (+) (-b) ` (sphere b 1 \ affine hull T)" ``` lp15@63130 ` 701` ``` by (auto simp: dist_norm) ``` lp15@63130 ` 702` ``` also have "... homeomorphic (sphere b 1 \ affine hull T)" ``` lp15@63130 ` 703` ``` by (metis homeomorphic_translation homeomorphic_sym) ``` lp15@63130 ` 704` ``` also have "... homeomorphic T - rel_interior T" ``` lp15@63130 ` 705` ``` by (metis starlike_compact_projective1 [OF \compact T\ b starT] homeomorphic_sym) ``` lp15@63130 ` 706` ``` finally have 2: "S - rel_interior S homeomorphic T - rel_interior T" . ``` lp15@63130 ` 707` ``` show ?thesis ``` lp15@63130 ` 708` ``` using 1 2 by blast ``` lp15@63130 ` 709` ```qed ``` lp15@63130 ` 710` lp15@63130 ` 711` ```lemma homeomorphic_convex_compact_sets: ``` lp15@63130 ` 712` ``` fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" ``` lp15@63130 ` 713` ``` assumes "convex S" "compact S" "convex T" "compact T" ``` lp15@63130 ` 714` ``` and affeq: "aff_dim S = aff_dim T" ``` lp15@63130 ` 715` ``` shows "S homeomorphic T" ``` lp15@63130 ` 716` ```using homeomorphic_convex_lemma [OF assms] assms ``` lp15@63130 ` 717` ```by (auto simp: rel_frontier_def) ``` lp15@63130 ` 718` lp15@63130 ` 719` ```lemma homeomorphic_rel_frontiers_convex_bounded_sets: ``` lp15@63130 ` 720` ``` fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" ``` lp15@63130 ` 721` ``` assumes "convex S" "bounded S" "convex T" "bounded T" ``` lp15@63130 ` 722` ``` and affeq: "aff_dim S = aff_dim T" ``` lp15@63130 ` 723` ``` shows "rel_frontier S homeomorphic rel_frontier T" ``` lp15@63130 ` 724` ```using assms homeomorphic_convex_lemma [of "closure S" "closure T"] ``` lp15@63130 ` 725` ```by (simp add: rel_frontier_def convex_rel_interior_closure) ``` lp15@63130 ` 726` lp15@63130 ` 727` lp15@63130 ` 728` ```subsection\Homeomorphisms between punctured spheres and affine sets\ ``` lp15@63130 ` 729` ```text\Including the famous stereoscopic projection of the 3-D sphere to the complex plane\ ``` lp15@63130 ` 730` lp15@63130 ` 731` ```text\The special case with centre 0 and radius 1\ ``` lp15@63130 ` 732` ```lemma homeomorphic_punctured_affine_sphere_affine_01: ``` lp15@63130 ` 733` ``` assumes "b \ sphere 0 1" "affine T" "0 \ T" "b \ T" "affine p" ``` lp15@63130 ` 734` ``` and affT: "aff_dim T = aff_dim p + 1" ``` lp15@63130 ` 735` ``` shows "(sphere 0 1 \ T) - {b} homeomorphic p" ``` lp15@63130 ` 736` ```proof - ``` lp15@63130 ` 737` ``` have [simp]: "norm b = 1" "b\b = 1" ``` lp15@63130 ` 738` ``` using assms by (auto simp: norm_eq_1) ``` lp15@63130 ` 739` ``` have [simp]: "T \ {v. b\v = 0} \ {}" ``` lp15@63130 ` 740` ``` using \0 \ T\ by auto ``` lp15@63130 ` 741` ``` have [simp]: "\ T \ {v. b\v = 0}" ``` lp15@63130 ` 742` ``` using \norm b = 1\ \b \ T\ by auto ``` lp15@63130 ` 743` ``` define f where "f \ \x. 2 *\<^sub>R b + (2 / (1 - b\x)) *\<^sub>R (x - b)" ``` lp15@63130 ` 744` ``` define g where "g \ \y. b + (4 / (norm y ^ 2 + 4)) *\<^sub>R (y - 2 *\<^sub>R b)" ``` lp15@63130 ` 745` ``` have [simp]: "\x. \x \ T; b\x = 0\ \ f (g x) = x" ``` lp15@63130 ` 746` ``` unfolding f_def g_def by (simp add: algebra_simps divide_simps add_nonneg_eq_0_iff) ``` lp15@63130 ` 747` ``` have no: "\x. \norm x = 1; b\x \ 1\ \ (norm (f x))\<^sup>2 = 4 * (1 + b\x) / (1 - b\x)" ``` lp15@63130 ` 748` ``` apply (simp add: dot_square_norm [symmetric]) ``` lp15@63130 ` 749` ``` apply (simp add: f_def vector_add_divide_simps divide_simps norm_eq_1) ``` lp15@63130 ` 750` ``` apply (simp add: algebra_simps inner_commute) ``` lp15@63130 ` 751` ``` done ``` lp15@63130 ` 752` ``` have [simp]: "\u::real. 8 + u * (u * 8) = u * 16 \ u=1" ``` lp15@63130 ` 753` ``` by algebra ``` lp15@63130 ` 754` ``` have [simp]: "\x. \norm x = 1; b \ x \ 1\ \ g (f x) = x" ``` lp15@63130 ` 755` ``` unfolding g_def no by (auto simp: f_def divide_simps) ``` lp15@63130 ` 756` ``` have [simp]: "\x. \x \ T; b \ x = 0\ \ norm (g x) = 1" ``` lp15@63130 ` 757` ``` unfolding g_def ``` lp15@63130 ` 758` ``` apply (rule power2_eq_imp_eq) ``` lp15@63130 ` 759` ``` apply (simp_all add: dot_square_norm [symmetric] divide_simps vector_add_divide_simps) ``` lp15@63130 ` 760` ``` apply (simp add: algebra_simps inner_commute) ``` lp15@63130 ` 761` ``` done ``` lp15@63130 ` 762` ``` have [simp]: "\x. \x \ T; b \ x = 0\ \ b \ g x \ 1" ``` lp15@63130 ` 763` ``` unfolding g_def ``` lp15@63130 ` 764` ``` apply (simp_all add: dot_square_norm [symmetric] divide_simps vector_add_divide_simps add_nonneg_eq_0_iff) ``` lp15@63130 ` 765` ``` apply (auto simp: algebra_simps) ``` lp15@63130 ` 766` ``` done ``` lp15@63130 ` 767` ``` have "subspace T" ``` lp15@63130 ` 768` ``` by (simp add: assms subspace_affine) ``` lp15@63130 ` 769` ``` have [simp]: "\x. \x \ T; b \ x = 0\ \ g x \ T" ``` lp15@63130 ` 770` ``` unfolding g_def ``` lp15@63130 ` 771` ``` by (blast intro: \subspace T\ \b \ T\ subspace_add subspace_mul subspace_diff) ``` lp15@63130 ` 772` ``` have "f ` {x. norm x = 1 \ b\x \ 1} \ {x. b\x = 0}" ``` lp15@63130 ` 773` ``` unfolding f_def using \norm b = 1\ norm_eq_1 ``` lp15@63130 ` 774` ``` by (force simp: field_simps inner_add_right inner_diff_right) ``` lp15@63130 ` 775` ``` moreover have "f ` T \ T" ``` lp15@63130 ` 776` ``` unfolding f_def using assms ``` lp15@63130 ` 777` ``` apply (auto simp: field_simps inner_add_right inner_diff_right) ``` lp15@63130 ` 778` ``` by (metis add_0 diff_zero mem_affine_3_minus) ``` lp15@63130 ` 779` ``` moreover have "{x. b\x = 0} \ T \ f ` ({x. norm x = 1 \ b\x \ 1} \ T)" ``` lp15@63130 ` 780` ``` apply clarify ``` lp15@63130 ` 781` ``` apply (rule_tac x = "g x" in image_eqI, auto) ``` lp15@63130 ` 782` ``` done ``` lp15@63130 ` 783` ``` ultimately have imf: "f ` ({x. norm x = 1 \ b\x \ 1} \ T) = {x. b\x = 0} \ T" ``` lp15@63130 ` 784` ``` by blast ``` lp15@63130 ` 785` ``` have no4: "\y. b\y = 0 \ norm ((y\y + 4) *\<^sub>R b + 4 *\<^sub>R (y - 2 *\<^sub>R b)) = y\y + 4" ``` lp15@63130 ` 786` ``` apply (rule power2_eq_imp_eq) ``` lp15@63130 ` 787` ``` apply (simp_all add: dot_square_norm [symmetric]) ``` lp15@63130 ` 788` ``` apply (auto simp: power2_eq_square algebra_simps inner_commute) ``` lp15@63130 ` 789` ``` done ``` lp15@63130 ` 790` ``` have [simp]: "\x. \norm x = 1; b \ x \ 1\ \ b \ f x = 0" ``` lp15@63130 ` 791` ``` by (simp add: f_def algebra_simps divide_simps) ``` lp15@63130 ` 792` ``` have [simp]: "\x. \x \ T; norm x = 1; b \ x \ 1\ \ f x \ T" ``` lp15@63130 ` 793` ``` unfolding f_def ``` lp15@63130 ` 794` ``` by (blast intro: \subspace T\ \b \ T\ subspace_add subspace_mul subspace_diff) ``` lp15@63130 ` 795` ``` have "g ` {x. b\x = 0} \ {x. norm x = 1 \ b\x \ 1}" ``` lp15@63130 ` 796` ``` unfolding g_def ``` lp15@63130 ` 797` ``` apply (clarsimp simp: no4 vector_add_divide_simps divide_simps add_nonneg_eq_0_iff dot_square_norm [symmetric]) ``` lp15@63130 ` 798` ``` apply (auto simp: algebra_simps) ``` lp15@63130 ` 799` ``` done ``` lp15@63130 ` 800` ``` moreover have "g ` T \ T" ``` lp15@63130 ` 801` ``` unfolding g_def ``` lp15@63130 ` 802` ``` by (blast intro: \subspace T\ \b \ T\ subspace_add subspace_mul subspace_diff) ``` lp15@63130 ` 803` ``` moreover have "{x. norm x = 1 \ b\x \ 1} \ T \ g ` ({x. b\x = 0} \ T)" ``` lp15@63130 ` 804` ``` apply clarify ``` lp15@63130 ` 805` ``` apply (rule_tac x = "f x" in image_eqI, auto) ``` lp15@63130 ` 806` ``` done ``` lp15@63130 ` 807` ``` ultimately have img: "g ` ({x. b\x = 0} \ T) = {x. norm x = 1 \ b\x \ 1} \ T" ``` lp15@63130 ` 808` ``` by blast ``` lp15@63130 ` 809` ``` have aff: "affine ({x. b\x = 0} \ T)" ``` lp15@63130 ` 810` ``` by (blast intro: affine_hyperplane assms) ``` lp15@63130 ` 811` ``` have contf: "continuous_on ({x. norm x = 1 \ b\x \ 1} \ T) f" ``` lp15@63130 ` 812` ``` unfolding f_def by (rule continuous_intros | force)+ ``` lp15@63130 ` 813` ``` have contg: "continuous_on ({x. b\x = 0} \ T) g" ``` lp15@63130 ` 814` ``` unfolding g_def by (rule continuous_intros | force simp: add_nonneg_eq_0_iff)+ ``` lp15@63130 ` 815` ``` have "(sphere 0 1 \ T) - {b} = {x. norm x = 1 \ (b\x \ 1)} \ T" ``` lp15@63130 ` 816` ``` using \norm b = 1\ by (auto simp: norm_eq_1) (metis vector_eq \b\b = 1\) ``` lp15@63130 ` 817` ``` also have "... homeomorphic {x. b\x = 0} \ T" ``` lp15@63130 ` 818` ``` by (rule homeomorphicI [OF imf img contf contg]) auto ``` lp15@63130 ` 819` ``` also have "... homeomorphic p" ``` lp15@63130 ` 820` ``` apply (rule homeomorphic_affine_sets [OF aff \affine p\]) ``` lp15@63130 ` 821` ``` apply (simp add: Int_commute aff_dim_affine_Int_hyperplane [OF \affine T\] affT) ``` lp15@63130 ` 822` ``` done ``` lp15@63130 ` 823` ``` finally show ?thesis . ``` lp15@63130 ` 824` ```qed ``` lp15@63130 ` 825` lp15@63130 ` 826` ```theorem homeomorphic_punctured_affine_sphere_affine: ``` lp15@63130 ` 827` ``` fixes a :: "'a :: euclidean_space" ``` lp15@63130 ` 828` ``` assumes "0 < r" "b \ sphere a r" "affine T" "a \ T" "b \ T" "affine p" ``` lp15@63130 ` 829` ``` and aff: "aff_dim T = aff_dim p + 1" ``` lp15@66710 ` 830` ``` shows "(sphere a r \ T) - {b} homeomorphic p" ``` lp15@63130 ` 831` ```proof - ``` lp15@63130 ` 832` ``` have "a \ b" using assms by auto ``` lp15@63130 ` 833` ``` then have inj: "inj (\x::'a. x /\<^sub>R norm (a - b))" ``` lp15@63130 ` 834` ``` by (simp add: inj_on_def) ``` lp15@63130 ` 835` ``` have "((sphere a r \ T) - {b}) homeomorphic ``` nipkow@67399 ` 836` ``` (+) (-a) ` ((sphere a r \ T) - {b})" ``` lp15@63130 ` 837` ``` by (rule homeomorphic_translation) ``` nipkow@67399 ` 838` ``` also have "... homeomorphic ( *\<^sub>R) (inverse r) ` (+) (- a) ` (sphere a r \ T - {b})" ``` lp15@63130 ` 839` ``` by (metis \0 < r\ homeomorphic_scaling inverse_inverse_eq inverse_zero less_irrefl) ``` nipkow@67399 ` 840` ``` also have "... = sphere 0 1 \ (( *\<^sub>R) (inverse r) ` (+) (- a) ` T) - {(b - a) /\<^sub>R r}" ``` lp15@63130 ` 841` ``` using assms by (auto simp: dist_norm norm_minus_commute divide_simps) ``` lp15@63130 ` 842` ``` also have "... homeomorphic p" ``` lp15@63130 ` 843` ``` apply (rule homeomorphic_punctured_affine_sphere_affine_01) ``` lp15@63130 ` 844` ``` using assms ``` lp15@63130 ` 845` ``` apply (auto simp: dist_norm norm_minus_commute affine_scaling affine_translation [symmetric] aff_dim_translation_eq inj) ``` lp15@63130 ` 846` ``` done ``` lp15@63130 ` 847` ``` finally show ?thesis . ``` lp15@63130 ` 848` ```qed ``` lp15@63130 ` 849` lp15@66710 ` 850` ```corollary homeomorphic_punctured_sphere_affine: ``` lp15@66710 ` 851` ``` fixes a :: "'a :: euclidean_space" ``` lp15@66710 ` 852` ``` assumes "0 < r" and b: "b \ sphere a r" ``` lp15@66710 ` 853` ``` and "affine T" and affS: "aff_dim T + 1 = DIM('a)" ``` lp15@66710 ` 854` ``` shows "(sphere a r - {b}) homeomorphic T" ``` lp15@66710 ` 855` ``` using homeomorphic_punctured_affine_sphere_affine [of r b a UNIV T] assms by auto ``` lp15@66710 ` 856` lp15@66710 ` 857` ```corollary homeomorphic_punctured_sphere_hyperplane: ``` lp15@66710 ` 858` ``` fixes a :: "'a :: euclidean_space" ``` lp15@66710 ` 859` ``` assumes "0 < r" and b: "b \ sphere a r" ``` lp15@66710 ` 860` ``` and "c \ 0" ``` lp15@66710 ` 861` ``` shows "(sphere a r - {b}) homeomorphic {x::'a. c \ x = d}" ``` lp15@66710 ` 862` ```apply (rule homeomorphic_punctured_sphere_affine) ``` lp15@66710 ` 863` ```using assms ``` lp15@66710 ` 864` ```apply (auto simp: affine_hyperplane of_nat_diff) ``` lp15@66710 ` 865` ```done ``` lp15@66710 ` 866` lp15@63130 ` 867` ```proposition homeomorphic_punctured_sphere_affine_gen: ``` lp15@63130 ` 868` ``` fixes a :: "'a :: euclidean_space" ``` lp15@63130 ` 869` ``` assumes "convex S" "bounded S" and a: "a \ rel_frontier S" ``` lp15@63130 ` 870` ``` and "affine T" and affS: "aff_dim S = aff_dim T + 1" ``` lp15@63130 ` 871` ``` shows "rel_frontier S - {a} homeomorphic T" ``` lp15@63130 ` 872` ```proof - ``` lp15@66690 ` 873` ``` obtain U :: "'a set" where "affine U" "convex U" and affdS: "aff_dim U = aff_dim S" ``` lp15@63130 ` 874` ``` using choose_affine_subset [OF affine_UNIV aff_dim_geq] ``` lp15@66690 ` 875` ``` by (meson aff_dim_affine_hull affine_affine_hull affine_imp_convex) ``` lp15@66690 ` 876` ``` have "S \ {}" using assms by auto ``` lp15@63130 ` 877` ``` then obtain z where "z \ U" ``` lp15@66690 ` 878` ``` by (metis aff_dim_negative_iff equals0I affdS) ``` lp15@63130 ` 879` ``` then have bne: "ball z 1 \ U \ {}" by force ``` lp15@66690 ` 880` ``` then have [simp]: "aff_dim(ball z 1 \ U) = aff_dim U" ``` lp15@66690 ` 881` ``` using aff_dim_convex_Int_open [OF \convex U\ open_ball] ``` lp15@63130 ` 882` ``` by (fastforce simp add: Int_commute) ``` lp15@63130 ` 883` ``` have "rel_frontier S homeomorphic rel_frontier (ball z 1 \ U)" ``` lp15@68006 ` 884` ``` by (rule homeomorphic_rel_frontiers_convex_bounded_sets) ``` lp15@68006 ` 885` ``` (auto simp: \affine U\ affine_imp_convex convex_Int affdS assms) ``` lp15@63130 ` 886` ``` also have "... = sphere z 1 \ U" ``` lp15@63130 ` 887` ``` using convex_affine_rel_frontier_Int [of "ball z 1" U] ``` lp15@63130 ` 888` ``` by (simp add: \affine U\ bne) ``` lp15@66690 ` 889` ``` finally have "rel_frontier S homeomorphic sphere z 1 \ U" . ``` lp15@66690 ` 890` ``` then obtain h k where him: "h ` rel_frontier S = sphere z 1 \ U" ``` lp15@63130 ` 891` ``` and kim: "k ` (sphere z 1 \ U) = rel_frontier S" ``` lp15@63130 ` 892` ``` and hcon: "continuous_on (rel_frontier S) h" ``` lp15@63130 ` 893` ``` and kcon: "continuous_on (sphere z 1 \ U) k" ``` lp15@63130 ` 894` ``` and kh: "\x. x \ rel_frontier S \ k(h(x)) = x" ``` lp15@63130 ` 895` ``` and hk: "\y. y \ sphere z 1 \ U \ h(k(y)) = y" ``` lp15@63130 ` 896` ``` unfolding homeomorphic_def homeomorphism_def by auto ``` lp15@63130 ` 897` ``` have "rel_frontier S - {a} homeomorphic (sphere z 1 \ U) - {h a}" ``` lp15@66690 ` 898` ``` proof (rule homeomorphicI) ``` lp15@63130 ` 899` ``` show h: "h ` (rel_frontier S - {a}) = sphere z 1 \ U - {h a}" ``` lp15@63130 ` 900` ``` using him a kh by auto metis ``` lp15@63130 ` 901` ``` show "k ` (sphere z 1 \ U - {h a}) = rel_frontier S - {a}" ``` lp15@63130 ` 902` ``` by (force simp: h [symmetric] image_comp o_def kh) ``` lp15@63130 ` 903` ``` qed (auto intro: continuous_on_subset hcon kcon simp: kh hk) ``` lp15@63130 ` 904` ``` also have "... homeomorphic T" ``` lp15@68006 ` 905` ``` by (rule homeomorphic_punctured_affine_sphere_affine) ``` lp15@68006 ` 906` ``` (use a him in \auto simp: affS affdS \affine T\ \affine U\ \z \ U\\) ``` lp15@63130 ` 907` ``` finally show ?thesis . ``` lp15@63130 ` 908` ```qed ``` lp15@63130 ` 909` lp15@63130 ` 910` lp15@63130 ` 911` ```text\ When dealing with AR, ANR and ANR later, it's useful to know that every set ``` lp15@63130 ` 912` ``` is homeomorphic to a closed subset of a convex set, and ``` lp15@63130 ` 913` ``` if the set is locally compact we can take the convex set to be the universe.\ ``` lp15@63130 ` 914` lp15@63130 ` 915` ```proposition homeomorphic_closedin_convex: ``` lp15@63130 ` 916` ``` fixes S :: "'m::euclidean_space set" ``` lp15@63130 ` 917` ``` assumes "aff_dim S < DIM('n)" ``` lp15@63130 ` 918` ``` obtains U and T :: "'n::euclidean_space set" ``` lp15@63130 ` 919` ``` where "convex U" "U \ {}" "closedin (subtopology euclidean U) T" ``` lp15@63130 ` 920` ``` "S homeomorphic T" ``` lp15@63130 ` 921` ```proof (cases "S = {}") ``` lp15@63130 ` 922` ``` case True then show ?thesis ``` lp15@63130 ` 923` ``` by (rule_tac U=UNIV and T="{}" in that) auto ``` lp15@63130 ` 924` ```next ``` lp15@63130 ` 925` ``` case False ``` lp15@63130 ` 926` ``` then obtain a where "a \ S" by auto ``` lp15@63130 ` 927` ``` obtain i::'n where i: "i \ Basis" "i \ 0" ``` lp15@63130 ` 928` ``` using SOME_Basis Basis_zero by force ``` nipkow@67399 ` 929` ``` have "0 \ affine hull ((+) (- a) ` S)" ``` lp15@63130 ` 930` ``` by (simp add: \a \ S\ hull_inc) ``` nipkow@67399 ` 931` ``` then have "dim ((+) (- a) ` S) = aff_dim ((+) (- a) ` S)" ``` lp15@63130 ` 932` ``` by (simp add: aff_dim_zero) ``` lp15@63130 ` 933` ``` also have "... < DIM('n)" ``` lp15@63130 ` 934` ``` by (simp add: aff_dim_translation_eq assms) ``` nipkow@67399 ` 935` ``` finally have dd: "dim ((+) (- a) ` S) < DIM('n)" ``` lp15@63130 ` 936` ``` by linarith ``` lp15@63130 ` 937` ``` obtain T where "subspace T" and Tsub: "T \ {x. i \ x = 0}" ``` nipkow@67399 ` 938` ``` and dimT: "dim T = dim ((+) (- a) ` S)" ``` nipkow@67399 ` 939` ``` apply (rule choose_subspace_of_subspace [of "dim ((+) (- a) ` S)" "{x::'n. i \ x = 0}"]) ``` lp15@63130 ` 940` ``` apply (simp add: dim_hyperplane [OF \i \ 0\]) ``` lp15@63130 ` 941` ``` apply (metis DIM_positive Suc_pred dd not_le not_less_eq_eq) ``` lp15@63130 ` 942` ``` apply (metis span_eq subspace_hyperplane) ``` lp15@63130 ` 943` ``` done ``` nipkow@67399 ` 944` ``` have "subspace (span ((+) (- a) ` S))" ``` lp15@63130 ` 945` ``` using subspace_span by blast ``` lp15@63130 ` 946` ``` then obtain h k where "linear h" "linear k" ``` nipkow@67399 ` 947` ``` and heq: "h ` span ((+) (- a) ` S) = T" ``` nipkow@67399 ` 948` ``` and keq:"k ` T = span ((+) (- a) ` S)" ``` nipkow@67399 ` 949` ``` and hinv [simp]: "\x. x \ span ((+) (- a) ` S) \ k(h x) = x" ``` lp15@63130 ` 950` ``` and kinv [simp]: "\x. x \ T \ h(k x) = x" ``` lp15@63130 ` 951` ``` apply (rule isometries_subspaces [OF _ \subspace T\]) ``` lp15@63130 ` 952` ``` apply (auto simp: dimT) ``` lp15@63130 ` 953` ``` done ``` lp15@63130 ` 954` ``` have hcont: "continuous_on A h" and kcont: "continuous_on B k" for A B ``` lp15@63130 ` 955` ``` using \linear h\ \linear k\ linear_continuous_on linear_conv_bounded_linear by blast+ ``` lp15@63130 ` 956` ``` have ihhhh[simp]: "\x. x \ S \ i \ h (x - a) = 0" ``` lp15@63130 ` 957` ``` using Tsub [THEN subsetD] heq span_inc by fastforce ``` lp15@63130 ` 958` ``` have "sphere 0 1 - {i} homeomorphic {x. i \ x = 0}" ``` lp15@63130 ` 959` ``` apply (rule homeomorphic_punctured_sphere_affine) ``` lp15@63130 ` 960` ``` using i ``` lp15@63130 ` 961` ``` apply (auto simp: affine_hyperplane) ``` lp15@63130 ` 962` ``` by (metis DIM_positive Suc_eq_plus1 add.left_neutral diff_add_cancel not_le not_less_eq_eq of_nat_1 of_nat_diff) ``` lp15@63130 ` 963` ``` then obtain f g where fg: "homeomorphism (sphere 0 1 - {i}) {x. i \ x = 0} f g" ``` lp15@63130 ` 964` ``` by (force simp: homeomorphic_def) ``` nipkow@67399 ` 965` ``` have "h ` (+) (- a) ` S \ T" ``` lp15@63130 ` 966` ``` using heq span_clauses(1) span_linear_image by blast ``` nipkow@67399 ` 967` ``` then have "g ` h ` (+) (- a) ` S \ g ` {x. i \ x = 0}" ``` lp15@63130 ` 968` ``` using Tsub by (simp add: image_mono) ``` lp15@63130 ` 969` ``` also have "... \ sphere 0 1 - {i}" ``` lp15@63130 ` 970` ``` by (simp add: fg [unfolded homeomorphism_def]) ``` nipkow@67399 ` 971` ``` finally have gh_sub_sph: "(g \ h) ` (+) (- a) ` S \ sphere 0 1 - {i}" ``` lp15@63130 ` 972` ``` by (metis image_comp) ``` nipkow@67399 ` 973` ``` then have gh_sub_cb: "(g \ h) ` (+) (- a) ` S \ cball 0 1" ``` lp15@63130 ` 974` ``` by (metis Diff_subset order_trans sphere_cball) ``` lp15@63130 ` 975` ``` have [simp]: "\u. u \ S \ norm (g (h (u - a))) = 1" ``` lp15@63130 ` 976` ``` using gh_sub_sph [THEN subsetD] by (auto simp: o_def) ``` nipkow@67399 ` 977` ``` have ghcont: "continuous_on ((+) (- a) ` S) (\x. g (h x))" ``` lp15@63130 ` 978` ``` apply (rule continuous_on_compose2 [OF homeomorphism_cont2 [OF fg] hcont], force) ``` lp15@63130 ` 979` ``` done ``` nipkow@67399 ` 980` ``` have kfcont: "continuous_on ((g \ h \ (+) (- a)) ` S) (\x. k (f x))" ``` lp15@63130 ` 981` ``` apply (rule continuous_on_compose2 [OF kcont]) ``` lp15@63130 ` 982` ``` using homeomorphism_cont1 [OF fg] gh_sub_sph apply (force intro: continuous_on_subset, blast) ``` lp15@63130 ` 983` ``` done ``` nipkow@67399 ` 984` ``` have "S homeomorphic (+) (- a) ` S" ``` lp15@63130 ` 985` ``` by (simp add: homeomorphic_translation) ``` nipkow@67399 ` 986` ``` also have Shom: "\ homeomorphic (g \ h) ` (+) (- a) ` S" ``` lp15@63130 ` 987` ``` apply (simp add: homeomorphic_def homeomorphism_def) ``` lp15@63130 ` 988` ``` apply (rule_tac x="g \ h" in exI) ``` lp15@63130 ` 989` ``` apply (rule_tac x="k \ f" in exI) ``` lp15@63130 ` 990` ``` apply (auto simp: ghcont kfcont span_clauses(1) homeomorphism_apply2 [OF fg] image_comp) ``` lp15@63130 ` 991` ``` apply (force simp: o_def homeomorphism_apply2 [OF fg] span_clauses(1)) ``` lp15@63130 ` 992` ``` done ``` nipkow@67399 ` 993` ``` finally have Shom: "S homeomorphic (g \ h) ` (+) (- a) ` S" . ``` lp15@63130 ` 994` ``` show ?thesis ``` nipkow@67399 ` 995` ``` apply (rule_tac U = "ball 0 1 \ image (g o h) ((+) (- a) ` S)" ``` nipkow@67399 ` 996` ``` and T = "image (g o h) ((+) (- a) ` S)" ``` lp15@63130 ` 997` ``` in that) ``` lp15@63130 ` 998` ``` apply (rule convex_intermediate_ball [of 0 1], force) ``` lp15@63130 ` 999` ``` using gh_sub_cb apply force ``` lp15@63130 ` 1000` ``` apply force ``` lp15@63130 ` 1001` ``` apply (simp add: closedin_closed) ``` lp15@63130 ` 1002` ``` apply (rule_tac x="sphere 0 1" in exI) ``` lp15@63130 ` 1003` ``` apply (auto simp: Shom) ``` lp15@63130 ` 1004` ``` done ``` lp15@63130 ` 1005` ```qed ``` lp15@63130 ` 1006` lp15@63130 ` 1007` ```subsection\Locally compact sets in an open set\ ``` lp15@63130 ` 1008` lp15@63130 ` 1009` ```text\ Locally compact sets are closed in an open set and are homeomorphic ``` lp15@63130 ` 1010` ``` to an absolutely closed set if we have one more dimension to play with.\ ``` lp15@63130 ` 1011` lp15@63130 ` 1012` ```lemma locally_compact_open_Int_closure: ``` lp15@63130 ` 1013` ``` fixes S :: "'a :: metric_space set" ``` lp15@63130 ` 1014` ``` assumes "locally compact S" ``` lp15@63130 ` 1015` ``` obtains T where "open T" "S = T \ closure S" ``` lp15@63130 ` 1016` ```proof - ``` lp15@63130 ` 1017` ``` have "\x\S. \T v u. u = S \ T \ x \ u \ u \ v \ v \ S \ open T \ compact v" ``` lp15@63130 ` 1018` ``` by (metis assms locally_compact openin_open) ``` lp15@63130 ` 1019` ``` then obtain t v where ``` lp15@63130 ` 1020` ``` tv: "\x. x \ S ``` lp15@63130 ` 1021` ``` \ v x \ S \ open (t x) \ compact (v x) \ (\u. x \ u \ u \ v x \ u = S \ t x)" ``` lp15@63130 ` 1022` ``` by metis ``` lp15@63130 ` 1023` ``` then have o: "open (UNION S t)" ``` lp15@63130 ` 1024` ``` by blast ``` lp15@63130 ` 1025` ``` have "S = \ (v ` S)" ``` lp15@63130 ` 1026` ``` using tv by blast ``` lp15@63130 ` 1027` ``` also have "... = UNION S t \ closure S" ``` lp15@63130 ` 1028` ``` proof ``` lp15@63130 ` 1029` ``` show "UNION S v \ UNION S t \ closure S" ``` lp15@63130 ` 1030` ``` apply safe ``` lp15@63130 ` 1031` ``` apply (metis Int_iff subsetD UN_iff tv) ``` lp15@63130 ` 1032` ``` apply (simp add: closure_def rev_subsetD tv) ``` lp15@63130 ` 1033` ``` done ``` lp15@63130 ` 1034` ``` have "t x \ closure S \ v x" if "x \ S" for x ``` lp15@63130 ` 1035` ``` proof - ``` lp15@63130 ` 1036` ``` have "t x \ closure S \ closure (t x \ S)" ``` lp15@63130 ` 1037` ``` by (simp add: open_Int_closure_subset that tv) ``` lp15@63130 ` 1038` ``` also have "... \ v x" ``` lp15@63130 ` 1039` ``` by (metis Int_commute closure_minimal compact_imp_closed that tv) ``` lp15@63130 ` 1040` ``` finally show ?thesis . ``` lp15@63130 ` 1041` ``` qed ``` lp15@63130 ` 1042` ``` then show "UNION S t \ closure S \ UNION S v" ``` lp15@63130 ` 1043` ``` by blast ``` lp15@63130 ` 1044` ``` qed ``` lp15@63130 ` 1045` ``` finally have e: "S = UNION S t \ closure S" . ``` lp15@63130 ` 1046` ``` show ?thesis ``` lp15@63130 ` 1047` ``` by (rule that [OF o e]) ``` lp15@63130 ` 1048` ```qed ``` lp15@63130 ` 1049` lp15@63130 ` 1050` lp15@63130 ` 1051` ```lemma locally_compact_closedin_open: ``` lp15@63130 ` 1052` ``` fixes S :: "'a :: metric_space set" ``` lp15@63130 ` 1053` ``` assumes "locally compact S" ``` lp15@63130 ` 1054` ``` obtains T where "open T" "closedin (subtopology euclidean T) S" ``` lp15@63130 ` 1055` ``` by (metis locally_compact_open_Int_closure [OF assms] closed_closure closedin_closed_Int) ``` lp15@63130 ` 1056` lp15@63130 ` 1057` lp15@63130 ` 1058` ```lemma locally_compact_homeomorphism_projection_closed: ``` lp15@63130 ` 1059` ``` assumes "locally compact S" ``` lp15@63130 ` 1060` ``` obtains T and f :: "'a \ 'a :: euclidean_space \ 'b :: euclidean_space" ``` lp15@63130 ` 1061` ``` where "closed T" "homeomorphism S T f fst" ``` lp15@63130 ` 1062` ```proof (cases "closed S") ``` lp15@63130 ` 1063` ``` case True ``` lp15@63130 ` 1064` ``` then show ?thesis ``` lp15@63130 ` 1065` ``` apply (rule_tac T = "S \ {0}" and f = "\x. (x, 0)" in that) ``` lp15@63130 ` 1066` ``` apply (auto simp: closed_Times homeomorphism_def continuous_intros) ``` lp15@63130 ` 1067` ``` done ``` lp15@63130 ` 1068` ```next ``` lp15@63130 ` 1069` ``` case False ``` lp15@63130 ` 1070` ``` obtain U where "open U" and US: "U \ closure S = S" ``` lp15@63130 ` 1071` ``` by (metis locally_compact_open_Int_closure [OF assms]) ``` lp15@63130 ` 1072` ``` with False have Ucomp: "-U \ {}" ``` lp15@63130 ` 1073` ``` using closure_eq by auto ``` lp15@63130 ` 1074` ``` have [simp]: "closure (- U) = -U" ``` lp15@63130 ` 1075` ``` by (simp add: \open U\ closed_Compl) ``` lp15@63130 ` 1076` ``` define f :: "'a \ 'a \ 'b" where "f \ \x. (x, One /\<^sub>R setdist {x} (- U))" ``` lp15@63130 ` 1077` ``` have "continuous_on U (\x. (x, One /\<^sub>R setdist {x} (- U)))" ``` lp15@63301 ` 1078` ``` apply (intro continuous_intros continuous_on_setdist) ``` lp15@63301 ` 1079` ``` by (simp add: Ucomp setdist_eq_0_sing_1) ``` lp15@63130 ` 1080` ``` then have homU: "homeomorphism U (f`U) f fst" ``` lp15@63130 ` 1081` ``` by (auto simp: f_def homeomorphism_def image_iff continuous_intros) ``` lp15@63130 ` 1082` ``` have cloS: "closedin (subtopology euclidean U) S" ``` lp15@63130 ` 1083` ``` by (metis US closed_closure closedin_closed_Int) ``` lp15@63130 ` 1084` ``` have cont: "isCont ((\x. setdist {x} (- U)) o fst) z" for z :: "'a \ 'b" ``` lp15@66827 ` 1085` ``` by (rule continuous_at_compose continuous_intros continuous_at_setdist)+ ``` lp15@63130 ` 1086` ``` have setdist1D: "setdist {a} (- U) *\<^sub>R b = One \ setdist {a} (- U) \ 0" for a::'a and b::'b ``` lp15@63130 ` 1087` ``` by force ``` lp15@63130 ` 1088` ``` have *: "r *\<^sub>R b = One \ b = (1 / r) *\<^sub>R One" for r and b::'b ``` lp15@63130 ` 1089` ``` by (metis One_non_0 nonzero_divide_eq_eq real_vector.scale_eq_0_iff real_vector.scale_scale scaleR_one) ``` lp15@66884 ` 1090` ``` have "f ` U = (\z. (setdist {fst z} (- U) *\<^sub>R snd z)) -` {One}" ``` lp15@63301 ` 1091` ``` apply (auto simp: f_def setdist_eq_0_sing_1 field_simps Ucomp) ``` lp15@63130 ` 1092` ``` apply (rule_tac x=a in image_eqI) ``` lp15@63301 ` 1093` ``` apply (auto simp: * setdist_eq_0_sing_1 dest: setdist1D) ``` lp15@63130 ` 1094` ``` done ``` lp15@63130 ` 1095` ``` then have clfU: "closed (f ` U)" ``` lp15@63130 ` 1096` ``` apply (rule ssubst) ``` lp15@66884 ` 1097` ``` apply (rule continuous_closed_vimage) ``` lp15@63130 ` 1098` ``` apply (auto intro: continuous_intros cont [unfolded o_def]) ``` lp15@63130 ` 1099` ``` done ``` lp15@63130 ` 1100` ``` have "closed (f ` S)" ``` lp15@63130 ` 1101` ``` apply (rule closedin_closed_trans [OF _ clfU]) ``` lp15@63130 ` 1102` ``` apply (rule homeomorphism_imp_closed_map [OF homU cloS]) ``` lp15@63130 ` 1103` ``` done ``` lp15@63130 ` 1104` ``` then show ?thesis ``` lp15@63130 ` 1105` ``` apply (rule that) ``` lp15@63130 ` 1106` ``` apply (rule homeomorphism_of_subsets [OF homU]) ``` lp15@63130 ` 1107` ``` using US apply auto ``` lp15@63130 ` 1108` ``` done ``` lp15@63130 ` 1109` ```qed ``` lp15@63130 ` 1110` lp15@63130 ` 1111` ```lemma locally_compact_closed_Int_open: ``` lp15@63130 ` 1112` ``` fixes S :: "'a :: euclidean_space set" ``` lp15@63130 ` 1113` ``` shows ``` lp15@63130 ` 1114` ``` "locally compact S \ (\U u. closed U \ open u \ S = U \ u)" ``` lp15@63130 ` 1115` ```by (metis closed_closure closed_imp_locally_compact inf_commute locally_compact_Int locally_compact_open_Int_closure open_imp_locally_compact) ``` lp15@63130 ` 1116` lp15@63130 ` 1117` lp15@63945 ` 1118` ```lemma lowerdim_embeddings: ``` lp15@63945 ` 1119` ``` assumes "DIM('a) < DIM('b)" ``` lp15@63945 ` 1120` ``` obtains f :: "'a::euclidean_space*real \ 'b::euclidean_space" ``` lp15@63945 ` 1121` ``` and g :: "'b \ 'a*real" ``` lp15@63945 ` 1122` ``` and j :: 'b ``` lp15@63945 ` 1123` ``` where "linear f" "linear g" "\z. g (f z) = z" "j \ Basis" "\x. f(x,0) \ j = 0" ``` lp15@63945 ` 1124` ```proof - ``` lp15@63945 ` 1125` ``` let ?B = "Basis :: ('a*real) set" ``` lp15@63945 ` 1126` ``` have b01: "(0,1) \ ?B" ``` lp15@63945 ` 1127` ``` by (simp add: Basis_prod_def) ``` lp15@63945 ` 1128` ``` have "DIM('a * real) \ DIM('b)" ``` lp15@63945 ` 1129` ``` by (simp add: Suc_leI assms) ``` lp15@63945 ` 1130` ``` then obtain basf :: "'a*real \ 'b" where sbf: "basf ` ?B \ Basis" and injbf: "inj_on basf Basis" ``` lp15@63945 ` 1131` ``` by (metis finite_Basis card_le_inj) ``` lp15@63945 ` 1132` ``` define basg:: "'b \ 'a * real" where ``` lp15@63945 ` 1133` ``` "basg \ \i. if i \ basf ` Basis then inv_into Basis basf i else (0,1)" ``` lp15@63945 ` 1134` ``` have bgf[simp]: "basg (basf i) = i" if "i \ Basis" for i ``` lp15@63945 ` 1135` ``` using inv_into_f_f injbf that by (force simp: basg_def) ``` lp15@63945 ` 1136` ``` have sbg: "basg ` Basis \ ?B" ``` lp15@63945 ` 1137` ``` by (force simp: basg_def injbf b01) ``` lp15@63945 ` 1138` ``` define f :: "'a*real \ 'b" where "f \ \u. \j\Basis. (u \ basg j) *\<^sub>R j" ``` lp15@63945 ` 1139` ``` define g :: "'b \ 'a*real" where "g \ \z. (\i\Basis. (z \ basf i) *\<^sub>R i)" ``` lp15@63945 ` 1140` ``` show ?thesis ``` lp15@63945 ` 1141` ``` proof ``` lp15@63945 ` 1142` ``` show "linear f" ``` lp15@63945 ` 1143` ``` unfolding f_def ``` nipkow@64267 ` 1144` ``` by (intro linear_compose_sum linearI ballI) (auto simp: algebra_simps) ``` lp15@63945 ` 1145` ``` show "linear g" ``` lp15@63945 ` 1146` ``` unfolding g_def ``` nipkow@64267 ` 1147` ``` by (intro linear_compose_sum linearI ballI) (auto simp: algebra_simps) ``` lp15@63945 ` 1148` ``` have *: "(\a \ Basis. a \ basf b * (x \ basg a)) = x \ b" if "b \ Basis" for x b ``` lp15@63945 ` 1149` ``` using sbf that by auto ``` lp15@63945 ` 1150` ``` show gf: "g (f x) = x" for x ``` lp15@63945 ` 1151` ``` apply (rule euclidean_eqI) ``` nipkow@64267 ` 1152` ``` apply (simp add: f_def g_def inner_sum_left scaleR_sum_left algebra_simps) ``` nipkow@64267 ` 1153` ``` apply (simp add: Groups_Big.sum_distrib_left [symmetric] *) ``` lp15@63945 ` 1154` ``` done ``` lp15@63945 ` 1155` ``` show "basf(0,1) \ Basis" ``` lp15@63945 ` 1156` ``` using b01 sbf by auto ``` lp15@63945 ` 1157` ``` then show "f(x,0) \ basf(0,1) = 0" for x ``` nipkow@64267 ` 1158` ``` apply (simp add: f_def inner_sum_left) ``` nipkow@64267 ` 1159` ``` apply (rule comm_monoid_add_class.sum.neutral) ``` lp15@63945 ` 1160` ``` using b01 inner_not_same_Basis by fastforce ``` lp15@63945 ` 1161` ``` qed ``` lp15@63945 ` 1162` ```qed ``` lp15@63945 ` 1163` lp15@63130 ` 1164` ```proposition locally_compact_homeomorphic_closed: ``` lp15@63130 ` 1165` ``` fixes S :: "'a::euclidean_space set" ``` lp15@63130 ` 1166` ``` assumes "locally compact S" and dimlt: "DIM('a) < DIM('b)" ``` lp15@63130 ` 1167` ``` obtains T :: "'b::euclidean_space set" where "closed T" "S homeomorphic T" ``` lp15@63130 ` 1168` ```proof - ``` lp15@63130 ` 1169` ``` obtain U:: "('a*real)set" and h ``` lp15@63130 ` 1170` ``` where "closed U" and homU: "homeomorphism S U h fst" ``` lp15@63130 ` 1171` ``` using locally_compact_homeomorphism_projection_closed assms by metis ``` lp15@63945 ` 1172` ``` obtain f :: "'a*real \ 'b" and g :: "'b \ 'a*real" ``` lp15@63945 ` 1173` ``` where "linear f" "linear g" and gf [simp]: "\z. g (f z) = z" ``` lp15@63945 ` 1174` ``` using lowerdim_embeddings [OF dimlt] by metis ``` lp15@63945 ` 1175` ``` then have "inj f" ``` lp15@63945 ` 1176` ``` by (metis injI) ``` lp15@63130 ` 1177` ``` have gfU: "g ` f ` U = U" ``` lp15@63945 ` 1178` ``` by (simp add: image_comp o_def) ``` lp15@63130 ` 1179` ``` have "S homeomorphic U" ``` lp15@63130 ` 1180` ``` using homU homeomorphic_def by blast ``` lp15@63130 ` 1181` ``` also have "... homeomorphic f ` U" ``` lp15@63130 ` 1182` ``` apply (rule homeomorphicI [OF refl gfU]) ``` lp15@63130 ` 1183` ``` apply (meson \inj f\ \linear f\ homeomorphism_cont2 linear_homeomorphism_image) ``` lp15@63945 ` 1184` ``` using \linear g\ linear_continuous_on linear_conv_bounded_linear apply blast ``` lp15@63945 ` 1185` ``` apply (auto simp: o_def) ``` lp15@63945 ` 1186` ``` done ``` lp15@63130 ` 1187` ``` finally show ?thesis ``` lp15@63130 ` 1188` ``` apply (rule_tac T = "f ` U" in that) ``` lp15@63130 ` 1189` ``` apply (rule closed_injective_linear_image [OF \closed U\ \linear f\ \inj f\], assumption) ``` lp15@63130 ` 1190` ``` done ``` lp15@63130 ` 1191` ```qed ``` lp15@63130 ` 1192` lp15@63130 ` 1193` lp15@63130 ` 1194` ```lemma homeomorphic_convex_compact_lemma: ``` lp15@64773 ` 1195` ``` fixes S :: "'a::euclidean_space set" ``` lp15@64773 ` 1196` ``` assumes "convex S" ``` lp15@64773 ` 1197` ``` and "compact S" ``` lp15@64773 ` 1198` ``` and "cball 0 1 \ S" ``` lp15@64773 ` 1199` ``` shows "S homeomorphic (cball (0::'a) 1)" ``` lp15@63130 ` 1200` ```proof (rule starlike_compact_projective_special[OF assms(2-3)]) ``` lp15@63130 ` 1201` ``` fix x u ``` lp15@64773 ` 1202` ``` assume "x \ S" and "0 \ u" and "u < (1::real)" ``` lp15@63130 ` 1203` ``` have "open (ball (u *\<^sub>R x) (1 - u))" ``` lp15@63130 ` 1204` ``` by (rule open_ball) ``` lp15@63130 ` 1205` ``` moreover have "u *\<^sub>R x \ ball (u *\<^sub>R x) (1 - u)" ``` lp15@63130 ` 1206` ``` unfolding centre_in_ball using \u < 1\ by simp ``` lp15@64773 ` 1207` ``` moreover have "ball (u *\<^sub>R x) (1 - u) \ S" ``` lp15@63130 ` 1208` ``` proof ``` lp15@63130 ` 1209` ``` fix y ``` lp15@63130 ` 1210` ``` assume "y \ ball (u *\<^sub>R x) (1 - u)" ``` lp15@63130 ` 1211` ``` then have "dist (u *\<^sub>R x) y < 1 - u" ``` lp15@63130 ` 1212` ``` unfolding mem_ball . ``` lp15@63130 ` 1213` ``` with \u < 1\ have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \ cball 0 1" ``` lp15@63130 ` 1214` ``` by (simp add: dist_norm inverse_eq_divide norm_minus_commute) ``` lp15@64773 ` 1215` ``` with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \ S" .. ``` lp15@64773 ` 1216` ``` with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \ S" ``` lp15@64773 ` 1217` ``` using \x \ S\ \0 \ u\ \u < 1\ [THEN less_imp_le] by (rule convexD_alt) ``` lp15@64773 ` 1218` ``` then show "y \ S" using \u < 1\ ``` lp15@63130 ` 1219` ``` by simp ``` lp15@63130 ` 1220` ``` qed ``` lp15@64773 ` 1221` ``` ultimately have "u *\<^sub>R x \ interior S" .. ``` lp15@64773 ` 1222` ``` then show "u *\<^sub>R x \ S - frontier S" ``` lp15@63130 ` 1223` ``` using frontier_def and interior_subset by auto ``` lp15@63130 ` 1224` ```qed ``` lp15@63130 ` 1225` lp15@63130 ` 1226` ```proposition homeomorphic_convex_compact_cball: ``` lp15@63130 ` 1227` ``` fixes e :: real ``` lp15@64773 ` 1228` ``` and S :: "'a::euclidean_space set" ``` lp15@64773 ` 1229` ``` assumes "convex S" ``` lp15@64773 ` 1230` ``` and "compact S" ``` lp15@64773 ` 1231` ``` and "interior S \ {}" ``` lp15@63130 ` 1232` ``` and "e > 0" ``` lp15@64773 ` 1233` ``` shows "S homeomorphic (cball (b::'a) e)" ``` lp15@63130 ` 1234` ```proof - ``` lp15@64773 ` 1235` ``` obtain a where "a \ interior S" ``` lp15@63130 ` 1236` ``` using assms(3) by auto ``` lp15@64773 ` 1237` ``` then obtain d where "d > 0" and d: "cball a d \ S" ``` lp15@63130 ` 1238` ``` unfolding mem_interior_cball by auto ``` lp15@63130 ` 1239` ``` let ?d = "inverse d" and ?n = "0::'a" ``` lp15@64773 ` 1240` ``` have "cball ?n 1 \ (\x. inverse d *\<^sub>R (x - a)) ` S" ``` lp15@63130 ` 1241` ``` apply rule ``` lp15@63130 ` 1242` ``` apply (rule_tac x="d *\<^sub>R x + a" in image_eqI) ``` lp15@63130 ` 1243` ``` defer ``` lp15@63130 ` 1244` ``` apply (rule d[unfolded subset_eq, rule_format]) ``` lp15@63130 ` 1245` ``` using \d > 0\ ``` lp15@63130 ` 1246` ``` unfolding mem_cball dist_norm ``` lp15@63130 ` 1247` ``` apply (auto simp add: mult_right_le_one_le) ``` lp15@63130 ` 1248` ``` done ``` lp15@64773 ` 1249` ``` then have "(\x. inverse d *\<^sub>R (x - a)) ` S homeomorphic cball ?n 1" ``` lp15@64773 ` 1250` ``` using homeomorphic_convex_compact_lemma[of "(\x. ?d *\<^sub>R -a + ?d *\<^sub>R x) ` S", ``` lp15@63130 ` 1251` ``` OF convex_affinity compact_affinity] ``` lp15@63130 ` 1252` ``` using assms(1,2) ``` lp15@63130 ` 1253` ``` by (auto simp add: scaleR_right_diff_distrib) ``` lp15@63130 ` 1254` ``` then show ?thesis ``` lp15@63130 ` 1255` ``` apply (rule_tac homeomorphic_trans[OF _ homeomorphic_balls(2)[of 1 _ ?n]]) ``` lp15@64773 ` 1256` ``` apply (rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" S "?d *\<^sub>R -a"]]) ``` lp15@63130 ` 1257` ``` using \d>0\ \e>0\ ``` lp15@63130 ` 1258` ``` apply (auto simp add: scaleR_right_diff_distrib) ``` lp15@63130 ` 1259` ``` done ``` lp15@63130 ` 1260` ```qed ``` lp15@63130 ` 1261` lp15@63130 ` 1262` ```corollary homeomorphic_convex_compact: ``` lp15@64773 ` 1263` ``` fixes S :: "'a::euclidean_space set" ``` lp15@64773 ` 1264` ``` and T :: "'a set" ``` lp15@64773 ` 1265` ``` assumes "convex S" "compact S" "interior S \ {}" ``` lp15@64773 ` 1266` ``` and "convex T" "compact T" "interior T \ {}" ``` lp15@64773 ` 1267` ``` shows "S homeomorphic T" ``` lp15@63130 ` 1268` ``` using assms ``` lp15@63130 ` 1269` ``` by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym) ``` lp15@63130 ` 1270` lp15@63301 ` 1271` ```subsection\Covering spaces and lifting results for them\ ``` lp15@63301 ` 1272` lp15@63301 ` 1273` ```definition covering_space ``` lp15@63301 ` 1274` ``` :: "'a::topological_space set \ ('a \ 'b) \ 'b::topological_space set \ bool" ``` lp15@63301 ` 1275` ``` where ``` lp15@64773 ` 1276` ``` "covering_space c p S \ ``` lp15@64773 ` 1277` ``` continuous_on c p \ p ` c = S \ ``` lp15@64773 ` 1278` ``` (\x \ S. \T. x \ T \ openin (subtopology euclidean S) T \ ``` lp15@66884 ` 1279` ``` (\v. \v = c \ p -` T \ ``` lp15@63301 ` 1280` ``` (\u \ v. openin (subtopology euclidean c) u) \ ``` lp15@63301 ` 1281` ``` pairwise disjnt v \ ``` lp15@64773 ` 1282` ``` (\u \ v. \q. homeomorphism u T p q)))" ``` lp15@63301 ` 1283` lp15@64773 ` 1284` ```lemma covering_space_imp_continuous: "covering_space c p S \ continuous_on c p" ``` lp15@63301 ` 1285` ``` by (simp add: covering_space_def) ``` lp15@63301 ` 1286` lp15@64773 ` 1287` ```lemma covering_space_imp_surjective: "covering_space c p S \ p ` c = S" ``` lp15@63301 ` 1288` ``` by (simp add: covering_space_def) ``` lp15@63301 ` 1289` lp15@64773 ` 1290` ```lemma homeomorphism_imp_covering_space: "homeomorphism S T f g \ covering_space S f T" ``` lp15@63301 ` 1291` ``` apply (simp add: homeomorphism_def covering_space_def, clarify) ``` lp15@64773 ` 1292` ``` apply (rule_tac x=T in exI, simp) ``` lp15@64773 ` 1293` ``` apply (rule_tac x="{S}" in exI, auto) ``` lp15@63301 ` 1294` ``` done ``` lp15@63301 ` 1295` lp15@63301 ` 1296` ```lemma covering_space_local_homeomorphism: ``` lp15@64773 ` 1297` ``` assumes "covering_space c p S" "x \ c" ``` lp15@64773 ` 1298` ``` obtains T u q where "x \ T" "openin (subtopology euclidean c) T" ``` lp15@64773 ` 1299` ``` "p x \ u" "openin (subtopology euclidean S) u" ``` lp15@64773 ` 1300` ``` "homeomorphism T u p q" ``` lp15@63301 ` 1301` ```using assms ``` lp15@63301 ` 1302` ```apply (simp add: covering_space_def, clarify) ``` lp15@66884 ` 1303` ``` apply (drule_tac x="p x" in bspec, force) ``` lp15@66884 ` 1304` ``` by (metis IntI UnionE vimage_eq) ``` lp15@63301 ` 1305` lp15@63301 ` 1306` lp15@63301 ` 1307` ```lemma covering_space_local_homeomorphism_alt: ``` lp15@64773 ` 1308` ``` assumes p: "covering_space c p S" and "y \ S" ``` lp15@66884 ` 1309` ``` obtains x T U q where "p x = y" ``` lp15@64773 ` 1310` ``` "x \ T" "openin (subtopology euclidean c) T" ``` lp15@66884 ` 1311` ``` "y \ U" "openin (subtopology euclidean S) U" ``` lp15@66884 ` 1312` ``` "homeomorphism T U p q" ``` lp15@63301 ` 1313` ```proof - ``` lp15@63301 ` 1314` ``` obtain x where "p x = y" "x \ c" ``` lp15@63301 ` 1315` ``` using assms covering_space_imp_surjective by blast ``` lp15@63301 ` 1316` ``` show ?thesis ``` lp15@63301 ` 1317` ``` apply (rule covering_space_local_homeomorphism [OF p \x \ c\]) ``` lp15@63301 ` 1318` ``` using that \p x = y\ by blast ``` lp15@63301 ` 1319` ```qed ``` lp15@63301 ` 1320` lp15@63301 ` 1321` ```proposition covering_space_open_map: ``` lp15@64773 ` 1322` ``` fixes S :: "'a :: metric_space set" and T :: "'b :: metric_space set" ``` lp15@64773 ` 1323` ``` assumes p: "covering_space c p S" and T: "openin (subtopology euclidean c) T" ``` lp15@64773 ` 1324` ``` shows "openin (subtopology euclidean S) (p ` T)" ``` lp15@63301 ` 1325` ```proof - ``` lp15@64773 ` 1326` ``` have pce: "p ` c = S" ``` lp15@63301 ` 1327` ``` and covs: ``` lp15@64773 ` 1328` ``` "\x. x \ S \ ``` lp15@64773 ` 1329` ``` \X VS. x \ X \ openin (subtopology euclidean S) X \ ``` lp15@66884 ` 1330` ``` \VS = c \ p -` X \ ``` lp15@63301 ` 1331` ``` (\u \ VS. openin (subtopology euclidean c) u) \ ``` lp15@63301 ` 1332` ``` pairwise disjnt VS \ ``` lp15@63301 ` 1333` ``` (\u \ VS. \q. homeomorphism u X p q)" ``` lp15@63301 ` 1334` ``` using p by (auto simp: covering_space_def) ``` lp15@64773 ` 1335` ``` have "T \ c" by (metis openin_euclidean_subtopology_iff T) ``` lp15@64773 ` 1336` ``` have "\X. openin (subtopology euclidean S) X \ y \ X \ X \ p ` T" ``` lp15@64773 ` 1337` ``` if "y \ p ` T" for y ``` lp15@63301 ` 1338` ``` proof - ``` lp15@64773 ` 1339` ``` have "y \ S" using \T \ c\ pce that by blast ``` lp15@64773 ` 1340` ``` obtain U VS where "y \ U" and U: "openin (subtopology euclidean S) U" ``` lp15@66884 ` 1341` ``` and VS: "\VS = c \ p -` U" ``` lp15@63301 ` 1342` ``` and openVS: "\V \ VS. openin (subtopology euclidean c) V" ``` lp15@63301 ` 1343` ``` and homVS: "\V. V \ VS \ \q. homeomorphism V U p q" ``` lp15@64773 ` 1344` ``` using covs [OF \y \ S\] by auto ``` lp15@64773 ` 1345` ``` obtain x where "x \ c" "p x \ U" "x \ T" "p x = y" ``` lp15@63301 ` 1346` ``` apply simp ``` lp15@64773 ` 1347` ``` using T [unfolded openin_euclidean_subtopology_iff] \y \ U\ \y \ p ` T\ by blast ``` lp15@63301 ` 1348` ``` with VS obtain V where "x \ V" "V \ VS" by auto ``` lp15@63301 ` 1349` ``` then obtain q where q: "homeomorphism V U p q" using homVS by blast ``` lp15@66884 ` 1350` ``` then have ptV: "p ` (T \ V) = U \ q -` (T \ V)" ``` lp15@63301 ` 1351` ``` using VS \V \ VS\ by (auto simp: homeomorphism_def) ``` lp15@63301 ` 1352` ``` have ocv: "openin (subtopology euclidean c) V" ``` lp15@63301 ` 1353` ``` by (simp add: \V \ VS\ openVS) ``` lp15@66884 ` 1354` ``` have "openin (subtopology euclidean U) (U \ q -` (T \ V))" ``` lp15@63301 ` 1355` ``` apply (rule continuous_on_open [THEN iffD1, rule_format]) ``` lp15@63301 ` 1356` ``` using homeomorphism_def q apply blast ``` lp15@64773 ` 1357` ``` using openin_subtopology_Int_subset [of c] q T unfolding homeomorphism_def ``` lp15@63301 ` 1358` ``` by (metis inf.absorb_iff2 Int_commute ocv openin_euclidean_subtopology_iff) ``` lp15@66884 ` 1359` ``` then have os: "openin (subtopology euclidean S) (U \ q -` (T \ V))" ``` lp15@63301 ` 1360` ``` using openin_trans [of U] by (simp add: Collect_conj_eq U) ``` lp15@63301 ` 1361` ``` show ?thesis ``` lp15@64773 ` 1362` ``` apply (rule_tac x = "p ` (T \ V)" in exI) ``` lp15@63301 ` 1363` ``` apply (rule conjI) ``` lp15@63301 ` 1364` ``` apply (simp only: ptV os) ``` lp15@64773 ` 1365` ``` using \p x = y\ \x \ V\ \x \ T\ apply blast ``` lp15@63301 ` 1366` ``` done ``` lp15@63301 ` 1367` ``` qed ``` lp15@63301 ` 1368` ``` with openin_subopen show ?thesis by blast ``` lp15@63301 ` 1369` ```qed ``` lp15@63301 ` 1370` lp15@63301 ` 1371` ```lemma covering_space_lift_unique_gen: ``` lp15@63301 ` 1372` ``` fixes f :: "'a::topological_space \ 'b::topological_space" ``` lp15@63301 ` 1373` ``` fixes g1 :: "'a \ 'c::real_normed_vector" ``` lp15@64773 ` 1374` ``` assumes cov: "covering_space c p S" ``` lp15@63301 ` 1375` ``` and eq: "g1 a = g2 a" ``` lp15@64773 ` 1376` ``` and f: "continuous_on T f" "f ` T \ S" ``` lp15@64773 ` 1377` ``` and g1: "continuous_on T g1" "g1 ` T \ c" ``` lp15@64773 ` 1378` ``` and fg1: "\x. x \ T \ f x = p(g1 x)" ``` lp15@64773 ` 1379` ``` and g2: "continuous_on T g2" "g2 ` T \ c" ``` lp15@64773 ` 1380` ``` and fg2: "\x. x \ T \ f x = p(g2 x)" ``` lp15@64773 ` 1381` ``` and u_compt: "U \ components T" and "a \ U" "x \ U" ``` lp15@63301 ` 1382` ``` shows "g1 x = g2 x" ``` lp15@63301 ` 1383` ```proof - ``` lp15@64773 ` 1384` ``` have "U \ T" by (rule in_components_subset [OF u_compt]) ``` lp15@65064 ` 1385` ``` define G12 where "G12 \ {x \ U. g1 x - g2 x = 0}" ``` lp15@64773 ` 1386` ``` have "connected U" by (rule in_components_connected [OF u_compt]) ``` lp15@64773 ` 1387` ``` have contu: "continuous_on U g1" "continuous_on U g2" ``` lp15@64773 ` 1388` ``` using \U \ T\ continuous_on_subset g1 g2 by blast+ ``` lp15@64773 ` 1389` ``` have o12: "openin (subtopology euclidean U) G12" ``` lp15@63301 ` 1390` ``` unfolding G12_def ``` lp15@63301 ` 1391` ``` proof (subst openin_subopen, clarify) ``` lp15@63301 ` 1392` ``` fix z ``` lp15@64773 ` 1393` ``` assume z: "z \ U" "g1 z - g2 z = 0" ``` lp15@63301 ` 1394` ``` obtain v w q where "g1 z \ v" and ocv: "openin (subtopology euclidean c) v" ``` lp15@64773 ` 1395` ``` and "p (g1 z) \ w" and osw: "openin (subtopology euclidean S) w" ``` lp15@63301 ` 1396` ``` and hom: "homeomorphism v w p q" ``` lp15@63301 ` 1397` ``` apply (rule_tac x = "g1 z" in covering_space_local_homeomorphism [OF cov]) ``` lp15@64773 ` 1398` ``` using \U \ T\ \z \ U\ g1(2) apply blast+ ``` lp15@63301 ` 1399` ``` done ``` lp15@63301 ` 1400` ``` have "g2 z \ v" using \g1 z \ v\ z by auto ``` lp15@66884 ` 1401` ``` have gg: "U \ g -` v = U \ g -` (v \ g ` U)" for g ``` lp15@63301 ` 1402` ``` by auto ``` lp15@64773 ` 1403` ``` have "openin (subtopology euclidean (g1 ` U)) (v \ g1 ` U)" ``` lp15@64773 ` 1404` ``` using ocv \U \ T\ g1 by (fastforce simp add: openin_open) ``` lp15@66884 ` 1405` ``` then have 1: "openin (subtopology euclidean U) (U \ g1 -` v)" ``` lp15@63301 ` 1406` ``` unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format]) ``` lp15@64773 ` 1407` ``` have "openin (subtopology euclidean (g2 ` U)) (v \ g2 ` U)" ``` lp15@64773 ` 1408` ``` using ocv \U \ T\ g2 by (fastforce simp add: openin_open) ``` lp15@66884 ` 1409` ``` then have 2: "openin (subtopology euclidean U) (U \ g2 -` v)" ``` lp15@63301 ` 1410` ``` unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format]) ``` lp15@66884 ` 1411` ``` show "\T. openin (subtopology euclidean U) T \ z \ T \ T \ {z \ U. g1 z - g2 z = 0}" ``` lp15@63301 ` 1412` ``` using z ``` lp15@66884 ` 1413` ``` apply (rule_tac x = "(U \ g1 -` v) \ (U \ g2 -` v)" in exI) ``` lp15@63301 ` 1414` ``` apply (intro conjI) ``` lp15@63301 ` 1415` ``` apply (rule openin_Int [OF 1 2]) ``` lp15@63301 ` 1416` ``` using \g1 z \ v\ \g2 z \ v\ apply (force simp:, clarify) ``` lp15@64773 ` 1417` ``` apply (metis \U \ T\ subsetD eq_iff_diff_eq_0 fg1 fg2 hom homeomorphism_def) ``` lp15@63301 ` 1418` ``` done ``` lp15@63301 ` 1419` ``` qed ``` lp15@64773 ` 1420` ``` have c12: "closedin (subtopology euclidean U) G12" ``` lp15@63301 ` 1421` ``` unfolding G12_def ``` lp15@63301 ` 1422` ``` by (intro continuous_intros continuous_closedin_preimage_constant contu) ``` lp15@64773 ` 1423` ``` have "G12 = {} \ G12 = U" ``` lp15@64773 ` 1424` ``` by (intro connected_clopen [THEN iffD1, rule_format] \connected U\ conjI o12 c12) ``` lp15@64773 ` 1425` ``` with eq \a \ U\ have "\x. x \ U \ g1 x - g2 x = 0" by (auto simp: G12_def) ``` lp15@63301 ` 1426` ``` then show ?thesis ``` lp15@64773 ` 1427` ``` using \x \ U\ by force ``` lp15@63301 ` 1428` ```qed ``` lp15@63301 ` 1429` lp15@63301 ` 1430` ```proposition covering_space_lift_unique: ``` lp15@63301 ` 1431` ``` fixes f :: "'a::topological_space \ 'b::topological_space" ``` lp15@63301 ` 1432` ``` fixes g1 :: "'a \ 'c::real_normed_vector" ``` lp15@64773 ` 1433` ``` assumes "covering_space c p S" ``` lp15@63301 ` 1434` ``` "g1 a = g2 a" ``` lp15@64773 ` 1435` ``` "continuous_on T f" "f ` T \ S" ``` lp15@64773 ` 1436` ``` "continuous_on T g1" "g1 ` T \ c" "\x. x \ T \ f x = p(g1 x)" ``` lp15@64773 ` 1437` ``` "continuous_on T g2" "g2 ` T \ c" "\x. x \ T \ f x = p(g2 x)" ``` lp15@64773 ` 1438` ``` "connected T" "a \ T" "x \ T" ``` lp15@63301 ` 1439` ``` shows "g1 x = g2 x" ``` lp15@64773 ` 1440` ```using covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv by blast ``` lp15@63301 ` 1441` lp15@64791 ` 1442` ```lemma covering_space_locally: ``` lp15@64791 ` 1443` ``` fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" ``` lp15@64791 ` 1444` ``` assumes loc: "locally \ C" and cov: "covering_space C p S" ``` lp15@64791 ` 1445` ``` and pim: "\T. \T \ C; \ T\ \ \(p ` T)" ``` lp15@64791 ` 1446` ``` shows "locally \ S" ``` lp15@64791 ` 1447` ```proof - ``` lp15@64791 ` 1448` ``` have "locally \ (p ` C)" ``` lp15@64791 ` 1449` ``` apply (rule locally_open_map_image [OF loc]) ``` lp15@64791 ` 1450` ``` using cov covering_space_imp_continuous apply blast ``` lp15@64791 ` 1451` ``` using cov covering_space_imp_surjective covering_space_open_map apply blast ``` lp15@64791 ` 1452` ``` by (simp add: pim) ``` lp15@64791 ` 1453` ``` then show ?thesis ``` lp15@64791 ` 1454` ``` using covering_space_imp_surjective [OF cov] by metis ``` lp15@64791 ` 1455` ```qed ``` lp15@64791 ` 1456` lp15@64791 ` 1457` lp15@64791 ` 1458` ```proposition covering_space_locally_eq: ``` lp15@64791 ` 1459` ``` fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" ``` lp15@64791 ` 1460` ``` assumes cov: "covering_space C p S" ``` lp15@64791 ` 1461` ``` and pim: "\T. \T \ C; \ T\ \ \(p ` T)" ``` lp15@64791 ` 1462` ``` and qim: "\q U. \U \ S; continuous_on U q; \ U\ \ \(q ` U)" ``` lp15@64791 ` 1463` ``` shows "locally \ S \ locally \ C" ``` lp15@64791 ` 1464` ``` (is "?lhs = ?rhs") ``` lp15@64791 ` 1465` ```proof ``` lp15@64791 ` 1466` ``` assume L: ?lhs ``` lp15@64791 ` 1467` ``` show ?rhs ``` lp15@64791 ` 1468` ``` proof (rule locallyI) ``` lp15@64791 ` 1469` ``` fix V x ``` lp15@64791 ` 1470` ``` assume V: "openin (subtopology euclidean C) V" and "x \ V" ``` lp15@64791 ` 1471` ``` have "p x \ p ` C" ``` lp15@64791 ` 1472` ``` by (metis IntE V \x \ V\ imageI openin_open) ``` lp15@64791 ` 1473` ``` then obtain T \ where "p x \ T" ``` lp15@64791 ` 1474` ``` and opeT: "openin (subtopology euclidean S) T" ``` lp15@66884 ` 1475` ``` and veq: "\\ = C \ p -` T" ``` lp15@64791 ` 1476` ``` and ope: "\U\\. openin (subtopology euclidean C) U" ``` lp15@64791 ` 1477` ``` and hom: "\U\\. \q. homeomorphism U T p q" ``` lp15@64791 ` 1478` ``` using cov unfolding covering_space_def by (blast intro: that) ``` lp15@64791 ` 1479` ``` have "x \ \\" ``` lp15@64791 ` 1480` ``` using V veq \p x \ T\ \x \ V\ openin_imp_subset by fastforce ``` lp15@64791 ` 1481` ``` then obtain U where "x \ U" "U \ \" ``` lp15@64791 ` 1482` ``` by blast ``` lp15@64791 ` 1483` ``` then obtain q where opeU: "openin (subtopology euclidean C) U" and q: "homeomorphism U T p q" ``` lp15@64791 ` 1484` ``` using ope hom by blast ``` lp15@64791 ` 1485` ``` with V have "openin (subtopology euclidean C) (U \ V)" ``` lp15@64791 ` 1486` ``` by blast ``` lp15@64791 ` 1487` ``` then have UV: "openin (subtopology euclidean S) (p ` (U \ V))" ``` lp15@64791 ` 1488` ``` using cov covering_space_open_map by blast ``` lp15@64791 ` 1489` ``` obtain W W' where opeW: "openin (subtopology euclidean S) W" and "\ W'" "p x \ W" "W \ W'" and W'sub: "W' \ p ` (U \ V)" ``` lp15@64791 ` 1490` ``` using locallyE [OF L UV] \x \ U\ \x \ V\ by blast ``` lp15@64791 ` 1491` ``` then have "W \ T" ``` lp15@64791 ` 1492` ``` by (metis Int_lower1 q homeomorphism_image1 image_Int_subset order_trans) ``` lp15@64791 ` 1493` ``` show "\U Z. openin (subtopology euclidean C) U \ ``` lp15@64791 ` 1494` ``` \ Z \ x \ U \ U \ Z \ Z \ V" ``` lp15@64791 ` 1495` ``` proof (intro exI conjI) ``` lp15@64791 ` 1496` ``` have "openin (subtopology euclidean T) W" ``` lp15@64791 ` 1497` ``` by (meson opeW opeT openin_imp_subset openin_subset_trans \W \ T\) ``` lp15@64791 ` 1498` ``` then have "openin (subtopology euclidean U) (q ` W)" ``` lp15@64791 ` 1499` ``` by (meson homeomorphism_imp_open_map homeomorphism_symD q) ``` lp15@64791 ` 1500` ``` then show "openin (subtopology euclidean C) (q ` W)" ``` lp15@64791 ` 1501` ``` using opeU openin_trans by blast ``` lp15@64791 ` 1502` ``` show "\ (q ` W')" ``` lp15@64791 ` 1503` ``` by (metis (mono_tags, lifting) Int_subset_iff UV W'sub \\ W'\ continuous_on_subset dual_order.trans homeomorphism_def image_Int_subset openin_imp_subset q qim) ``` lp15@64791 ` 1504` ``` show "x \ q ` W" ``` lp15@64791 ` 1505` ``` by (metis \p x \ W\ \x \ U\ homeomorphism_def imageI q) ``` lp15@64791 ` 1506` ``` show "q ` W \ q ` W'" ``` lp15@64791 ` 1507` ``` using \W \ W'\ by blast ``` lp15@64791 ` 1508` ``` have "W' \ p ` V" ``` lp15@64791 ` 1509` ``` using W'sub by blast ``` lp15@64791 ` 1510` ``` then show "q ` W' \ V" ``` lp15@64791 ` 1511` ``` using W'sub homeomorphism_apply1 [OF q] by auto ``` lp15@64791 ` 1512` ``` qed ``` lp15@64791 ` 1513` ``` qed ``` lp15@64791 ` 1514` ```next ``` lp15@64791 ` 1515` ``` assume ?rhs ``` lp15@64791 ` 1516` ``` then show ?lhs ``` lp15@64791 ` 1517` ``` using cov covering_space_locally pim by blast ``` lp15@64791 ` 1518` ```qed ``` lp15@64791 ` 1519` lp15@64791 ` 1520` ```lemma covering_space_locally_compact_eq: ``` lp15@64791 ` 1521` ``` fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" ``` lp15@64791 ` 1522` ``` assumes "covering_space C p S" ``` lp15@64791 ` 1523` ``` shows "locally compact S \ locally compact C" ``` lp15@64791 ` 1524` ``` apply (rule covering_space_locally_eq [OF assms]) ``` lp15@64791 ` 1525` ``` apply (meson assms compact_continuous_image continuous_on_subset covering_space_imp_continuous) ``` lp15@64791 ` 1526` ``` using compact_continuous_image by blast ``` lp15@64791 ` 1527` lp15@64791 ` 1528` ```lemma covering_space_locally_connected_eq: ``` lp15@64791 ` 1529` ``` fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" ``` lp15@64791 ` 1530` ``` assumes "covering_space C p S" ``` lp15@64791 ` 1531` ``` shows "locally connected S \ locally connected C" ``` lp15@64791 ` 1532` ``` apply (rule covering_space_locally_eq [OF assms]) ``` lp15@64791 ` 1533` ``` apply (meson connected_continuous_image assms continuous_on_subset covering_space_imp_continuous) ``` lp15@64791 ` 1534` ``` using connected_continuous_image by blast ``` lp15@64791 ` 1535` lp15@64791 ` 1536` ```lemma covering_space_locally_path_connected_eq: ``` lp15@64791 ` 1537` ``` fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" ``` lp15@64791 ` 1538` ``` assumes "covering_space C p S" ``` lp15@64791 ` 1539` ``` shows "locally path_connected S \ locally path_connected C" ``` lp15@64791 ` 1540` ``` apply (rule covering_space_locally_eq [OF assms]) ``` lp15@64791 ` 1541` ``` apply (meson path_connected_continuous_image assms continuous_on_subset covering_space_imp_continuous) ``` lp15@64791 ` 1542` ``` using path_connected_continuous_image by blast ``` lp15@64791 ` 1543` lp15@64791 ` 1544` lp15@64791 ` 1545` ```lemma covering_space_locally_compact: ``` lp15@64791 ` 1546` ``` fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" ``` lp15@64791 ` 1547` ``` assumes "locally compact C" "covering_space C p S" ``` lp15@64791 ` 1548` ``` shows "locally compact S" ``` lp15@64791 ` 1549` ``` using assms covering_space_locally_compact_eq by blast ``` lp15@64791 ` 1550` lp15@64791 ` 1551` lp15@64791 ` 1552` ```lemma covering_space_locally_connected: ``` lp15@64791 ` 1553` ``` fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" ``` lp15@64791 ` 1554` ``` assumes "locally connected C" "covering_space C p S" ``` lp15@64791 ` 1555` ``` shows "locally connected S" ``` lp15@64791 ` 1556` ``` using assms covering_space_locally_connected_eq by blast ``` lp15@64791 ` 1557` lp15@64791 ` 1558` ```lemma covering_space_locally_path_connected: ``` lp15@64791 ` 1559` ``` fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" ``` lp15@64791 ` 1560` ``` assumes "locally path_connected C" "covering_space C p S" ``` lp15@64791 ` 1561` ``` shows "locally path_connected S" ``` lp15@64791 ` 1562` ``` using assms covering_space_locally_path_connected_eq by blast ``` lp15@64791 ` 1563` lp15@64792 ` 1564` ```proposition covering_space_lift_homotopy: ``` lp15@64792 ` 1565` ``` fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" ``` lp15@64792 ` 1566` ``` and h :: "real \ 'c::real_normed_vector \ 'b" ``` lp15@64792 ` 1567` ``` assumes cov: "covering_space C p S" ``` lp15@64792 ` 1568` ``` and conth: "continuous_on ({0..1} \ U) h" ``` lp15@64792 ` 1569` ``` and him: "h ` ({0..1} \ U) \ S" ``` lp15@64792 ` 1570` ``` and heq: "\y. y \ U \ h (0,y) = p(f y)" ``` lp15@64792 ` 1571` ``` and contf: "continuous_on U f" and fim: "f ` U \ C" ``` lp15@64792 ` 1572` ``` obtains k where "continuous_on ({0..1} \ U) k" ``` lp15@64792 ` 1573` ``` "k ` ({0..1} \ U) \ C" ``` lp15@64792 ` 1574` ``` "\y. y \ U \ k(0, y) = f y" ``` lp15@64792 ` 1575` ``` "\z. z \ {0..1} \ U \ h z = p(k z)" ``` lp15@64792 ` 1576` ```proof - ``` lp15@64792 ` 1577` ``` have "\V k. openin (subtopology euclidean U) V \ y \ V \ ``` lp15@64792 ` 1578` ``` continuous_on ({0..1} \ V) k \ k ` ({0..1} \ V) \ C \ ``` lp15@64792 ` 1579` ``` (\z \ V. k(0, z) = f z) \ (\z \ {0..1} \ V. h z = p(k z))" ``` lp15@64792 ` 1580` ``` if "y \ U" for y ``` lp15@64792 ` 1581` ``` proof - ``` lp15@64792 ` 1582` ``` obtain UU where UU: "\s. s \ S \ s \ (UU s) \ openin (subtopology euclidean S) (UU s) \ ``` lp15@66884 ` 1583` ``` (\\. \\ = C \ p -` UU s \ ``` lp15@64792 ` 1584` ``` (\U \ \. openin (subtopology euclidean C) U) \ ``` lp15@64792 ` 1585` ``` pairwise disjnt \ \ ``` lp15@64792 ` 1586` ``` (\U \ \. \q. homeomorphism U (UU s) p q))" ``` lp15@64792 ` 1587` ``` using cov unfolding covering_space_def by (metis (mono_tags)) ``` lp15@64792 ` 1588` ``` then have ope: "\s. s \ S \ s \ (UU s) \ openin (subtopology euclidean S) (UU s)" ``` lp15@64792 ` 1589` ``` by blast ``` lp15@64792 ` 1590` ``` have "\k n i. open k \ open n \ ``` lp15@64792 ` 1591` ``` t \ k \ y \ n \ i \ S \ h ` (({0..1} \ k) \ (U \ n)) \ UU i" if "t \ {0..1}" for t ``` lp15@64792 ` 1592` ``` proof - ``` lp15@64792 ` 1593` ``` have hinS: "h (t, y) \ S" ``` lp15@64792 ` 1594` ``` using \y \ U\ him that by blast ``` lp15@66884 ` 1595` ``` then have "(t,y) \ ({0..1} \ U) \ h -` UU(h(t, y))" ``` lp15@64792 ` 1596` ``` using \y \ U\ \t \ {0..1}\ by (auto simp: ope) ``` lp15@66884 ` 1597` ``` moreover have ope_01U: "openin (subtopology euclidean ({0..1} \ U)) (({0..1} \ U) \ h -` UU(h(t, y)))" ``` lp15@64792 ` 1598` ``` using hinS ope continuous_on_open_gen [OF him] conth by blast ``` lp15@64792 ` 1599` ``` ultimately obtain V W where opeV: "open V" and "t \ {0..1} \ V" "t \ {0..1} \ V" ``` lp15@64792 ` 1600` ``` and opeW: "open W" and "y \ U" "y \ W" ``` lp15@66884 ` 1601` ``` and VW: "({0..1} \ V) \ (U \ W) \ (({0..1} \ U) \ h -` UU(h(t, y)))" ``` lp15@64792 ` 1602` ``` by (rule Times_in_interior_subtopology) (auto simp: openin_open) ``` lp15@64792 ` 1603` ``` then show ?thesis ``` lp15@64792 ` 1604` ``` using hinS by blast ``` lp15@64792 ` 1605` ``` qed ``` lp15@64792 ` 1606` ``` then obtain K NN X where ``` lp15@64792 ` 1607` ``` K: "\t. t \ {0..1} \ open (K t)" ``` lp15@64792 ` 1608` ``` and NN: "\t. t \ {0..1} \ open (NN t)" ``` lp15@64792 ` 1609` ``` and inUS: "\t. t \ {0..1} \ t \ K t \ y \ NN t \ X t \ S" ``` lp15@64792 ` 1610` ``` and him: "\t. t \ {0..1} \ h ` (({0..1} \ K t) \ (U \ NN t)) \ UU (X t)" ``` lp15@64792 ` 1611` ``` by (metis (mono_tags)) ``` lp15@64792 ` 1612` ``` obtain \ where "\ \ ((\i. K i \ NN i)) ` {0..1}" "finite \" "{0::real..1} \ {y} \ \\" ``` lp15@64792 ` 1613` ``` proof (rule compactE) ``` lp15@64792 ` 1614` ``` show "compact ({0::real..1} \ {y})" ``` lp15@64792 ` 1615` ``` by (simp add: compact_Times) ``` lp15@64792 ` 1616` ``` show "{0..1} \ {y} \ (\i\{0..1}. K i \ NN i)" ``` lp15@64792 ` 1617` ``` using K inUS by auto ``` lp15@64792 ` 1618` ``` show "\B. B \ (\i. K i \ NN i) ` {0..1} \ open B" ``` lp15@64792 ` 1619` ``` using K NN by (auto simp: open_Times) ``` lp15@64792 ` 1620` ``` qed blast ``` lp15@64792 ` 1621` ``` then obtain tk where "tk \ {0..1}" "finite tk" ``` lp15@64792 ` 1622` ``` and tk: "{0::real..1} \ {y} \ (\i \ tk. K i \ NN i)" ``` lp15@64792 ` 1623` ``` by (metis (no_types, lifting) finite_subset_image) ``` lp15@64792 ` 1624` ``` then have "tk \ {}" ``` lp15@64792 ` 1625` ``` by auto ``` lp15@64792 ` 1626` ``` define n where "n = INTER tk NN" ``` lp15@64792 ` 1627` ``` have "y \ n" "open n" ``` lp15@64792 ` 1628` ``` using inUS NN \tk \ {0..1}\ \finite tk\ ``` lp15@64792 ` 1629` ``` by (auto simp: n_def open_INT subset_iff) ``` lp15@64792 ` 1630` ``` obtain \ where "0 < \" and \: "\T. \T \ {0..1}; diameter T < \\ \ \B\K ` tk. T \ B" ``` lp15@64792 ` 1631` ``` proof (rule Lebesgue_number_lemma [of "{0..1}" "K ` tk"]) ``` lp15@64792 ` 1632` ``` show "K ` tk \ {}" ``` lp15@64792 ` 1633` ``` using \tk \ {}\ by auto ``` lp15@64792 ` 1634` ``` show "{0..1} \ UNION tk K" ``` lp15@64792 ` 1635` ``` using tk by auto ``` lp15@64792 ` 1636` ``` show "\B. B \ K ` tk \ open B" ``` lp15@64792 ` 1637` ``` using \tk \ {0..1}\ K by auto ``` lp15@64792 ` 1638` ``` qed auto ``` lp15@64792 ` 1639` ``` obtain N::nat where N: "N > 1 / \" ``` lp15@64792 ` 1640` ``` using reals_Archimedean2 by blast ``` lp15@64792 ` 1641` ``` then have "N > 0" ``` lp15@64792 ` 1642` ``` using \0 < \\ order.asym by force ``` lp15@64792 ` 1643` ``` have *: "\V k. openin (subtopology euclidean U) V \ y \ V \ ``` lp15@64792 ` 1644` ``` continuous_on ({0..of_nat n / N} \ V) k \ ``` lp15@64792 ` 1645` ``` k ` ({0..of_nat n / N} \ V) \ C \ ``` lp15@64792 ` 1646` ``` (\z\V. k (0, z) = f z) \ ``` lp15@64792 ` 1647` ``` (\z\{0..of_nat n / N} \ V. h z = p (k z))" if "n \ N" for n ``` lp15@64792 ` 1648` ``` using that ``` lp15@64792 ` 1649` ``` proof (induction n) ``` lp15@64792 ` 1650` ``` case 0 ``` lp15@64792 ` 1651` ``` show ?case ``` lp15@64792 ` 1652` ``` apply (rule_tac x=U in exI) ``` lp15@64792 ` 1653` ``` apply (rule_tac x="f \ snd" in exI) ``` lp15@64792 ` 1654` ``` apply (intro conjI \y \ U\ continuous_intros continuous_on_subset [OF contf]) ``` lp15@64792 ` 1655` ``` using fim apply (auto simp: heq) ``` lp15@64792 ` 1656` ``` done ``` lp15@64792 ` 1657` ``` next ``` lp15@64792 ` 1658` ``` case (Suc n) ``` lp15@64792 ` 1659` ``` then obtain V k where opeUV: "openin (subtopology euclidean U) V" ``` lp15@64792 ` 1660` ``` and "y \ V" ``` lp15@64792 ` 1661` ``` and contk: "continuous_on ({0..real n / real N} \ V) k" ``` lp15@64792 ` 1662` ``` and kim: "k ` ({0..real n / real N} \ V) \ C" ``` lp15@64792 ` 1663` ``` and keq: "\z. z \ V \ k (0, z) = f z" ``` lp15@64792 ` 1664` ``` and heq: "\z. z \ {0..real n / real N} \ V \ h z = p (k z)" ``` lp15@64792 ` 1665` ``` using Suc_leD by auto ``` lp15@64792 ` 1666` ``` have "n \ N" ``` lp15@64792 ` 1667` ``` using Suc.prems by auto ``` lp15@64792 ` 1668` ``` obtain t where "t \ tk" and t: "{real n / real N .. (1 + real n) / real N} \ K t" ``` lp15@64792 ` 1669` ``` proof (rule bexE [OF \]) ``` lp15@64792 ` 1670` ``` show "{real n / real N .. (1 + real n) / real N} \ {0..1}" ``` lp15@64792 ` 1671` ``` using Suc.prems by (auto simp: divide_simps algebra_simps) ``` lp15@64792 ` 1672` ``` show diameter_less: "diameter {real n / real N .. (1 + real n) / real N} < \" ``` lp15@64792 ` 1673` ``` using \0 < \\ N by (auto simp: divide_simps algebra_simps) ``` lp15@64792 ` 1674` ``` qed blast ``` lp15@64792 ` 1675` ``` have t01: "t \ {0..1}" ``` lp15@64792 ` 1676` ``` using \t \ tk\ \tk \ {0..1}\ by blast ``` lp15@66884 ` 1677` ``` obtain \ where \: "\\ = C \ p -` UU (X t)" ``` lp15@64792 ` 1678` ``` and opeC: "\U. U \ \ \ openin (subtopology euclidean C) U" ``` lp15@64792 ` 1679` ``` and "pairwise disjnt \" ``` lp15@64792 ` 1680` ``` and homuu: "\U. U \ \ \ \q. homeomorphism U (UU (X t)) p q" ``` lp15@64792 ` 1681` ``` using inUS [OF t01] UU by meson ``` lp15@64792 ` 1682` ``` have n_div_N_in: "real n / real N \ {real n / real N .. (1 + real n) / real N}" ``` lp15@64792 ` 1683` ``` using N by (auto simp: divide_simps algebra_simps) ``` lp15@64792 ` 1684` ``` with t have nN_in_kkt: "real n / real N \ K t" ``` lp15@64792 ` 1685` ``` by blast ``` lp15@66884 ` 1686` ``` have "k (real n / real N, y) \ C \ p -` UU (X t)" ``` lp15@64792 ` 1687` ``` proof (simp, rule conjI) ``` lp15@64792 ` 1688` ``` show "k (real n / real N, y) \ C" ``` lp15@64792 ` 1689` ``` using \y \ V\ kim keq by force ``` lp15@64792 ` 1690` ``` have "p (k (real n / real N, y)) = h (real n / real N, y)" ``` lp15@64792 ` 1691` ``` by (simp add: \y \ V\ heq) ``` lp15@64792 ` 1692` ``` also have "... \ h ` (({0..1} \ K t) \ (U \ NN t))" ``` lp15@64792 ` 1693` ``` apply (rule imageI) ``` lp15@64792 ` 1694` ``` using \y \ V\ t01 \n \ N\ ``` lp15@64792 ` 1695` ``` apply (simp add: nN_in_kkt \y \ U\ inUS divide_simps) ``` lp15@64792 ` 1696` ``` done ``` lp15@64792 ` 1697` ``` also have "... \ UU (X t)" ``` lp15@64792 ` 1698` ``` using him t01 by blast ``` lp15@64792 ` 1699` ``` finally show "p (k (real n / real N, y)) \ UU (X t)" . ``` lp15@64792 ` 1700` ``` qed ``` lp15@66884 ` 1701` ``` with \ have "k (real n / real N, y) \ \\" ``` lp15@66884 ` 1702` ``` by blast ``` lp15@64792 ` 1703` ``` then obtain W where W: "k (real n / real N, y) \ W" and "W \ \" ``` lp15@64792 ` 1704` ``` by blast ``` lp15@64792 ` 1705` ``` then obtain p' where opeC': "openin (subtopology euclidean C) W" ``` lp15@64792 ` 1706` ``` and hom': "homeomorphism W (UU (X t)) p p'" ``` lp15@64792 ` 1707` ``` using homuu opeC by blast ``` lp15@64792 ` 1708` ``` then have "W \ C" ``` lp15@64792 ` 1709` ``` using openin_imp_subset by blast ``` lp15@64792 ` 1710` ``` define W' where "W' = UU(X t)" ``` lp15@66884 ` 1711` ``` have opeVW: "openin (subtopology euclidean V) (V \ (k \ Pair (n / N)) -` W)" ``` lp15@64792 ` 1712` ``` apply (rule continuous_openin_preimage [OF _ _ opeC']) ``` lp15@64792 ` 1713` ``` apply (intro continuous_intros continuous_on_subset [OF contk]) ``` lp15@64792 ` 1714` ``` using kim apply (auto simp: \y \ V\ W) ``` lp15@64792 ` 1715` ``` done ``` lp15@64792 ` 1716` ``` obtain N' where opeUN': "openin (subtopology euclidean U) N'" ``` lp15@64792 ` 1717` ``` and "y \ N'" and kimw: "k ` ({(real n / real N)} \ N') \ W" ``` lp15@66884 ` 1718` ``` apply (rule_tac N' = "(V \ (k \ Pair (n / N)) -` W)" in that) ``` lp15@64792 ` 1719` ``` apply (fastforce simp: \y \ V\ W intro!: openin_trans [OF opeVW opeUV])+ ``` lp15@64792 ` 1720` ``` done ``` lp15@64792 ` 1721` ``` obtain Q Q' where opeUQ: "openin (subtopology euclidean U) Q" ``` lp15@64792 ` 1722` ``` and cloUQ': "closedin (subtopology euclidean U) Q'" ``` lp15@64792 ` 1723` ``` and "y \ Q" "Q \ Q'" ``` lp15@64792 ` 1724` ``` and Q': "Q' \ (U \ NN(t)) \ N' \ V" ``` lp15@64792 ` 1725` ``` proof - ``` lp15@64792 ` 1726` ``` obtain VO VX where "open VO" "open VX" and VO: "V = U \ VO" and VX: "N' = U \ VX" ``` lp15@64792 ` 1727` ``` using opeUV opeUN' by (auto simp: openin_open) ``` lp15@64792 ` 1728` ``` then have "open (NN(t) \ VO \ VX)" ``` lp15@64792 ` 1729` ``` using NN t01 by blast ``` lp15@64792 ` 1730` ``` then obtain e where "e > 0" and e: "cball y e \ NN(t) \ VO \ VX" ``` lp15@64792 ` 1731` ``` by (metis Int_iff \N' = U \ VX\ \V = U \ VO\ \y \ N'\ \y \ V\ inUS open_contains_cball t01) ``` lp15@64792 ` 1732` ``` show ?thesis ``` lp15@64792 ` 1733` ``` proof ``` lp15@64792 ` 1734` ``` show "openin (subtopology euclidean U) (U \ ball y e)" ``` lp15@64792 ` 1735` ``` by blast ``` lp15@64792 ` 1736` ``` show "closedin (subtopology euclidean U) (U \ cball y e)" ``` lp15@64792 ` 1737` ``` using e by (auto simp: closedin_closed) ``` lp15@64792 ` 1738` ``` qed (use \y \ U\ \e > 0\ VO VX e in auto) ``` lp15@64792 ` 1739` ``` qed ``` lp15@64792 ` 1740` ``` then have "y \ Q'" "Q \ (U \ NN(t)) \ N' \ V" ``` lp15@64792 ` 1741` ``` by blast+ ``` lp15@64792 ` 1742` ``` have neq: "{0..real n / real N} \ {real n / real N..(1 + real n) / real N} = {0..(1 + real n) / real N}" ``` lp15@64792 ` 1743` ``` apply (auto simp: divide_simps) ``` lp15@64792 ` 1744` ``` by (metis mult_zero_left of_nat_0_le_iff of_nat_0_less_iff order_trans real_mult_le_cancel_iff1) ``` lp15@64792 ` 1745` ``` then have neqQ': "{0..real n / real N} \ Q' \ {real n / real N..(1 + real n) / real N} \ Q' = {0..(1 + real n) / real N} \ Q'" ``` lp15@64792 ` 1746` ``` by blast ``` lp15@64792 ` 1747` ``` have cont: "continuous_on ({0..(1 + real n) / real N} \ Q') ``` lp15@64792 ` 1748` ``` (\x. if x \ {0..real n / real N} \ Q' then k x else (p' \ h) x)" ``` lp15@64792 ` 1749` ``` unfolding neqQ' [symmetric] ``` lp15@64792 ` 1750` ``` proof (rule continuous_on_cases_local, simp_all add: neqQ' del: comp_apply) ``` lp15@64792 ` 1751` ``` show "closedin (subtopology euclidean ({0..(1 + real n) / real N} \ Q')) ``` lp15@64792 ` 1752` ``` ({0..real n / real N} \ Q')" ``` lp15@64792 ` 1753` ``` apply (simp add: closedin_closed) ``` lp15@64792 ` 1754` ``` apply (rule_tac x="{0 .. real n / real N} \ UNIV" in exI) ``` lp15@64792 ` 1755` ``` using n_div_N_in apply (auto simp: closed_Times) ``` lp15@64792 ` 1756` ``` done ``` lp15@64792 ` 1757` ``` show "closedin (subtopology euclidean ({0..(1 + real n) / real N} \ Q')) ``` lp15@64792 ` 1758` ``` ({real n / real N..(1 + real n) / real N} \ Q')" ``` lp15@64792 ` 1759` ``` apply (simp add: closedin_closed) ``` lp15@64792 ` 1760` ``` apply (rule_tac x="{real n / real N .. (1 + real n) / real N} \ UNIV" in exI) ``` lp15@64792 ` 1761` ``` apply (auto simp: closed_Times) ``` lp15@64792 ` 1762` ``` by (meson divide_nonneg_nonneg of_nat_0_le_iff order_trans) ``` lp15@64792 ` 1763` ``` show "continuous_on ({0..real n / real N} \ Q') k" ``` lp15@64792 ` 1764` ``` apply (rule continuous_on_subset [OF contk]) ``` lp15@64792 ` 1765` ``` using Q' by auto ``` lp15@64792 ` 1766` ``` have "continuous_on ({real n / real N..(1 + real n) / real N} \ Q') h" ``` lp15@64792 ` 1767` ``` proof (rule continuous_on_subset [OF conth]) ``` lp15@64792 ` 1768` ``` show "{real n / real N..(1 + real n) / real N} \ Q' \ {0..1} \ U" ``` lp15@64792 ` 1769` ``` using \N > 0\ ``` lp15@64792 ` 1770` ``` apply auto ``` lp15@64792 ` 1771` ``` apply (meson divide_nonneg_nonneg of_nat_0_le_iff order_trans) ``` lp15@64792 ` 1772` ``` using Suc.prems order_trans apply fastforce ``` lp15@64792 ` 1773` ``` apply (metis IntE cloUQ' closedin_closed) ``` lp15@64792 ` 1774` ``` done ``` lp15@64792 ` 1775` ``` qed ``` lp15@64792 ` 1776` ``` moreover have "continuous_on (h ` ({real n / real N..(1 + real n) / real N} \ Q')) p'" ``` lp15@64792 ` 1777` ``` proof (rule continuous_on_subset [OF homeomorphism_cont2 [OF hom']]) ``` lp15@64792 ` 1778` ``` have "h ` ({real n / real N..(1 + real n) / real N} \ Q') \ h ` (({0..1} \ K t) \ (U \ NN t))" ``` lp15@64792 ` 1779` ``` apply (rule image_mono) ``` lp15@64792 ` 1780` ``` using \0 < \\ \N > 0\ Suc.prems apply auto ``` lp15@64792 ` 1781` ``` apply (meson divide_nonneg_nonneg of_nat_0_le_iff order_trans) ``` lp15@64792 ` 1782` ``` using Suc.prems order_trans apply fastforce ``` lp15@64792 ` 1783` ``` using t Q' apply auto ``` lp15@64792 ` 1784` ``` done ``` lp15@64792 ` 1785` ``` with him show "h ` ({real n / real N..(1 + real n) / real N} \ Q') \ UU (X t)" ``` lp15@64792 ` 1786` ``` using t01 by blast ``` lp15@64792 ` 1787` ``` qed ``` lp15@64792 ` 1788` ``` ultimately show "continuous_on ({real n / real N..(1 + real n) / real N} \ Q') (p' \ h)" ``` lp15@64792 ` 1789` ``` by (rule continuous_on_compose) ``` lp15@64792 ` 1790` ``` have "k (real n / real N, b) = p' (h (real n / real N, b))" if "b \ Q'" for b ``` lp15@64792 ` 1791` ``` proof - ``` lp15@64792 ` 1792` ``` have "k (real n / real N, b) \ W" ``` lp15@64792 ` 1793` ``` using that Q' kimw by force ``` lp15@64792 ` 1794` ``` then have "k (real n / real N, b) = p' (p (k (real n / real N, b)))" ``` lp15@64792 ` 1795` ``` by (simp add: homeomorphism_apply1 [OF hom']) ``` lp15@64792 ` 1796` ``` then show ?thesis ``` lp15@64792 ` 1797` ``` using Q' that by (force simp: heq) ``` lp15@64792 ` 1798` ``` qed ``` lp15@64792 ` 1799` ``` then show "\x. x \ {real n / real N..(1 + real n) / real N} \ Q' \ ``` lp15@64792 ` 1800` ``` x \ {0..real n / real N} \ Q' \ k x = (p' \ h) x" ``` lp15@64792 ` 1801` ``` by auto ``` lp15@64792 ` 1802` ``` qed ``` lp15@64792 ` 1803` ``` have h_in_UU: "h (x, y) \ UU (X t)" if "y \ Q" "\ x \ real n / real N" "0 \ x" "x \ (1 + real n) / real N" for x y ``` lp15@64792 ` 1804` ``` proof - ``` lp15@64792 ` 1805` ``` have "x \ 1" ``` lp15@64792 ` 1806` ``` using Suc.prems that order_trans by force ``` lp15@64792 ` 1807` ``` moreover have "x \ K t" ``` lp15@64792 ` 1808` ``` by (meson atLeastAtMost_iff le_less not_le subset_eq t that) ``` lp15@64792 ` 1809` ``` moreover have "y \ U" ``` lp15@64792 ` 1810` ``` using \y \ Q\ opeUQ openin_imp_subset by blast ``` lp15@64792 ` 1811` ``` moreover have "y \ NN t" ``` lp15@64792 ` 1812` ``` using Q' \Q \ Q'\ \y \ Q\ by auto ``` lp15@64792 ` 1813` ``` ultimately have "(x, y) \ (({0..1} \ K t) \ (U \ NN t))" ``` lp15@64792 ` 1814` ``` using that by auto ``` lp15@64792 ` 1815` ``` then have "h (x, y) \ h ` (({0..1} \ K t) \ (U \ NN t))" ``` lp15@64792 ` 1816` ``` by blast ``` lp15@64792 ` 1817` ``` also have "... \ UU (X t)" ``` lp15@64792 ` 1818` ``` by (metis him t01) ``` lp15@64792 ` 1819` ``` finally show ?thesis . ``` lp15@64792 ` 1820` ``` qed ``` lp15@64792 ` 1821` ``` let ?k = "(\x. if x \ {0..real n / real N} \ Q' then k x else (p' \ h) x)" ``` lp15@64792 ` 1822` ``` show ?case ``` lp15@64792 ` 1823` ``` proof (intro exI conjI) ``` lp15@64792 ` 1824` ``` show "continuous_on ({0..real (Suc n) / real N} \ Q) ?k" ``` lp15@64792 ` 1825` ``` apply (rule continuous_on_subset [OF cont]) ``` lp15@64792 ` 1826` ``` using \Q \ Q'\ by auto ``` lp15@64792 ` 1827` ``` have "\a b. \a \ real n / real N; b \ Q'; 0 \ a\ \ k (a, b) \ C" ``` lp15@64792 ` 1828` ``` using kim Q' by force ``` lp15@64792 ` 1829` ``` moreover have "\a b. \b \ Q; 0 \ a; a \ (1 + real n) / real N; \ a \ real n / real N\ \ p' (h (a, b)) \ C" ``` lp15@64792 ` 1830` ``` apply (rule \W \ C\ [THEN subsetD]) ``` lp15@64792 ` 1831` ``` using homeomorphism_image2 [OF hom', symmetric] h_in_UU Q' \Q \ Q'\ \W \ C\ ``` lp15@64792 ` 1832` ``` apply auto ``` lp15@64792 ` 1833` ``` done ``` lp15@64792 ` 1834` ``` ultimately show "?k ` ({0..real (Suc n) / real N} \ Q) \ C" ``` lp15@64792 ` 1835` ``` using Q' \Q \ Q'\ by force ``` lp15@64792 ` 1836` ``` show "\z\Q. ?k (0, z) = f z" ``` lp15@64792 ` 1837` ``` using Q' keq \Q \ Q'\ by auto ``` lp15@64792 ` 1838` ``` show "\z \ {0..real (Suc n) / real N} \ Q. h z = p(?k z)" ``` lp15@64792 ` 1839` ``` using \Q \ U \ NN t \ N' \ V\ heq apply clarsimp ``` lp15@64792 ` 1840` ``` using h_in_UU Q' \Q \ Q'\ apply (auto simp: homeomorphism_apply2 [OF hom', symmetric]) ``` lp15@64792 ` 1841` ``` done ``` lp15@64792 ` 1842` ``` qed (auto simp: \y \ Q\ opeUQ) ``` lp15@64792 ` 1843` ``` qed ``` lp15@64792 ` 1844` ``` show ?thesis ``` lp15@64792 ` 1845` ``` using*[OF order_refl] N \0 < \\ by (simp add: split: if_split_asm) ``` lp15@64792 ` 1846` ``` qed ``` lp15@64792 ` 1847` ``` then obtain V fs where opeV: "\y. y \ U \ openin (subtopology euclidean U) (V y)" ``` lp15@64792 ` 1848` ``` and V: "\y. y \ U \ y \ V y" ``` lp15@64792 ` 1849` ``` and contfs: "\y. y \ U \ continuous_on ({0..1} \ V y) (fs y)" ``` lp15@64792 ` 1850` ``` and *: "\y. y \ U \ (fs y) ` ({0..1} \ V y) \ C \ ``` lp15@64792 ` 1851` ``` (\z \ V y. fs y (0, z) = f z) \ ``` lp15@64792 ` 1852` ``` (\z \ {0..1} \ V y. h z = p(fs y z))" ``` lp15@64792 ` 1853` ``` by (metis (mono_tags)) ``` lp15@64792 ` 1854` ``` then have VU: "\y. y \ U \ V y \ U" ``` lp15@64792 ` 1855` ``` by (meson openin_imp_subset) ``` lp15@64792 ` 1856` ``` obtain k where contk: "continuous_on ({0..1} \ U) k" ``` lp15@64792 ` 1857` ``` and k: "\x i. \i \ U; x \ {0..1} \ U \ {0..1} \ V i\ \ k x = fs i x" ``` lp15@64792 ` 1858` ``` proof (rule pasting_lemma_exists) ``` lp15@64792 ` 1859` ``` show "{0..1} \ U \ (\i\U. {0..1} \ V i)" ``` lp15@64792 ` 1860` ``` apply auto ``` lp15@64792 ` 1861` ``` using V by blast ``` lp15@64792 ` 1862` ``` show "\i. i \ U \ openin (subtopology euclidean ({0..1} \ U)) ({0..1} \ V i)" ``` lp15@64792 ` 1863` ``` by (simp add: opeV openin_Times) ``` lp15@64792 ` 1864` ``` show "\i. i \ U \ continuous_on ({0..1} \ V i) (fs i)" ``` lp15@64792 ` 1865` ``` using contfs by blast ``` lp15@64792 ` 1866` ``` show "fs i x = fs j x" if "i \ U" "j \ U" and x: "x \ {0..1} \ U \ {0..1} \ V i \ {0..1} \ V j" ``` lp15@64792 ` 1867` ``` for i j x ``` lp15@64792 ` 1868` ``` proof - ``` lp15@64792 ` 1869` ``` obtain u y where "x = (u, y)" "y \ V i" "y \ V j" "0 \ u" "u \ 1" ``` lp15@64792 ` 1870` ``` using x by auto ``` lp15@64792 ` 1871` ``` show ?thesis ``` lp15@64792 ` 1872` ``` proof (rule covering_space_lift_unique [OF cov, of _ "(0,y)" _ "{0..1} \ {y}" h]) ``` lp15@64792 ` 1873` ``` show "fs i (0, y) = fs j (0, y)" ``` lp15@64792 ` 1874` ``` using*V by (simp add: \y \ V i\ \y \ V j\ that) ``` lp15@64792 ` 1875` ``` show conth_y: "continuous_on ({0..1} \ {y}) h" ``` lp15@64792 ` 1876` ``` apply (rule continuous_on_subset [OF conth]) ``` lp15@64792 ` 1877` ``` using VU \y \ V j\ that by auto ``` lp15@64792 ` 1878` ``` show "h ` ({0..1} \ {y}) \ S" ``` lp15@64792 ` 1879` ``` using \y \ V i\ assms(3) VU that by fastforce ``` lp15@64792 ` 1880` ``` show "continuous_on ({0..1} \ {y}) (fs i)" ``` lp15@64792 ` 1881` ``` using continuous_on_subset [OF contfs] \i \ U\ ``` lp15@64792 ` 1882` ``` by (simp add: \y \ V i\ subset_iff) ``` lp15@64792 ` 1883` ``` show "fs i ` ({0..1} \ {y}) \ C" ``` lp15@64792 ` 1884` ``` using "*" \y \ V i\ \i \ U\ by fastforce ``` lp15@64792 ` 1885` ``` show "\x. x \ {0..1} \ {y} \ h x = p (fs i x)" ``` lp15@64792 ` 1886` ``` using "*" \y \ V i\ \i \ U\ by blast ``` lp15@64792 ` 1887` ``` show "continuous_on ({0..1} \ {y}) (fs j)" ``` lp15@64792 ` 1888` ``` using continuous_on_subset [OF contfs] \j \ U\ ``` lp15@64792 ` 1889` ``` by (simp add: \y \ V j\ subset_iff) ``` lp15@64792 ` 1890` ``` show "fs j ` ({0..1} \ {y}) \ C" ``` lp15@64792 ` 1891` ``` using "*" \y \ V j\ \j \ U\ by fastforce ``` lp15@64792 ` 1892` ``` show "\x. x \ {0..1} \ {y} \ h x = p (fs j x)" ``` lp15@64792 ` 1893` ``` using "*" \y \ V j\ \j \ U\ by blast ``` lp15@64792 ` 1894` ``` show "connected ({0..1::real} \ {y})" ``` lp15@64792 ` 1895` ``` using connected_Icc connected_Times connected_sing by blast ``` lp15@64792 ` 1896` ``` show "(0, y) \ {0..1::real} \ {y}" ``` lp15@64792 ` 1897` ``` by force ``` lp15@64792 ` 1898` ``` show "x \ {0..1} \ {y}" ``` lp15@64792 ` 1899` ``` using \x = (u, y)\ x by blast ``` lp15@64792 ` 1900` ``` qed ``` lp15@64792 ` 1901` ``` qed ``` lp15@64792 ` 1902` ``` qed blast ``` lp15@64792 ` 1903` ``` show ?thesis ``` lp15@64792 ` 1904` ``` proof ``` lp15@64792 ` 1905` ``` show "k ` ({0..1} \ U) \ C" ``` lp15@64792 ` 1906` ``` using V*k VU by fastforce ``` lp15@64792 ` 1907` ``` show "\y. y \ U \ k (0, y) = f y" ``` lp15@64792 ` 1908` ``` by (simp add: V*k) ``` lp15@64792 ` 1909` ``` show "\z. z \ {0..1} \ U \ h z = p (k z)" ``` lp15@64792 ` 1910` ``` using V*k by auto ``` lp15@64792 ` 1911` ``` qed (auto simp: contk) ``` lp15@64792 ` 1912` ```qed ``` lp15@64792 ` 1913` lp15@64792 ` 1914` ```corollary covering_space_lift_homotopy_alt: ``` lp15@64792 ` 1915` ``` fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" ``` lp15@64792 ` 1916` ``` and h :: "'c::real_normed_vector \ real \ 'b" ``` lp15@64792 ` 1917` ``` assumes cov: "covering_space C p S" ``` lp15@64792 ` 1918` ``` and conth: "continuous_on (U \ {0..1}) h" ``` lp15@64792 ` 1919` ``` and him: "h ` (U \ {0..1}) \ S" ``` lp15@64792 ` 1920` ``` and heq: "\y. y \ U \ h (y,0) = p(f y)" ``` lp15@64792 ` 1921` ``` and contf: "continuous_on U f" and fim: "f ` U \ C" ``` lp15@64792 ` 1922` ``` obtains k where "continuous_on (U \ {0..1}) k" ``` lp15@64792 ` 1923` ``` "k ` (U \ {0..1}) \ C" ``` lp15@64792 ` 1924` ``` "\y. y \ U \ k(y, 0) = f y" ``` lp15@64792 ` 1925` ``` "\z. z \ U \ {0..1} \ h z = p(k z)" ``` lp15@64792 ` 1926` ```proof - ``` lp15@64792 ` 1927` ``` have "continuous_on ({0..1} \ U) (h \ (\z. (snd z, fst z)))" ``` lp15@64792 ` 1928` ``` by (intro continuous_intros continuous_on_subset [OF conth]) auto ``` lp15@64792 ` 1929` ``` then obtain k where contk: "continuous_on ({0..1} \ U) k" ``` lp15@64792 ` 1930` ``` and kim: "k ` ({0..1} \ U) \ C" ``` lp15@64792 ` 1931` ``` and k0: "\y. y \ U \ k(0, y) = f y" ``` lp15@64792 ` 1932` ``` and heqp: "\z. z \ {0..1} \ U \ (h \ (\z. Pair (snd z) (fst z))) z = p(k z)" ``` lp15@64792 ` 1933` ``` apply (rule covering_space_lift_homotopy [OF cov _ _ _ contf fim]) ``` lp15@64792 ` 1934` ``` using him by (auto simp: contf heq) ``` lp15@64792 ` 1935` ``` show ?thesis ``` lp15@64792 ` 1936` ``` apply (rule_tac k="k \ (\z. Pair (snd z) (fst z))" in that) ``` lp15@64792 ` 1937` ``` apply (intro continuous_intros continuous_on_subset [OF contk]) ``` lp15@64792 ` 1938` ``` using kim heqp apply (auto simp: k0) ``` lp15@64792 ` 1939` ``` done ``` lp15@64792 ` 1940` ```qed ``` lp15@64792 ` 1941` lp15@64792 ` 1942` ```corollary covering_space_lift_homotopic_function: ``` lp15@64792 ` 1943` ``` fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" and g:: "'c::real_normed_vector \ 'a" ``` lp15@64792 ` 1944` ``` assumes cov: "covering_space C p S" ``` lp15@64792 ` 1945` ``` and contg: "continuous_on U g" ``` lp15@64792 ` 1946` ``` and gim: "g ` U \ C" ``` lp15@64792 ` 1947` ``` and pgeq: "\y. y \ U \ p(g y) = f y" ``` lp15@64792 ` 1948` ``` and hom: "homotopic_with (\x. True) U S f f'" ``` lp15@64792 ` 1949` ``` obtains g' where "continuous_on U g'" "image g' U \ C" "\y. y \ U \ p(g' y) = f' y" ``` lp15@64792 ` 1950` ```proof - ``` lp15@64792 ` 1951` ``` obtain h where conth: "continuous_on ({0..1::real} \ U) h" ``` lp15@64792 ` 1952` ``` and him: "h ` ({0..1} \ U) \ S" ``` lp15@64792 ` 1953` ``` and h0: "\x. h(0, x) = f x" ``` lp15@64792 ` 1954` ``` and h1: "\x. h(1, x) = f' x" ``` lp15@64792 ` 1955` ``` using hom by (auto simp: homotopic_with_def) ``` lp15@64792 ` 1956` ``` have "\y. y \ U \ h (0, y) = p (g y)" ``` lp15@64792 ` 1957` ``` by (simp add: h0 pgeq) ``` lp15@64792 ` 1958` ``` then obtain k where contk: "continuous_on ({0..1} \ U) k" ``` lp15@64792 ` 1959` ``` and kim: "k ` ({0..1} \ U) \ C" ``` lp15@64792 ` 1960` ``` and k0: "\y. y \ U \ k(0, y) = g y" ``` lp15@64792 ` 1961` ``` and heq: "\z. z \ {0..1} \ U \ h z = p(k z)" ``` lp15@64792 ` 1962` ``` using covering_space_lift_homotopy [OF cov conth him _ contg gim] by metis ``` lp15@64792 ` 1963` ``` show ?thesis ``` lp15@64792 ` 1964` ``` proof ``` lp15@64792 ` 1965` ``` show "continuous_on U (k \ Pair 1)" ``` lp15@64792 ` 1966` ``` by (meson contk atLeastAtMost_iff continuous_on_o_Pair order_refl zero_le_one) ``` lp15@64792 ` 1967` ``` show "(k \ Pair 1) ` U \ C" ``` lp15@64792 ` 1968` ``` using kim by auto ``` lp15@64792 ` 1969` ``` show "\y. y \ U \ p ((k \ Pair 1) y) = f' y" ``` lp15@64792 ` 1970` ``` by (auto simp: h1 heq [symmetric]) ``` lp15@64792 ` 1971` ``` qed ``` lp15@64792 ` 1972` ```qed ``` lp15@64792 ` 1973` lp15@64792 ` 1974` ```corollary covering_space_lift_inessential_function: ``` lp15@64792 ` 1975` ``` fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" and U :: "'c::real_normed_vector set" ``` lp15@64792 ` 1976` ``` assumes cov: "covering_space C p S" ``` lp15@64792 ` 1977` ``` and hom: "homotopic_with (\x. True) U S f (\x. a)" ``` lp15@64792 ` 1978` ``` obtains g where "continuous_on U g" "g ` U \ C" "\y. y \ U \ p(g y) = f y" ``` lp15@64792 ` 1979` ```proof (cases "U = {}") ``` lp15@64792 ` 1980` ``` case True ``` lp15@64792 ` 1981` ``` then show ?thesis ``` lp15@64792 ` 1982` ``` using that continuous_on_empty by blast ``` lp15@64792 ` 1983` ```next ``` lp15@64792 ` 1984` ``` case False ``` lp15@64792 ` 1985` ``` then obtain b where b: "b \ C" "p b = a" ``` lp15@64792 ` 1986` ``` using covering_space_imp_surjective [OF cov] homotopic_with_imp_subset2 [OF hom] ``` lp15@64792 ` 1987` ``` by auto ``` lp15@64792 ` 1988` ``` then have gim: "(\y. b) ` U \ C" ``` lp15@64792 ` 1989` ``` by blast ``` lp15@64792 ` 1990` ``` show ?thesis ``` lp15@64792 ` 1991` ``` apply (rule covering_space_lift_homotopic_function ``` lp15@64792 ` 1992` ``` [OF cov continuous_on_const gim _ homotopic_with_symD [OF hom]]) ``` lp15@64792 ` 1993` ``` using b that apply auto ``` lp15@64792 ` 1994` ``` done ``` lp15@64792 ` 1995` ```qed ``` lp15@64792 ` 1996` lp15@64792 ` 1997` ```subsection\ Lifting of general functions to covering space\ ``` lp15@64792 ` 1998` lp15@64792 ` 1999` ```proposition covering_space_lift_path_strong: ``` lp15@64792 ` 2000` ``` fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" ``` lp15@64792 ` 2001` ``` and f :: "'c::real_normed_vector \ 'b" ``` lp15@64792 ` 2002` ``` assumes cov: "covering_space C p S" and "a \ C" ``` lp15@64792 ` 2003` ``` and "path g" and pag: "path_image g \ S" and pas: "pathstart g = p a" ``` lp15@64792 ` 2004` ``` obtains h where "path h" "path_image h \ C" "pathstart h = a" ``` lp15@64792 ` 2005` ``` and "\t. t \ {0..1} \ p(h t) = g t" ``` lp15@64792 ` 2006` ```proof - ``` lp15@64792 ` 2007` ``` obtain k:: "real \ 'c \ 'a" ``` lp15@64792 ` 2008` ``` where contk: "continuous_on ({0..1} \ {undefined}) k" ``` lp15@64792 ` 2009` ``` and kim: "k ` ({0..1} \ {undefined}) \ C" ``` lp15@64792 ` 2010` ``` and k0: "k (0, undefined) = a" ``` lp15@64792 ` 2011` ``` and pk: "\z. z \ {0..1} \ {undefined} \ p(k z) = (g \ fst) z" ``` lp15@64792 ` 2012` ``` proof (rule covering_space_lift_homotopy [OF cov, of "{undefined}" "g \ fst"]) ``` lp15@64792 ` 2013` ``` show "continuous_on ({0..1::real} \ {undefined::'c}) (g \ fst)" ``` lp15@64792 ` 2014` ``` apply (intro continuous_intros) ``` lp15@64792 ` 2015` ``` using \path g\ by (simp add: path_def) ``` lp15@64792 ` 2016` ``` show "(g \ fst) ` ({0..1} \ {undefined}) \ S" ``` lp15@64792 ` 2017` ``` using pag by (auto simp: path_image_def) ``` lp15@64792 ` 2018` ``` show "(g \ fst) (0, y) = p a" if "y \ {undefined}" for y::'c ``` lp15@64792 ` 2019` ``` by (metis comp_def fst_conv pas pathstart_def) ``` lp15@64792 ` 2020` ``` qed (use assms in auto) ``` lp15@64792 ` 2021` ``` show ?thesis ``` lp15@64792 ` 2022` ``` proof ``` lp15@64792 ` 2023` ``` show "path (k \ (\t. Pair t undefined))" ``` lp15@64792 ` 2024` ``` unfolding path_def ``` lp15@64792 ` 2025` ``` by (intro continuous_on_compose continuous_intros continuous_on_subset [OF contk]) auto ``` lp15@64792 ` 2026` ``` show "path_image (k \ (\t. (t, undefined))) \ C" ``` lp15@64792 ` 2027` ``` using kim by (auto simp: path_image_def) ``` lp15@64792 ` 2028` ``` show "pathstart (k \ (\t. (t, undefined))) = a" ``` lp15@64792 ` 2029` ``` by (auto simp: pathstart_def k0) ``` lp15@64792 ` 2030` ``` show "\t. t \ {0..1} \ p ((k \ (\t. (t, undefined))) t) = g t" ``` lp15@64792 ` 2031` ``` by (auto simp: pk) ``` lp15@64792 ` 2032` ``` qed ``` lp15@64792 ` 2033` ```qed ``` lp15@64792 ` 2034` lp15@64792 ` 2035` ```corollary covering_space_lift_path: ``` lp15@64792 ` 2036` ``` fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" ``` lp15@64792 ` 2037` ``` assumes cov: "covering_space C p S" and "path g" and pig: "path_image g \ S" ``` lp15@64792 ` 2038` ``` obtains h where "path h" "path_image h \ C" "\t. t \ {0..1} \ p(h t) = g t" ``` lp15@64792 ` 2039` ```proof - ``` lp15@64792 ` 2040` ``` obtain a where "a \ C" "pathstart g = p a" ``` lp15@64792 ` 2041` ``` by (metis pig cov covering_space_imp_surjective imageE pathstart_in_path_image subsetCE) ``` lp15@64792 ` 2042` ``` show ?thesis ``` lp15@64792 ` 2043` ``` using covering_space_lift_path_strong [OF cov \a \ C\ \path g\ pig] ``` lp15@64792 ` 2044` ``` by (metis \pathstart g = p a\ that) ``` lp15@64792 ` 2045` ```qed ``` lp15@64792 ` 2046` lp15@64792 ` 2047` ``` ``` lp15@64792 ` 2048` ```proposition covering_space_lift_homotopic_paths: ``` lp15@64792 ` 2049` ``` fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" ``` lp15@64792 ` 2050` ``` assumes cov: "covering_space C p S" ``` lp15@64792 ` 2051` ``` and "path g1" and pig1: "path_image g1 \ S" ``` lp15@64792 ` 2052` ``` and "path g2" and pig2: "path_image g2 \ S" ``` lp15@64792 ` 2053` ``` and hom: "homotopic_paths S g1 g2" ``` lp15@64792 ` 2054` ``` and "path h1" and pih1: "path_image h1 \ C" and ph1: "\t. t \ {0..1} \ p(h1 t) = g1 t" ``` lp15@64792 ` 2055` ``` and "path h2" and pih2: "path_image h2 \ C" and ph2: "\t. t \ {0..1} \ p(h2 t) = g2 t" ``` lp15@64792 ` 2056` ``` and h1h2: "pathstart h1 = pathstart h2" ``` lp15@64792 ` 2057` ``` shows "homotopic_paths C h1 h2" ``` lp15@64792 ` 2058` ```proof - ``` lp15@64792 ` 2059` ``` obtain h :: "real \ real \ 'b" ``` lp15@64792 ` 2060` ``` where conth: "continuous_on ({0..1} \ {0..1}) h" ``` lp15@64792 ` 2061` ``` and him: "h ` ({0..1} \ {0..1}) \ S" ``` lp15@64792 ` 2062` ``` and h0: "\x. h (0, x) = g1 x" and h1: "\x. h (1, x) = g2 x" ``` lp15@64792 ` 2063` ``` and heq0: "\t. t \ {0..1} \ h (t, 0) = g1 0" ``` lp15@64792 ` 2064` ``` and heq1: "\t. t \ {0..1} \ h (t, 1) = g1 1" ``` lp15@64792 ` 2065` ``` using hom by (auto simp: homotopic_paths_def homotopic_with_def pathstart_def pathfinish_def) ``` lp15@64792 ` 2066` ``` obtain k where contk: "continuous_on ({0..1} \ {0..1}) k" ``` lp15@64792 ` 2067` ``` and kim: "k ` ({0..1} \ {0..1}) \ C" ``` lp15@64792 ` 2068` ``` and kh2: "\y. y \ {0..1} \ k (y, 0) = h2 0" ``` lp15@64792 ` 2069` ``` and hpk: "\z. z \ {0..1} \ {0..1} \ h z = p (k z)" ``` lp15@64792 ` 2070` ``` apply (rule covering_space_lift_homotopy_alt [OF cov conth him, of "\x. h2 0"]) ``` lp15@64792 ` 2071` ``` using h1h2 ph1 ph2 apply (force simp: heq0 pathstart_def pathfinish_def) ``` lp15@64792 ` 2072` ``` using path_image_def pih2 continuous_on_const by fastforce+ ``` lp15@64792 ` 2073` ``` have contg1: "continuous_on {0..1} g1" and contg2: "continuous_on {0..1} g2" ``` lp15@64792 ` 2074` ``` using \path g1\ \path g2\ path_def by blast+ ``` lp15@64792 ` 2075` ``` have g1im: "g1 ` {0..1} \ S" and g2im: "g2 ` {0..1} \ S" ``` lp15@64792 ` 2076` ``` using path_image_def pig1 pig2 by auto ``` lp15@64792 ` 2077` ``` have conth1: "continuous_on {0..1} h1" and conth2: "continuous_on {0..1} h2" ``` lp15@64792 ` 2078` ``` using \path h1\ \path h2\ path_def by blast+ ``` lp15@64792 ` 2079` ``` have h1im: "h1 ` {0..1} \ C" and h2im: "h2 ` {0..1} \ C" ``` lp15@64792 ` 2080` ``` using path_image_def pih1 pih2 by auto ``` lp15@64792 ` 2081` ``` show ?thesis ``` lp15@64792 ` 2082` ``` unfolding homotopic_paths pathstart_def pathfinish_def ``` lp15@64792 ` 2083` ``` proof (intro exI conjI ballI) ``` lp15@64792 ` 2084` ``` show keqh1: "k(0, x) = h1 x" if "x \ {0..1}" for x ``` lp15@64792 ` 2085` ``` proof (rule covering_space_lift_unique [OF cov _ contg1 g1im]) ``` lp15@64792 ` 2086` ``` show "k (0,0) = h1 0" ``` lp15@64792 ` 2087` ``` by (metis atLeastAtMost_iff h1h2 kh2 order_refl pathstart_def zero_le_one) ``` lp15@64792 ` 2088` ``` show "continuous_on {0..1} (\a. k (0, a))" ``` lp15@64792 ` 2089` ``` by (intro continuous_intros continuous_on_compose2 [OF contk]) auto ``` lp15@64792 ` 2090` ``` show "\x. x \ {0..1} \ g1 x = p (k (0, x))" ``` lp15@64792 ` 2091` ``` by (metis atLeastAtMost_iff h0 hpk zero_le_one mem_Sigma_iff order_refl) ``` lp15@64792 ` 2092` ``` qed (use conth1 h1im kim that in \auto simp: ph1\) ``` lp15@64792 ` 2093` ``` show "k(1, x) = h2 x" if "x \ {0..1}" for x ``` lp15@64792 ` 2094` ``` proof (rule covering_space_lift_unique [OF cov _ contg2 g2im]) ``` lp15@64792 ` 2095` ``` show "k (1,0) = h2 0" ``` lp15@64792 ` 2096` ``` by (metis atLeastAtMost_iff kh2 order_refl zero_le_one) ``` lp15@64792 ` 2097` ``` show "continuous_on {0..1} (\a. k (1, a))" ``` lp15@64792 ` 2098` ``` by (intro continuous_intros continuous_on_compose2 [OF contk]) auto ``` lp15@64792 ` 2099` ``` show "\x. x \ {0..1} \ g2 x = p (k (1, x))" ``` lp15@64792 ` 2100` ``` by (metis atLeastAtMost_iff h1 hpk mem_Sigma_iff order_refl zero_le_one) ``` lp15@64792 ` 2101` ``` qed (use conth2 h2im kim that in \auto simp: ph2\) ``` lp15@64792 ` 2102` ``` show "\t. t \ {0..1} \ (k \ Pair t) 0 = h1 0" ``` lp15@64792 ` 2103` ``` by (metis comp_apply h1h2 kh2 pathstart_def) ``` lp15@64792 ` 2104` ``` show "(k \ Pair t) 1 = h1 1" if "t \ {0..1}" for t ``` lp15@64792 ` 2105` ``` proof (rule covering_space_lift_unique ``` lp15@64792 ` 2106` ``` [OF cov, of "\a. (k \ Pair a) 1" 0 "\a. h1 1" "{0..1}" "\x. g1 1"]) ``` lp15@64792 ` 2107` ``` show "(k \ Pair 0) 1 = h1 1" ``` lp15@64792 ` 2108` ``` using keqh1 by auto ``` lp15@64792 ` 2109` ``` show "continuous_on {0..1} (\a. (k \ Pair a) 1)" ``` lp15@64792 ` 2110` ``` apply simp ``` lp15@64792 ` 2111` ``` by (intro continuous_intros continuous_on_compose2 [OF contk]) auto ``` lp15@64792 ` 2112` ``` show "\x. x \ {0..1} \ g1 1 = p ((k \ Pair x) 1)" ``` lp15@64792 ` 2113` ``` using heq1 hpk by auto ``` lp15@64792 ` 2114` ``` qed (use contk kim g1im h1im that in \auto simp: ph1 continuous_on_const\) ``` lp15@64792 ` 2115` ``` qed (use contk kim in auto) ``` lp15@64792 ` 2116` ```qed ``` lp15@64792 ` 2117` lp15@64792 ` 2118` lp15@64792 ` 2119` ```corollary covering_space_monodromy: ``` lp15@64792 ` 2120` ``` fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" ``` lp15@64792 ` 2121` ``` assumes cov: "covering_space C p S" ``` lp15@64792 ` 2122` ``` and "path g1" and pig1: "path_image g1 \ S" ``` lp15@64792 ` 2123` ``` and "path g2" and pig2: "path_image g2 \ S" ``` lp15@64792 ` 2124` ``` and hom: "homotopic_paths S g1 g2" ``` lp15@64792 ` 2125` ``` and "path h1" and pih1: "path_image h1 \ C" and ph1: "\t. t \ {0..1} \ p(h1 t) = g1 t" ``` lp15@64792 ` 2126` ``` and "path h2" and pih2: "path_image h2 \ C" and ph2: "\t. t \ {0..1} \ p(h2 t) = g2 t" ``` lp15@64792 ` 2127` ``` and h1h2: "pathstart h1 = pathstart h2" ``` lp15@64792 ` 2128` ``` shows "pathfinish h1 = pathfinish h2" ``` lp15@64792 ` 2129` ``` using covering_space_lift_homotopic_paths [OF assms] homotopic_paths_imp_pathfinish by blast ``` lp15@64792 ` 2130` lp15@64792 ` 2131` lp15@64792 ` 2132` ```corollary covering_space_lift_homotopic_path: ``` lp15@64792 ` 2133` ``` fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" ``` lp15@64792 ` 2134` ``` assumes cov: "covering_space C p S" ``` lp15@64792 ` 2135` ``` and hom: "homotopic_paths S f f'" ``` lp15@64792 ` 2136` ``` and "path g" and pig: "path_image g \ C" ``` lp15@64792 ` 2137` ``` and a: "pathstart g = a" and b: "pathfinish g = b" ``` lp15@64792 ` 2138` ``` and pgeq: "\t. t \ {0..1} \ p(g t) = f t" ``` lp15@64792 ` 2139` ``` obtains g' where "path g'" "path_image g' \ C" ``` lp15@64792 ` 2140` ``` "pathstart g' = a" "pathfinish g' = b" "\t. t \ {0..1} \ p(g' t) = f' t" ``` lp15@64792 ` 2141` ```proof (rule covering_space_lift_path_strong [OF cov, of a f']) ``` lp15@64792 ` 2142` ``` show "a \ C" ``` lp15@64792 ` 2143` ``` using a pig by auto ``` lp15@64792 ` 2144` ``` show "path f'" "path_image f' \ S" ``` lp15@64792 ` 2145` ``` using hom homotopic_paths_imp_path homotopic_paths_imp_subset by blast+ ``` lp15@64792 ` 2146` ``` show "pathstart f' = p a" ``` lp15@64792 ` 2147` ``` by (metis a atLeastAtMost_iff hom homotopic_paths_imp_pathstart order_refl pathstart_def pgeq zero_le_one) ``` lp15@64792 ` 2148` ```qed (metis (mono_tags, lifting) assms cov covering_space_monodromy hom homotopic_paths_imp_path homotopic_paths_imp_subset pgeq pig) ``` lp15@64792 ` 2149` lp15@64792 ` 2150` lp15@64792 ` 2151` ```proposition covering_space_lift_general: ``` lp15@64792 ` 2152` ``` fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" ``` lp15@64792 ` 2153` ``` and f :: "'c::real_normed_vector \ 'b" ``` lp15@64792 ` 2154` ``` assumes cov: "covering_space C p S" and "a \ C" "z \ U" ``` lp15@64792 ` 2155` ``` and U: "path_connected U" "locally path_connected U" ``` lp15@64792 ` 2156` ``` and contf: "continuous_on U f" and fim: "f ` U \ S" ``` lp15@64792 ` 2157` ``` and feq: "f z = p a" ``` lp15@64792 ` 2158` ``` and hom: "\r. \path r; path_image r \ U; pathstart r = z; pathfinish r = z\ ``` lp15@64792 ` 2159` ``` \ \q. path q \ path_image q \ C \ ``` lp15@64792 ` 2160` ``` pathstart q = a \ pathfinish q = a \ ``` lp15@64792 ` 2161` ``` homotopic_paths S (f \ r) (p \ q)" ``` lp15@64792 ` 2162` ``` obtains g where "continuous_on U g" "g ` U \ C" "g z = a" "\y. y \ U \ p(g y) = f y" ``` lp15@64792 ` 2163` ```proof - ``` lp15@64792 ` 2164` ``` have *: "\g h. path g \ path_image g \ U \ ``` lp15@64792 ` 2165` ``` pathstart g = z \ pathfinish g = y \ ``` lp15@64792 ` 2166` ``` path h \ path_image h \ C \ pathstart h = a \ ``` lp15@64792 ` 2167` ``` (\t \ {0..1}. p(h t) = f(g t))" ``` lp15@64792 ` 2168` ``` if "y \ U" for y ``` lp15@64792 ` 2169` ``` proof - ``` lp15@64792 ` 2170` ``` obtain g where "path g" "path_image g \ U" and pastg: "pathstart g = z" ``` lp15@64792 ` 2171` ``` and pafig: "pathfinish g = y" ``` lp15@64792 ` 2172` ``` using U \z \ U\ \y \ U\ by (force simp: path_connected_def) ``` lp15@64792 ` 2173` ``` obtain h where "path h" "path_image h \ C" "pathstart h = a" ``` lp15@64792 ` 2174` ``` and "\t. t \ {0..1} \ p(h t) = (f \ g) t" ``` lp15@64792 ` 2175` ``` proof (rule covering_space_lift_path_strong [OF cov \a \ C\]) ``` lp15@64792 ` 2176` ``` show "path (f \ g)" ``` lp15@64792 ` 2177` ``` using \path g\ \path_image g \ U\ contf continuous_on_subset path_continuous_image by blast ``` lp15@64792 ` 2178` ``` show "path_image (f \ g) \ S" ``` lp15@64792 ` 2179` ``` by (metis \path_image g \ U\ fim image_mono path_image_compose subset_trans) ``` lp15@64792 ` 2180` ``` show "pathstart (f \ g) = p a" ``` lp15@64792 ` 2181` ``` by (simp add: feq pastg pathstart_compose) ``` lp15@64792 ` 2182` ``` qed auto ``` lp15@64792 ` 2183` ``` then show ?thesis ``` lp15@64792 ` 2184` ``` by (metis \path g\ \path_image g \ U\ comp_apply pafig pastg) ``` lp15@64792 ` 2185` ``` qed ``` lp15@64792 ` 2186` ``` have "\l. \g h. path g \ path_image g \ U \ pathstart g = z \ pathfinish g = y \ ``` lp15@64792 ` 2187` ``` path h \ path_image h \ C \ pathstart h = a \ ``` lp15@64792 ` 2188` ``` (\t \ {0..1}. p(h t) = f(g t)) \ pathfinish h = l" for y ``` lp15@64792 ` 2189` ``` proof - ``` lp15@64792 ` 2190` ``` have "pathfinish h = pathfinish h'" ``` lp15@64792 ` 2191` ``` if g: "path g" "path_image g \ U" "pathstart g = z" "pathfinish g = y" ``` lp15@64792 ` 2192` ``` and h: "path h" "path_image h \ C" "pathstart h = a" ``` lp15@64792 ` 2193` ``` and phg: "\t. t \ {0..1} \ p(h t) = f(g t)" ``` lp15@64792 ` 2194` ``` and g': "path g'" "path_image g' \ U" "pathstart g' = z" "pathfinish g' = y" ``` lp15@64792 ` 2195` ``` and h': "path h'" "path_image h' \ C" "pathstart h' = a" ``` lp15@64792 ` 2196` ``` and phg': "\t. t \ {0..1} \ p(h' t) = f(g' t)" ``` lp15@64792 ` 2197` ``` for g h g' h' ``` lp15@64792 ` 2198` ``` proof - ``` lp15@64792 ` 2199` ``` obtain q where "path q" and piq: "path_image q \ C" and pastq: "pathstart q = a" and pafiq: "pathfinish q = a" ``` lp15@64792 ` 2200` ``` and homS: "homotopic_paths S (f \ g +++ reversepath g') (p \ q)" ``` lp15@64792 ` 2201` ``` using g g' hom [of "g +++ reversepath g'"] by (auto simp: subset_path_image_join) ``` lp15@64792 ` 2202` ``` have papq: "path (p \ q)" ``` lp15@64792 ` 2203` ``` using homS homotopic_paths_imp_path by blast ``` lp15@64792 ` 2204` ``` have pipq: "path_image (p \ q) \ S" ``` lp15@64792 ` 2205` ``` using homS homotopic_paths_imp_subset by blast ``` lp15@64792 ` 2206` ``` obtain q' where "path q'" "path_image q' \ C" ``` lp15@64792 ` 2207` ``` and "pathstart q' = pathstart q" "pathfinish q' = pathfinish q" ``` lp15@64792 ` 2208` ``` and pq'_eq: "\t. t \ {0..1} \ p (q' t) = (f \ g +++ reversepath g') t" ``` lp15@64792 ` 2209` ``` using covering_space_lift_homotopic_path [OF cov homotopic_paths_sym [OF homS] \path q\ piq refl refl] ``` lp15@64792 ` 2210` ``` by auto ``` nipkow@67399 ` 2211` ``` have "q' t = (h \ ( *\<^sub>R) 2) t" if "0 \ t" "t \ 1/2" for t ``` nipkow@67399 ` 2212` ``` proof (rule covering_space_lift_unique [OF cov, of q' 0 "h \ ( *\<^sub>R) 2" "{0..1/2}" "f \ g \ ( *\<^sub>R) 2" t]) ``` nipkow@67399 ` 2213` ``` show "q' 0 = (h \ ( *\<^sub>R) 2) 0" ``` lp15@64792 ` 2214` ``` by (metis \pathstart q' = pathstart q\ comp_def g h pastq pathstart_def pth_4(2)) ``` nipkow@67399 ` 2215` ``` show "continuous_on {0..1/2} (f \ g \ ( *\<^sub>R) 2)" ``` lp15@64792 ` 2216` ``` apply (intro continuous_intros continuous_on_compose continuous_on_path [OF \path g\] continuous_on_subset [OF contf]) ``` lp15@64792 ` 2217` ``` using g(2) path_image_def by fastforce+ ``` nipkow@67399 ` 2218` ``` show "(f \ g \ ( *\<^sub>R) 2) ` {0..1/2} \ S" ``` lp15@64792 ` 2219` ``` using g(2) path_image_def fim by fastforce ``` nipkow@67399 ` 2220` ``` show "(h \ ( *\<^sub>R) 2) ` {0..1/2} \ C" ``` lp15@64792 ` 2221` ``` using h path_image_def by fastforce ``` lp15@64792 ` 2222` ``` show "q' ` {0..1/2} \ C" ``` lp15@64792 ` 2223` ``` using \path_image q' \ C\ path_image_def by fastforce ``` nipkow@67399 ` 2224` ``` show "\x. x \ {0..1/2} \ (f \ g \ ( *\<^sub>R) 2) x = p (q' x)" ``` lp15@64792 ` 2225` ``` by (auto simp: joinpaths_def pq'_eq) ``` nipkow@67399 ` 2226` ``` show "\x. x \ {0..1/2} \ (f \ g \ ( *\<^sub>R) 2) x = p ((h \ ( *\<^sub>R) 2) x)" ``` lp15@64792 ` 2227` ``` by (simp add: phg) ``` lp15@64792 ` 2228` ``` show "continuous_on {0..1/2} q'" ``` lp15@64792 ` 2229` ``` by (simp add: continuous_on_path \path q'\) ``` nipkow@67399 ` 2230` ``` show "continuous_on {0..1/2} (h \ ( *\<^sub>R) 2)" ``` lp15@64792 ` 2231` ``` apply (intro continuous_intros continuous_on_compose continuous_on_path [OF \path h\], force) ``` lp15@64792 ` 2232` ``` done ``` lp15@64792 ` 2233` ``` qed (use that in auto) ``` lp15@64792 ` 2234` ``` moreover have "q' t = (reversepath h' \ (\t. 2 *\<^sub>R t - 1)) t" if "1/2 < t" "t \ 1" for t ``` lp15@64792 ` 2235` ``` proof (rule covering_space_lift_unique [OF cov, of q' 1 "reversepath h' \ (\t. 2 *\<^sub>R t - 1)" "{1/2<..1}" "f \ reversepath g' \ (\t. 2 *\<^sub>R t - 1)" t]) ``` lp15@64792 ` 2236` ``` show "q' 1 = (reversepath h' \ (\t. 2 *\<^sub>R t - 1)) 1" ``` lp15@64792 ` 2237` ``` using h' \pathfinish q' = pathfinish q\ pafiq ``` lp15@64792 ` 2238` ``` by (simp add: pathstart_def pathfinish_def reversepath_def) ``` lp15@64792 ` 2239` ``` show "continuous_on {1/2<..1} (f \ reversepath g' \ (\t. 2 *\<^sub>R t - 1))" ``` lp15@64792 ` 2240` ``` apply (intro continuous_intros continuous_on_compose continuous_on_path \path g'\ continuous_on_subset [OF contf]) ``` lp15@64792 ` 2241` ``` using g' apply simp_all ``` lp15@64792 ` 2242` ``` by (auto simp: path_image_def reversepath_def) ``` lp15@64792 ` 2243` ``` show "(f \ reversepath g' \ (\t. 2 *\<^sub>R t - 1)) ` {1/2<..1} \ S" ``` lp15@64792 ` 2244` ``` using g'(2) path_image_def fim by (auto simp: image_subset_iff path_image_def reversepath_def) ``` lp15@64792 ` 2245` ``` show "q' ` {1/2<..1} \ C" ``` lp15@64792 ` 2246` ``` using \path_image q' \ C\ path_image_def by fastforce ``` lp15@64792 ` 2247` ``` show "(reversepath h' \ (\t. 2 *\<^sub>R t - 1)) ` {1/2<..1} \ C" ``` lp15@64792 ` 2248` ``` using h' by (simp add: path_image_def reversepath_def subset_eq) ``` lp15@64792 ` 2249` ``` show "\x. x \ {1/2<..1} \ (f \ reversepath g' \ (\t. 2 *\<^sub>R t - 1)) x = p (q' x)" ``` lp15@64792 ` 2250` ``` by (auto simp: joinpaths_def pq'_eq) ``` lp15@64792 ` 2251` ``` show "\x. x \ {1/2<..1} \ ``` lp15@64792 ` 2252` ``` (f \ reversepath g' \ (\t. 2 *\<^sub>R t - 1)) x = p ((reversepath h' \ (\t. 2 *\<^sub>R t - 1)) x)" ``` lp15@64792 ` 2253` ``` by (simp add: phg' reversepath_def) ``` lp15@64792 ` 2254` ``` show "continuous_on {1/2<..1} q'" ``` lp15@64792 ` 2255` ``` by (auto intro: continuous_on_path [OF \path q'\]) ``` lp15@64792 ` 2256` ``` show "continuous_on {1/2<..1} (reversepath h' \ (\t. 2 *\<^sub>R t - 1))" ``` lp15@64792 ` 2257` ``` apply (intro continuous_intros continuous_on_compose continuous_on_path \path h'\) ``` lp15@64792 ` 2258` ``` using h' apply auto ``` lp15@64792 ` 2259` ``` done ``` lp15@64792 ` 2260` ``` qed (use that in auto) ``` lp15@64792 ` 2261` ``` ultimately have "q' t = (h +++ reversepath h') t" if "0 \ t" "t \ 1" for t ``` lp15@64792 ` 2262` ``` using that by (simp add: joinpaths_def) ``` lp15@64792 ` 2263` ``` then have "path(h +++ reversepath h')" ``` lp15@64792 ` 2264` ``` by (auto intro: path_eq [OF \path q'\]) ``` lp15@64792 ` 2265` ``` then show ?thesis ``` lp15@64792 ` 2266` ``` by (auto simp: \path h\ \path h'\) ``` lp15@64792 ` 2267` ``` qed ``` lp15@64792 ` 2268` ``` then show ?thesis by metis ``` lp15@64792 ` 2269` ``` qed ``` lp15@64792 ` 2270` ``` then obtain l :: "'c \ 'a" ``` lp15@64792 ` 2271` ``` where l: "\y g h. \path g; path_image g \ U; pathstart g = z; pathfinish g = y; ``` lp15@64792 ` 2272` ``` path h; path_image h \ C; pathstart h = a; ``` lp15@64792 ` 2273` ``` \t. t \ {0..1} \ p(h t) = f(g t)\ \ pathfinish h = l y" ``` lp15@64792 ` 2274` ``` by metis ``` lp15@64792 ` 2275` ``` show ?thesis ``` lp15@64792 ` 2276` ``` proof ``` lp15@64792 ` 2277` ``` show pleq: "p (l y) = f y" if "y \ U" for y ``` lp15@64792 ` 2278` ``` using*[OF \y \ U\] by (metis l atLeastAtMost_iff order_refl pathfinish_def zero_le_one) ``` lp15@64792 ` 2279` ``` show "l z = a" ``` lp15@64792 ` 2280` ``` using l [of "linepath z z" z "linepath a a"] by (auto simp: assms) ``` lp15@64792 ` 2281` ``` show LC: "l ` U \ C" ``` lp15@64792 ` 2282` ``` by (clarify dest!: *) (metis (full_types) l pathfinish_in_path_image subsetCE) ``` lp15@66884 ` 2283` ``` have "\T. openin (subtopology euclidean U) T \ y \ T \ T \ U \ l -` X" ``` lp15@64792 ` 2284` ``` if X: "openin (subtopology euclidean C) X" and "y \ U" "l y \ X" for X y ``` lp15@64792 ` 2285` ``` proof - ``` lp15@64792 ` 2286` ``` have "X \ C" ``` lp15@64792 ` 2287` ``` using X openin_euclidean_subtopology_iff by blast ``` lp15@64792 ` 2288` ``` have "f y \ S" ``` lp15@64792 ` 2289` ``` using fim \y \ U\ by blast ``` lp15@64792 ` 2290` ``` then obtain W \ ``` lp15@64792 ` 2291` ``` where WV: "f y \ W \ openin (subtopology euclidean S) W \ ``` lp15@66884 ` 2292` ``` (\\ = C \ p -` W \ ``` lp15@64792 ` 2293` ``` (\U \ \. openin (subtopology euclidean C) U) \ ``` lp15@64792 ` 2294` ``` pairwise disjnt \ \ ``` lp15@64792 ` 2295` ``` (\U \ \. \q. homeomorphism U W p q))" ``` lp15@64792 ` 2296` ``` using cov by (force simp: covering_space_def) ``` lp15@64792 ` 2297` ``` then have "l y \ \\" ``` lp15@64792 ` 2298` ``` using \X \ C\ pleq that by auto ``` lp15@64792 ` 2299` ``` then obtain W' where "l y \ W'" and "W' \ \" ``` lp15@64792 ` 2300` ``` by blast ``` lp15@64792 ` 2301` ``` with WV obtain p' where opeCW': "openin (subtopology euclidean C) W'" ``` lp15@64792 ` 2302` ``` and homUW': "homeomorphism W' W p p'" ``` lp15@64792 ` 2303` ``` by blast ``` lp15@64792 ` 2304` ``` then have contp': "continuous_on W p'" and p'im: "p' ` W \ W'" ``` lp15@64792 ` 2305` ``` using homUW' homeomorphism_image2 homeomorphism_cont2 by fastforce+ ``` lp15@64792 ` 2306` ``` obtain V where "y \ V" "y \ U" and fimW: "f ` V \ W" "V \ U" ``` lp15@64792 ` 2307` ``` and "path_connected V" and opeUV: "openin (subtopology euclidean U) V" ``` lp15@64792 ` 2308` ``` proof - ``` lp15@66884 ` 2309` ``` have "openin (subtopology euclidean U) (U \ f -` W)" ``` lp15@64792 ` 2310` ``` using WV contf continuous_on_open_gen fim by auto ``` lp15@64792 ` 2311` ``` then show ?thesis ``` lp15@64792 ` 2312` ``` using U WV ``` lp15@64792 ` 2313` ``` apply (auto simp: locally_path_connected) ``` lp15@66884 ` 2314` ``` apply (drule_tac x="U \ f -` W" in spec) ``` lp15@64792 ` 2315` ``` apply (drule_tac x=y in spec) ``` lp15@64792 ` 2316` ``` apply (auto simp: \y \ U\ intro: that) ``` lp15@64792 ` 2317` ``` done ``` lp15@64792 ` 2318` ``` qed ``` lp15@64792 ` 2319` ``` have "W' \ C" "W \ S" ``` lp15@64792 ` 2320` ``` using opeCW' WV openin_imp_subset by auto ``` lp15@64792 ` 2321` ``` have p'im: "p' ` W \ W'" ``` lp15@64792 ` 2322` ``` using homUW' homeomorphism_image2 by fastforce ``` lp15@64792 ` 2323` ``` show ?thesis ``` lp15@64792 ` 2324` ``` proof (intro exI conjI) ``` lp15@66884 ` 2325` ``` have "openin (subtopology euclidean S) (W \ p' -` (W' \ X))" ``` lp15@64792 ` 2326` ``` proof (rule openin_trans) ``` lp15@66884 ` 2327` ``` show "openin (subtopology euclidean W) (W \ p' -` (W' \ X))" ``` lp15@64792 ` 2328` ``` apply (rule continuous_openin_preimage [OF contp' p'im]) ``` lp15@64792 ` 2329` ``` using X \W' \ C\ apply (auto simp: openin_open) ``` lp15@64792 ` 2330` ``` done ``` lp15@64792 ` 2331` ``` show "openin (subtopology euclidean S) W" ``` lp15@64792 ` 2332` ``` using WV by blast ``` lp15@64792 ` 2333` ``` qed ``` lp15@66884 ` 2334` ``` then show "openin (subtopology euclidean U) (V \ (U \ (f -` (W \ (p' -` (W' \ X))))))" ``` lp15@66884 ` 2335` ``` by (blast intro: opeUV openin_subtopology_self continuous_openin_preimage [OF contf fim]) ``` lp15@66884 ` 2336` ``` have "p' (f y) \ X" ``` lp15@64792 ` 2337` ``` using \l y \ W'\ homeomorphism_apply1 [OF homUW'] pleq \y \ U\ \l y \ X\ by fastforce ``` lp15@66884 ` 2338` ``` then show "y \ V \ (U \ f -` (W \ p' -` (W' \ X)))" ``` lp15@64792 ` 2339` ``` using \y \ U\ \y \ V\ WV p'im by auto ``` lp15@66884 ` 2340` ``` show "V \ (U \ f -` (W \ p' -` (W' \ X))) \ U \ l -` X" ``` lp15@66884 ` 2341` ``` proof (intro subsetI IntI; clarify) ``` lp15@64792 ` 2342` ``` fix y' ``` lp15@64792 ` 2343` ``` assume y': "y' \ V" "y' \ U" "f y' \ W" "p' (f y') \ W'" "p' (f y') \ X" ``` lp15@64792 ` 2344` ``` then obtain \ where "path \" "path_image \ \ V" "pathstart \ = y" "pathfinish \ = y'" ``` lp15@64792 ` 2345` ``` by (meson \path_connected V\ \y \ V\ path_connected_def) ``` lp15@64792 ` 2346` ``` obtain pp qq where "path pp" "path_image pp \ U" ``` lp15@64792 ` 2347` ``` "pathstart pp = z" "pathfinish pp = y" ``` lp15@64792 ` 2348` ``` "path qq" "path_image qq \ C" "pathstart qq = a" ``` lp15@64792 ` 2349` ``` and pqqeq: "\t. t \ {0..1} \ p(qq t) = f(pp t)" ``` lp15@64792 ` 2350` ``` using*[OF \y \ U\] by blast ``` lp15@64792 ` 2351` ``` have finW: "\x. \0 \ x; x \ 1\ \ f (\ x) \ W" ``` lp15@64792 ` 2352` ``` using \path_image \ \ V\ by (auto simp: image_subset_iff path_image_def fimW [THEN subsetD]) ``` lp15@64792 ` 2353` ``` have "pathfinish (qq +++ (p' \ f \ \)) = l y'" ``` lp15@66884 ` 2354` ``` proof (rule l [of "pp +++ \" y' "qq +++ (p' \ f \ \)"]) ``` lp15@64792 ` 2355` ``` show "path (pp +++ \)" ``` lp15@64792 ` 2356` ``` by (simp add: \path \\ \path pp\ \pathfinish pp = y\ \pathstart \ = y\) ``` lp15@64792 ` 2357` ``` show "path_image (pp +++ \) \ U" ``` lp15@64792 ` 2358` ``` using \V \ U\ \path_image \ \ V\ \path_image pp \ U\ not_in_path_image_join by blast ``` lp15@64792 ` 2359` ``` show "pathstart (pp +++ \) = z" ``` lp15@64792 ` 2360` ``` by (simp add: \pathstart pp = z\) ``` lp15@64792 ` 2361` ``` show "pathfinish (pp +++ \) = y'" ``` lp15@64792 ` 2362` ``` by (simp add: \pathfinish \ = y'\) ``` lp15@64792 ` 2363` ``` have paqq: "pathfinish qq = pathstart (p' \ f \ \)" ``` lp15@64792 ` 2364` ``` apply (simp add: \pathstart \ = y\ pathstart_compose) ``` lp15@64792 ` 2365` ``` apply (metis (mono_tags, lifting) \l y \ W'\ \path pp\ \path qq\ \path_image pp \ U\ \path_image qq \ C\ ``` lp15@64792 ` 2366` ``` \pathfinish pp = y\ \pathstart pp = z\ \pathstart qq = a\ ``` lp15@64792 ` 2367` ``` homeomorphism_apply1 [OF homUW'] l pleq pqqeq \y \ U\) ``` lp15@64792 ` 2368` ``` done ``` lp15@64792 ` 2369` ``` have "continuous_on (path_image \) (p' \ f)" ``` lp15@64792 ` 2370` ``` proof (rule continuous_on_compose) ``` lp15@64792 ` 2371` ``` show "continuous_on (path_image \) f" ``` lp15@64792 ` 2372` ``` using \path_image \ \ V\ \V \ U\ contf continuous_on_subset by blast ``` lp15@64792 ` 2373` ``` show "continuous_on (f ` path_image \) p'" ``` lp15@64792 ` 2374` ``` apply (rule continuous_on_subset [OF contp']) ``` lp15@64792 ` 2375` ``` apply (auto simp: path_image_def pathfinish_def pathstart_def finW) ``` lp15@64792 ` 2376` ``` done ``` lp15@64792 ` 2377` ``` qed ``` lp15@64792 ` 2378` ``` then show "path (qq +++ (p' \ f \ \))" ``` lp15@64792 ` 2379` ``` using \path \\ \path qq\ paqq path_continuous_image path_join_imp by blast ``` lp15@64792 ` 2380` ``` show "path_image (qq +++ (p' \ f \ \)) \ C" ``` lp15@64792 ` 2381` ``` apply (rule subset_path_image_join) ``` lp15@64792 ` 2382` ``` apply (simp add: \path_image qq \ C\) ``` lp15@64792 ` 2383` ``` by (metis \W' \ C\ \path_image \ \ V\ dual_order.trans fimW(1) image_comp image_mono p'im path_image_compose) ``` lp15@64792 ` 2384` ``` show "pathstart (qq +++ (p' \ f \ \)) = a" ``` lp15@64792 ` 2385` ``` by (simp add: \pathstart qq = a\) ``` lp15@64792 ` 2386` ``` show "p ((qq +++ (p' \ f \ \)) \) = f ((pp +++ \) \)" if \: "\ \ {0..1}" for \ ``` lp15@64792 ` 2387` ``` proof (simp add: joinpaths_def, safe) ``` lp15@64792 ` 2388` ``` show "p (qq (2*\)) = f (pp (2*\))" if "\*2 \ 1" ``` lp15@64792 ` 2389` ``` using \\ \ {0..1}\ pqqeq that by auto ``` lp15@64792 ` 2390` ``` show "p (p' (f (\ (2*\ - 1)))) = f (\ (2*\ - 1))" if "\ \*2 \ 1" ``` lp15@64792 ` 2391` ``` apply (rule homeomorphism_apply2 [OF homUW' finW]) ``` lp15@64792 ` 2392` ``` using that \ by auto ``` lp15@64792 ` 2393` ``` qed ``` lp15@64792 ` 2394` ``` qed ``` lp15@66884 ` 2395` ``` with \pathfinish \ = y'\ \p' (f y') \ X\ show "y' \ l -` X" ``` lp15@64792 ` 2396` ``` unfolding pathfinish_join by (simp add: pathfinish_def) ``` lp15@64792 ` 2397` ``` qed ``` lp15@64792 ` 2398` ``` qed ``` lp15@64792 ` 2399` ``` qed ``` lp15@64792 ` 2400` ``` then show "continuous_on U l" ``` lp15@66884 ` 2401` ``` by (metis IntD1 IntD2 vimage_eq openin_subopen continuous_on_open_gen [OF LC]) ``` lp15@64792 ` 2402` ``` qed ``` lp15@64792 ` 2403` ```qed ``` lp15@64792 ` 2404` lp15@64792 ` 2405` lp15@64792 ` 2406` ```corollary covering_space_lift_stronger: ``` lp15@64792 ` 2407` ``` fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" ``` lp15@64792 ` 2408` ``` and f :: "'c::real_normed_vector \ 'b" ``` lp15@64792 ` 2409` ` assumes cov: "covering_space C p S" "a \ C" "z \