src/HOL/Analysis/Further_Topology.thy
 author nipkow Sat Dec 29 15:43:53 2018 +0100 (6 months ago) changeset 69529 4ab9657b3257 parent 69508 2a4c8a2a3f8e child 69566 c41954ee87cf permissions -rw-r--r--
capitalize proper names in lemma names
 ak2110@68833 ` 1` ```section%important \Extending Continous Maps, Invariance of Domain, etc\ ``` lp15@64006 ` 2` lp15@64006 ` 3` ```text\Ported from HOL Light (moretop.ml) by L C Paulson\ ``` lp15@64006 ` 4` hoelzl@64289 ` 5` ```theory Further_Topology ``` lp15@64291 ` 6` ``` imports Equivalence_Lebesgue_Henstock_Integration Weierstrass_Theorems Polytope Complex_Transcendental ``` lp15@64006 ` 7` ```begin ``` lp15@64006 ` 8` ak2110@68833 ` 9` ```subsection%important\A map from a sphere to a higher dimensional sphere is nullhomotopic\ ``` ak2110@68833 ` 10` ak2110@68833 ` 11` ```lemma%important spheremap_lemma1: ``` lp15@64006 ` 12` ``` fixes f :: "'a::euclidean_space \ 'a::euclidean_space" ``` lp15@64006 ` 13` ``` assumes "subspace S" "subspace T" and dimST: "dim S < dim T" ``` lp15@64006 ` 14` ``` and "S \ T" ``` lp15@64006 ` 15` ``` and diff_f: "f differentiable_on sphere 0 1 \ S" ``` lp15@64006 ` 16` ``` shows "f ` (sphere 0 1 \ S) \ sphere 0 1 \ T" ``` ak2110@68833 ` 17` ```proof%unimportant ``` lp15@64006 ` 18` ``` assume fim: "f ` (sphere 0 1 \ S) = sphere 0 1 \ T" ``` lp15@64006 ` 19` ``` have inS: "\x. \x \ S; x \ 0\ \ (x /\<^sub>R norm x) \ S" ``` lp15@64006 ` 20` ``` using subspace_mul \subspace S\ by blast ``` lp15@64006 ` 21` ``` have subS01: "(\x. x /\<^sub>R norm x) ` (S - {0}) \ sphere 0 1 \ S" ``` lp15@64006 ` 22` ``` using \subspace S\ subspace_mul by fastforce ``` lp15@64006 ` 23` ``` then have diff_f': "f differentiable_on (\x. x /\<^sub>R norm x) ` (S - {0})" ``` lp15@64006 ` 24` ``` by (rule differentiable_on_subset [OF diff_f]) ``` lp15@64006 ` 25` ``` define g where "g \ \x. norm x *\<^sub>R f(inverse(norm x) *\<^sub>R x)" ``` lp15@64006 ` 26` ``` have gdiff: "g differentiable_on S - {0}" ``` lp15@64006 ` 27` ``` unfolding g_def ``` lp15@64006 ` 28` ``` by (rule diff_f' derivative_intros differentiable_on_compose [where f=f] | force)+ ``` lp15@64006 ` 29` ``` have geq: "g ` (S - {0}) = T - {0}" ``` lp15@64006 ` 30` ``` proof ``` lp15@64006 ` 31` ``` have "g ` (S - {0}) \ T" ``` lp15@64006 ` 32` ``` apply (auto simp: g_def subspace_mul [OF \subspace T\]) ``` lp15@64006 ` 33` ``` apply (metis (mono_tags, lifting) DiffI subS01 subspace_mul [OF \subspace T\] fim image_subset_iff inf_le2 singletonD) ``` lp15@64006 ` 34` ``` done ``` lp15@64006 ` 35` ``` moreover have "g ` (S - {0}) \ UNIV - {0}" ``` lp15@64006 ` 36` ``` proof (clarsimp simp: g_def) ``` lp15@64006 ` 37` ``` fix y ``` lp15@64006 ` 38` ``` assume "y \ S" and f0: "f (y /\<^sub>R norm y) = 0" ``` lp15@64006 ` 39` ``` then have "y \ 0 \ y /\<^sub>R norm y \ sphere 0 1 \ S" ``` lp15@64006 ` 40` ``` by (auto simp: subspace_mul [OF \subspace S\]) ``` lp15@64006 ` 41` ``` then show "y = 0" ``` lp15@64006 ` 42` ``` by (metis fim f0 Int_iff image_iff mem_sphere_0 norm_eq_zero zero_neq_one) ``` lp15@64006 ` 43` ``` qed ``` lp15@64006 ` 44` ``` ultimately show "g ` (S - {0}) \ T - {0}" ``` lp15@64006 ` 45` ``` by auto ``` lp15@64006 ` 46` ``` next ``` lp15@64006 ` 47` ``` have *: "sphere 0 1 \ T \ f ` (sphere 0 1 \ S)" ``` lp15@64006 ` 48` ``` using fim by (simp add: image_subset_iff) ``` lp15@64006 ` 49` ``` have "x \ (\x. norm x *\<^sub>R f (x /\<^sub>R norm x)) ` (S - {0})" ``` lp15@64006 ` 50` ``` if "x \ T" "x \ 0" for x ``` lp15@64006 ` 51` ``` proof - ``` lp15@64006 ` 52` ``` have "x /\<^sub>R norm x \ T" ``` lp15@64006 ` 53` ``` using \subspace T\ subspace_mul that by blast ``` lp15@64006 ` 54` ``` then show ?thesis ``` lp15@64006 ` 55` ``` using * [THEN subsetD, of "x /\<^sub>R norm x"] that apply clarsimp ``` lp15@64006 ` 56` ``` apply (rule_tac x="norm x *\<^sub>R xa" in image_eqI, simp) ``` lp15@64006 ` 57` ``` apply (metis norm_eq_zero right_inverse scaleR_one scaleR_scaleR) ``` lp15@64006 ` 58` ``` using \subspace S\ subspace_mul apply force ``` lp15@64006 ` 59` ``` done ``` lp15@64006 ` 60` ``` qed ``` lp15@64006 ` 61` ``` then have "T - {0} \ (\x. norm x *\<^sub>R f (x /\<^sub>R norm x)) ` (S - {0})" ``` lp15@64006 ` 62` ``` by force ``` lp15@64006 ` 63` ``` then show "T - {0} \ g ` (S - {0})" ``` lp15@64006 ` 64` ``` by (simp add: g_def) ``` lp15@64006 ` 65` ``` qed ``` lp15@64006 ` 66` ``` define T' where "T' \ {y. \x \ T. orthogonal x y}" ``` lp15@64006 ` 67` ``` have "subspace T'" ``` lp15@64006 ` 68` ``` by (simp add: subspace_orthogonal_to_vectors T'_def) ``` lp15@64006 ` 69` ``` have dim_eq: "dim T' + dim T = DIM('a)" ``` lp15@64006 ` 70` ``` using dim_subspace_orthogonal_to_vectors [of T UNIV] \subspace T\ ``` immler@68072 ` 71` ``` by (simp add: T'_def) ``` lp15@64006 ` 72` ``` have "\v1 v2. v1 \ span T \ (\w \ span T. orthogonal v2 w) \ x = v1 + v2" for x ``` lp15@64006 ` 73` ``` by (force intro: orthogonal_subspace_decomp_exists [of T x]) ``` lp15@64006 ` 74` ``` then obtain p1 p2 where p1span: "p1 x \ span T" ``` lp15@64006 ` 75` ``` and "\w. w \ span T \ orthogonal (p2 x) w" ``` lp15@64006 ` 76` ``` and eq: "p1 x + p2 x = x" for x ``` lp15@64006 ` 77` ``` by metis ``` lp15@64006 ` 78` ``` then have p1: "\z. p1 z \ T" and ortho: "\w. w \ T \ orthogonal (p2 x) w" for x ``` immler@68072 ` 79` ``` using span_eq_iff \subspace T\ by blast+ ``` lp15@64006 ` 80` ``` then have p2: "\z. p2 z \ T'" ``` lp15@64006 ` 81` ``` by (simp add: T'_def orthogonal_commute) ``` lp15@64006 ` 82` ``` have p12_eq: "\x y. \x \ T; y \ T'\ \ p1(x + y) = x \ p2(x + y) = y" ``` lp15@64006 ` 83` ``` proof (rule orthogonal_subspace_decomp_unique [OF eq p1span, where T=T']) ``` lp15@64006 ` 84` ``` show "\x y. \x \ T; y \ T'\ \ p2 (x + y) \ span T'" ``` immler@68072 ` 85` ``` using span_eq_iff p2 \subspace T'\ by blast ``` lp15@64006 ` 86` ``` show "\a b. \a \ T; b \ T'\ \ orthogonal a b" ``` lp15@64006 ` 87` ``` using T'_def by blast ``` immler@68072 ` 88` ``` qed (auto simp: span_base) ``` lp15@64006 ` 89` ``` then have "\c x. p1 (c *\<^sub>R x) = c *\<^sub>R p1 x \ p2 (c *\<^sub>R x) = c *\<^sub>R p2 x" ``` immler@68072 ` 90` ``` proof - ``` immler@68072 ` 91` ``` fix c :: real and x :: 'a ``` immler@68072 ` 92` ``` have f1: "c *\<^sub>R x = c *\<^sub>R p1 x + c *\<^sub>R p2 x" ``` immler@68072 ` 93` ``` by (metis eq pth_6) ``` immler@68072 ` 94` ``` have f2: "c *\<^sub>R p2 x \ T'" ``` immler@68072 ` 95` ``` by (simp add: \subspace T'\ p2 subspace_scale) ``` immler@68072 ` 96` ``` have "c *\<^sub>R p1 x \ T" ``` immler@68072 ` 97` ``` by (metis (full_types) assms(2) p1span span_eq_iff subspace_scale) ``` immler@68072 ` 98` ``` then show "p1 (c *\<^sub>R x) = c *\<^sub>R p1 x \ p2 (c *\<^sub>R x) = c *\<^sub>R p2 x" ``` immler@68072 ` 99` ``` using f2 f1 p12_eq by presburger ``` immler@68072 ` 100` ``` qed ``` lp15@64006 ` 101` ``` moreover have lin_add: "\x y. p1 (x + y) = p1 x + p1 y \ p2 (x + y) = p2 x + p2 y" ``` lp15@64006 ` 102` ``` proof (rule orthogonal_subspace_decomp_unique [OF _ p1span, where T=T']) ``` lp15@64006 ` 103` ``` show "\x y. p1 (x + y) + p2 (x + y) = p1 x + p1 y + (p2 x + p2 y)" ``` lp15@64006 ` 104` ``` by (simp add: add.assoc add.left_commute eq) ``` lp15@64006 ` 105` ``` show "\a b. \a \ T; b \ T'\ \ orthogonal a b" ``` lp15@64006 ` 106` ``` using T'_def by blast ``` immler@68072 ` 107` ``` qed (auto simp: p1span p2 span_base span_add) ``` lp15@64006 ` 108` ``` ultimately have "linear p1" "linear p2" ``` lp15@64006 ` 109` ``` by unfold_locales auto ``` lp15@64006 ` 110` ``` have "(\z. g (p1 z)) differentiable_on {x + y |x y. x \ S - {0} \ y \ T'}" ``` lp15@64006 ` 111` ``` apply (rule differentiable_on_compose [where f=g]) ``` lp15@64006 ` 112` ``` apply (rule linear_imp_differentiable_on [OF \linear p1\]) ``` lp15@64006 ` 113` ``` apply (rule differentiable_on_subset [OF gdiff]) ``` lp15@64006 ` 114` ``` using p12_eq \S \ T\ apply auto ``` lp15@64006 ` 115` ``` done ``` lp15@64006 ` 116` ``` then have diff: "(\x. g (p1 x) + p2 x) differentiable_on {x + y |x y. x \ S - {0} \ y \ T'}" ``` lp15@64006 ` 117` ``` by (intro derivative_intros linear_imp_differentiable_on [OF \linear p2\]) ``` lp15@64006 ` 118` ``` have "dim {x + y |x y. x \ S - {0} \ y \ T'} \ dim {x + y |x y. x \ S \ y \ T'}" ``` lp15@64006 ` 119` ``` by (blast intro: dim_subset) ``` lp15@64006 ` 120` ``` also have "... = dim S + dim T' - dim (S \ T')" ``` lp15@64006 ` 121` ``` using dim_sums_Int [OF \subspace S\ \subspace T'\] ``` lp15@64006 ` 122` ``` by (simp add: algebra_simps) ``` lp15@64006 ` 123` ``` also have "... < DIM('a)" ``` lp15@64006 ` 124` ``` using dimST dim_eq by auto ``` lp15@64006 ` 125` ``` finally have neg: "negligible {x + y |x y. x \ S - {0} \ y \ T'}" ``` lp15@64006 ` 126` ``` by (rule negligible_lowdim) ``` lp15@64006 ` 127` ``` have "negligible ((\x. g (p1 x) + p2 x) ` {x + y |x y. x \ S - {0} \ y \ T'})" ``` lp15@64006 ` 128` ``` by (rule negligible_differentiable_image_negligible [OF order_refl neg diff]) ``` lp15@64006 ` 129` ``` then have "negligible {x + y |x y. x \ g ` (S - {0}) \ y \ T'}" ``` lp15@64006 ` 130` ``` proof (rule negligible_subset) ``` lp15@64006 ` 131` ``` have "\t' \ T'; s \ S; s \ 0\ ``` lp15@64006 ` 132` ``` \ g s + t' \ (\x. g (p1 x) + p2 x) ` ``` lp15@64006 ` 133` ``` {x + t' |x t'. x \ S \ x \ 0 \ t' \ T'}" for t' s ``` lp15@64006 ` 134` ``` apply (rule_tac x="s + t'" in image_eqI) ``` lp15@64006 ` 135` ``` using \S \ T\ p12_eq by auto ``` lp15@64006 ` 136` ``` then show "{x + y |x y. x \ g ` (S - {0}) \ y \ T'} ``` lp15@64006 ` 137` ``` \ (\x. g (p1 x) + p2 x) ` {x + y |x y. x \ S - {0} \ y \ T'}" ``` lp15@64006 ` 138` ``` by auto ``` lp15@64006 ` 139` ``` qed ``` lp15@64006 ` 140` ``` moreover have "- T' \ {x + y |x y. x \ g ` (S - {0}) \ y \ T'}" ``` lp15@64006 ` 141` ``` proof clarsimp ``` lp15@64006 ` 142` ``` fix z assume "z \ T'" ``` lp15@64006 ` 143` ``` show "\x y. z = x + y \ x \ g ` (S - {0}) \ y \ T'" ``` lp15@64006 ` 144` ``` apply (rule_tac x="p1 z" in exI) ``` lp15@64006 ` 145` ``` apply (rule_tac x="p2 z" in exI) ``` lp15@64006 ` 146` ``` apply (simp add: p1 eq p2 geq) ``` lp15@64006 ` 147` ``` by (metis \z \ T'\ add.left_neutral eq p2) ``` lp15@64006 ` 148` ``` qed ``` lp15@64006 ` 149` ``` ultimately have "negligible (-T')" ``` lp15@64006 ` 150` ``` using negligible_subset by blast ``` lp15@64006 ` 151` ``` moreover have "negligible T'" ``` lp15@64006 ` 152` ``` using negligible_lowdim ``` lp15@64006 ` 153` ``` by (metis add.commute assms(3) diff_add_inverse2 diff_self_eq_0 dim_eq le_add1 le_antisym linordered_semidom_class.add_diff_inverse not_less0) ``` lp15@64006 ` 154` ``` ultimately have "negligible (-T' \ T')" ``` lp15@64006 ` 155` ``` by (metis negligible_Un_eq) ``` lp15@64006 ` 156` ``` then show False ``` lp15@64006 ` 157` ``` using negligible_Un_eq non_negligible_UNIV by simp ``` lp15@64006 ` 158` ```qed ``` lp15@64006 ` 159` lp15@64006 ` 160` ak2110@68833 ` 161` ```lemma%important spheremap_lemma2: ``` lp15@64006 ` 162` ``` fixes f :: "'a::euclidean_space \ 'a::euclidean_space" ``` lp15@64006 ` 163` ``` assumes ST: "subspace S" "subspace T" "dim S < dim T" ``` lp15@64006 ` 164` ``` and "S \ T" ``` lp15@64006 ` 165` ``` and contf: "continuous_on (sphere 0 1 \ S) f" ``` lp15@64006 ` 166` ``` and fim: "f ` (sphere 0 1 \ S) \ sphere 0 1 \ T" ``` lp15@64006 ` 167` ``` shows "\c. homotopic_with (\x. True) (sphere 0 1 \ S) (sphere 0 1 \ T) f (\x. c)" ``` ak2110@68833 ` 168` ```proof%unimportant - ``` lp15@64006 ` 169` ``` have [simp]: "\x. \norm x = 1; x \ S\ \ norm (f x) = 1" ``` lp15@64006 ` 170` ``` using fim by (simp add: image_subset_iff) ``` lp15@64006 ` 171` ``` have "compact (sphere 0 1 \ S)" ``` lp15@64006 ` 172` ``` by (simp add: \subspace S\ closed_subspace compact_Int_closed) ``` lp15@64006 ` 173` ``` then obtain g where pfg: "polynomial_function g" and gim: "g ` (sphere 0 1 \ S) \ T" ``` lp15@64006 ` 174` ``` and g12: "\x. x \ sphere 0 1 \ S \ norm(f x - g x) < 1/2" ``` lp15@64006 ` 175` ``` apply (rule Stone_Weierstrass_polynomial_function_subspace [OF _ contf _ \subspace T\, of "1/2"]) ``` lp15@64006 ` 176` ``` using fim apply auto ``` lp15@64006 ` 177` ``` done ``` lp15@64006 ` 178` ``` have gnz: "g x \ 0" if "x \ sphere 0 1 \ S" for x ``` lp15@64006 ` 179` ``` proof - ``` lp15@64006 ` 180` ``` have "norm (f x) = 1" ``` lp15@64006 ` 181` ``` using fim that by (simp add: image_subset_iff) ``` lp15@64006 ` 182` ``` then show ?thesis ``` lp15@64006 ` 183` ``` using g12 [OF that] by auto ``` lp15@64006 ` 184` ``` qed ``` lp15@64006 ` 185` ``` have diffg: "g differentiable_on sphere 0 1 \ S" ``` lp15@64006 ` 186` ``` by (metis pfg differentiable_on_polynomial_function) ``` lp15@64006 ` 187` ``` define h where "h \ \x. inverse(norm(g x)) *\<^sub>R g x" ``` lp15@64006 ` 188` ``` have h: "x \ sphere 0 1 \ S \ h x \ sphere 0 1 \ T" for x ``` lp15@64006 ` 189` ``` unfolding h_def ``` lp15@64006 ` 190` ``` using gnz [of x] ``` lp15@64006 ` 191` ``` by (auto simp: subspace_mul [OF \subspace T\] subsetD [OF gim]) ``` lp15@64006 ` 192` ``` have diffh: "h differentiable_on sphere 0 1 \ S" ``` lp15@64006 ` 193` ``` unfolding h_def ``` lp15@64006 ` 194` ``` apply (intro derivative_intros diffg differentiable_on_compose [OF diffg]) ``` lp15@64006 ` 195` ``` using gnz apply auto ``` lp15@64006 ` 196` ``` done ``` lp15@64006 ` 197` ``` have homfg: "homotopic_with (\z. True) (sphere 0 1 \ S) (T - {0}) f g" ``` lp15@64006 ` 198` ``` proof (rule homotopic_with_linear [OF contf]) ``` lp15@64006 ` 199` ``` show "continuous_on (sphere 0 1 \ S) g" ``` lp15@64006 ` 200` ``` using pfg by (simp add: differentiable_imp_continuous_on diffg) ``` lp15@64006 ` 201` ``` next ``` lp15@64006 ` 202` ``` have non0fg: "0 \ closed_segment (f x) (g x)" if "norm x = 1" "x \ S" for x ``` lp15@64006 ` 203` ``` proof - ``` lp15@64006 ` 204` ``` have "f x \ sphere 0 1" ``` lp15@64006 ` 205` ``` using fim that by (simp add: image_subset_iff) ``` lp15@64006 ` 206` ``` moreover have "norm(f x - g x) < 1/2" ``` lp15@64006 ` 207` ``` apply (rule g12) ``` lp15@64006 ` 208` ``` using that by force ``` lp15@64006 ` 209` ``` ultimately show ?thesis ``` lp15@64006 ` 210` ``` by (auto simp: norm_minus_commute dest: segment_bound) ``` lp15@64006 ` 211` ``` qed ``` lp15@64006 ` 212` ``` show "\x. x \ sphere 0 1 \ S \ closed_segment (f x) (g x) \ T - {0}" ``` lp15@64006 ` 213` ``` apply (simp add: subset_Diff_insert non0fg) ``` lp15@64006 ` 214` ``` apply (simp add: segment_convex_hull) ``` lp15@64006 ` 215` ``` apply (rule hull_minimal) ``` lp15@64006 ` 216` ``` using fim image_eqI gim apply force ``` lp15@64006 ` 217` ``` apply (rule subspace_imp_convex [OF \subspace T\]) ``` lp15@64006 ` 218` ``` done ``` lp15@64006 ` 219` ``` qed ``` lp15@64006 ` 220` ``` obtain d where d: "d \ (sphere 0 1 \ T) - h ` (sphere 0 1 \ S)" ``` lp15@64006 ` 221` ``` using h spheremap_lemma1 [OF ST \S \ T\ diffh] by force ``` lp15@64006 ` 222` ``` then have non0hd: "0 \ closed_segment (h x) (- d)" if "norm x = 1" "x \ S" for x ``` lp15@64006 ` 223` ``` using midpoint_between [of 0 "h x" "-d"] that h [of x] ``` lp15@64006 ` 224` ``` by (auto simp: between_mem_segment midpoint_def) ``` lp15@64006 ` 225` ``` have conth: "continuous_on (sphere 0 1 \ S) h" ``` lp15@64006 ` 226` ``` using differentiable_imp_continuous_on diffh by blast ``` lp15@64006 ` 227` ``` have hom_hd: "homotopic_with (\z. True) (sphere 0 1 \ S) (T - {0}) h (\x. -d)" ``` lp15@64006 ` 228` ``` apply (rule homotopic_with_linear [OF conth continuous_on_const]) ``` lp15@64006 ` 229` ``` apply (simp add: subset_Diff_insert non0hd) ``` lp15@64006 ` 230` ``` apply (simp add: segment_convex_hull) ``` lp15@64006 ` 231` ``` apply (rule hull_minimal) ``` lp15@64006 ` 232` ``` using h d apply (force simp: subspace_neg [OF \subspace T\]) ``` lp15@64006 ` 233` ``` apply (rule subspace_imp_convex [OF \subspace T\]) ``` lp15@64006 ` 234` ``` done ``` lp15@64006 ` 235` ``` have conT0: "continuous_on (T - {0}) (\y. inverse(norm y) *\<^sub>R y)" ``` lp15@64006 ` 236` ``` by (intro continuous_intros) auto ``` lp15@64006 ` 237` ``` have sub0T: "(\y. y /\<^sub>R norm y) ` (T - {0}) \ sphere 0 1 \ T" ``` lp15@64006 ` 238` ``` by (fastforce simp: assms(2) subspace_mul) ``` lp15@64006 ` 239` ``` obtain c where homhc: "homotopic_with (\z. True) (sphere 0 1 \ S) (sphere 0 1 \ T) h (\x. c)" ``` lp15@64006 ` 240` ``` apply (rule_tac c="-d" in that) ``` lp15@64006 ` 241` ``` apply (rule homotopic_with_eq) ``` lp15@64006 ` 242` ``` apply (rule homotopic_compose_continuous_left [OF hom_hd conT0 sub0T]) ``` lp15@64006 ` 243` ``` using d apply (auto simp: h_def) ``` lp15@64006 ` 244` ``` done ``` lp15@64006 ` 245` ``` show ?thesis ``` lp15@64006 ` 246` ``` apply (rule_tac x=c in exI) ``` lp15@64006 ` 247` ``` apply (rule homotopic_with_trans [OF _ homhc]) ``` lp15@64006 ` 248` ``` apply (rule homotopic_with_eq) ``` lp15@64006 ` 249` ``` apply (rule homotopic_compose_continuous_left [OF homfg conT0 sub0T]) ``` lp15@64006 ` 250` ``` apply (auto simp: h_def) ``` lp15@64006 ` 251` ``` done ``` lp15@64006 ` 252` ```qed ``` lp15@64006 ` 253` lp15@64006 ` 254` ak2110@68833 ` 255` ```lemma%important spheremap_lemma3: ``` lp15@64006 ` 256` ``` assumes "bounded S" "convex S" "subspace U" and affSU: "aff_dim S \ dim U" ``` lp15@64006 ` 257` ``` obtains T where "subspace T" "T \ U" "S \ {} \ aff_dim T = aff_dim S" ``` lp15@64006 ` 258` ``` "(rel_frontier S) homeomorphic (sphere 0 1 \ T)" ``` ak2110@68833 ` 259` ```proof%unimportant (cases "S = {}") ``` lp15@64006 ` 260` ``` case True ``` lp15@64006 ` 261` ``` with \subspace U\ subspace_0 show ?thesis ``` lp15@64006 ` 262` ``` by (rule_tac T = "{0}" in that) auto ``` lp15@64006 ` 263` ```next ``` lp15@64006 ` 264` ``` case False ``` lp15@64006 ` 265` ``` then obtain a where "a \ S" ``` lp15@64006 ` 266` ``` by auto ``` lp15@64006 ` 267` ``` then have affS: "aff_dim S = int (dim ((\x. -a+x) ` S))" ``` lp15@64006 ` 268` ``` by (metis hull_inc aff_dim_eq_dim) ``` lp15@64006 ` 269` ``` with affSU have "dim ((\x. -a+x) ` S) \ dim U" ``` lp15@64006 ` 270` ``` by linarith ``` lp15@64006 ` 271` ``` with choose_subspace_of_subspace ``` lp15@64006 ` 272` ``` obtain T where "subspace T" "T \ span U" and dimT: "dim T = dim ((\x. -a+x) ` S)" . ``` lp15@64006 ` 273` ``` show ?thesis ``` lp15@64006 ` 274` ``` proof (rule that [OF \subspace T\]) ``` lp15@64006 ` 275` ``` show "T \ U" ``` immler@68072 ` 276` ``` using span_eq_iff \subspace U\ \T \ span U\ by blast ``` lp15@64006 ` 277` ``` show "aff_dim T = aff_dim S" ``` lp15@64006 ` 278` ``` using dimT \subspace T\ affS aff_dim_subspace by fastforce ``` lp15@64006 ` 279` ``` show "rel_frontier S homeomorphic sphere 0 1 \ T" ``` lp15@64006 ` 280` ``` proof - ``` lp15@64006 ` 281` ``` have "aff_dim (ball 0 1 \ T) = aff_dim (T)" ``` lp15@64006 ` 282` ``` by (metis IntI interior_ball \subspace T\ aff_dim_convex_Int_nonempty_interior centre_in_ball empty_iff inf_commute subspace_0 subspace_imp_convex zero_less_one) ``` lp15@64006 ` 283` ``` then have affS_eq: "aff_dim S = aff_dim (ball 0 1 \ T)" ``` lp15@64006 ` 284` ``` using \aff_dim T = aff_dim S\ by simp ``` lp15@64006 ` 285` ``` have "rel_frontier S homeomorphic rel_frontier(ball 0 1 \ T)" ``` lp15@64006 ` 286` ``` apply (rule homeomorphic_rel_frontiers_convex_bounded_sets [OF \convex S\ \bounded S\]) ``` lp15@64006 ` 287` ``` apply (simp add: \subspace T\ convex_Int subspace_imp_convex) ``` lp15@64006 ` 288` ``` apply (simp add: bounded_Int) ``` lp15@64006 ` 289` ``` apply (rule affS_eq) ``` lp15@64006 ` 290` ``` done ``` lp15@64006 ` 291` ``` also have "... = frontier (ball 0 1) \ T" ``` lp15@64006 ` 292` ``` apply (rule convex_affine_rel_frontier_Int [OF convex_ball]) ``` lp15@64006 ` 293` ``` apply (simp add: \subspace T\ subspace_imp_affine) ``` lp15@64006 ` 294` ``` using \subspace T\ subspace_0 by force ``` lp15@64006 ` 295` ``` also have "... = sphere 0 1 \ T" ``` lp15@64006 ` 296` ``` by auto ``` lp15@64006 ` 297` ``` finally show ?thesis . ``` lp15@64006 ` 298` ``` qed ``` lp15@64006 ` 299` ``` qed ``` lp15@64006 ` 300` ```qed ``` lp15@64006 ` 301` lp15@64006 ` 302` ak2110@68833 ` 303` ```proposition%important inessential_spheremap_lowdim_gen: ``` lp15@64006 ` 304` ``` fixes f :: "'M::euclidean_space \ 'a::euclidean_space" ``` lp15@64006 ` 305` ``` assumes "convex S" "bounded S" "convex T" "bounded T" ``` lp15@64006 ` 306` ``` and affST: "aff_dim S < aff_dim T" ``` lp15@64006 ` 307` ``` and contf: "continuous_on (rel_frontier S) f" ``` lp15@64006 ` 308` ``` and fim: "f ` (rel_frontier S) \ rel_frontier T" ``` lp15@64006 ` 309` ``` obtains c where "homotopic_with (\z. True) (rel_frontier S) (rel_frontier T) f (\x. c)" ``` ak2110@68833 ` 310` ```proof%unimportant (cases "S = {}") ``` lp15@64006 ` 311` ``` case True ``` lp15@64006 ` 312` ``` then show ?thesis ``` lp15@64006 ` 313` ``` by (simp add: that) ``` lp15@64006 ` 314` ```next ``` lp15@64006 ` 315` ``` case False ``` lp15@64006 ` 316` ``` then show ?thesis ``` lp15@64006 ` 317` ``` proof (cases "T = {}") ``` lp15@64006 ` 318` ``` case True ``` lp15@64006 ` 319` ``` then show ?thesis ``` lp15@64006 ` 320` ``` using fim that by auto ``` lp15@64006 ` 321` ``` next ``` lp15@64006 ` 322` ``` case False ``` lp15@64006 ` 323` ``` obtain T':: "'a set" ``` lp15@64006 ` 324` ``` where "subspace T'" and affT': "aff_dim T' = aff_dim T" ``` lp15@64006 ` 325` ``` and homT: "rel_frontier T homeomorphic sphere 0 1 \ T'" ``` lp15@64006 ` 326` ``` apply (rule spheremap_lemma3 [OF \bounded T\ \convex T\ subspace_UNIV, where 'b='a]) ``` immler@68072 ` 327` ``` apply (simp add: aff_dim_le_DIM) ``` lp15@64006 ` 328` ``` using \T \ {}\ by blast ``` lp15@64006 ` 329` ``` with homeomorphic_imp_homotopy_eqv ``` lp15@64006 ` 330` ``` have relT: "sphere 0 1 \ T' homotopy_eqv rel_frontier T" ``` lp15@64006 ` 331` ``` using homotopy_eqv_sym by blast ``` lp15@64006 ` 332` ``` have "aff_dim S \ int (dim T')" ``` lp15@64006 ` 333` ``` using affT' \subspace T'\ affST aff_dim_subspace by force ``` lp15@64006 ` 334` ``` with spheremap_lemma3 [OF \bounded S\ \convex S\ \subspace T'\] \S \ {}\ ``` lp15@64006 ` 335` ``` obtain S':: "'a set" where "subspace S'" "S' \ T'" ``` lp15@64006 ` 336` ``` and affS': "aff_dim S' = aff_dim S" ``` lp15@64006 ` 337` ``` and homT: "rel_frontier S homeomorphic sphere 0 1 \ S'" ``` lp15@64006 ` 338` ``` by metis ``` lp15@64006 ` 339` ``` with homeomorphic_imp_homotopy_eqv ``` lp15@64006 ` 340` ``` have relS: "sphere 0 1 \ S' homotopy_eqv rel_frontier S" ``` lp15@64006 ` 341` ``` using homotopy_eqv_sym by blast ``` lp15@64006 ` 342` ``` have dimST': "dim S' < dim T'" ``` lp15@64006 ` 343` ``` by (metis \S' \ T'\ \subspace S'\ \subspace T'\ affS' affST affT' less_irrefl not_le subspace_dim_equal) ``` lp15@64006 ` 344` ``` have "\c. homotopic_with (\z. True) (rel_frontier S) (rel_frontier T) f (\x. c)" ``` lp15@64006 ` 345` ``` apply (rule homotopy_eqv_homotopic_triviality_null_imp [OF relT contf fim]) ``` lp15@64006 ` 346` ``` apply (rule homotopy_eqv_cohomotopic_triviality_null[OF relS, THEN iffD1, rule_format]) ``` lp15@64006 ` 347` ``` apply (metis dimST' \subspace S'\ \subspace T'\ \S' \ T'\ spheremap_lemma2, blast) ``` lp15@64006 ` 348` ``` done ``` lp15@64006 ` 349` ``` with that show ?thesis by blast ``` lp15@64006 ` 350` ``` qed ``` lp15@64006 ` 351` ```qed ``` lp15@64006 ` 352` ak2110@68833 ` 353` ```lemma%unimportant inessential_spheremap_lowdim: ``` lp15@64006 ` 354` ``` fixes f :: "'M::euclidean_space \ 'a::euclidean_space" ``` lp15@64006 ` 355` ``` assumes ``` lp15@64006 ` 356` ``` "DIM('M) < DIM('a)" and f: "continuous_on (sphere a r) f" "f ` (sphere a r) \ (sphere b s)" ``` lp15@64006 ` 357` ``` obtains c where "homotopic_with (\z. True) (sphere a r) (sphere b s) f (\x. c)" ``` lp15@64006 ` 358` ```proof (cases "s \ 0") ``` lp15@64006 ` 359` ``` case True then show ?thesis ``` lp15@64006 ` 360` ``` by (meson nullhomotopic_into_contractible f contractible_sphere that) ``` lp15@64006 ` 361` ```next ``` lp15@64006 ` 362` ``` case False ``` lp15@64006 ` 363` ``` show ?thesis ``` lp15@64006 ` 364` ``` proof (cases "r \ 0") ``` lp15@64006 ` 365` ``` case True then show ?thesis ``` lp15@64006 ` 366` ``` by (meson f nullhomotopic_from_contractible contractible_sphere that) ``` lp15@64006 ` 367` ``` next ``` lp15@64006 ` 368` ``` case False ``` nipkow@69508 ` 369` ``` with \\ s \ 0\ have "r > 0" "s > 0" by auto ``` lp15@64006 ` 370` ``` show ?thesis ``` lp15@64006 ` 371` ``` apply (rule inessential_spheremap_lowdim_gen [of "cball a r" "cball b s" f]) ``` lp15@64006 ` 372` ``` using \0 < r\ \0 < s\ assms(1) ``` lp15@64006 ` 373` ``` apply (simp_all add: f aff_dim_cball) ``` lp15@64006 ` 374` ``` using that by blast ``` lp15@64006 ` 375` ``` qed ``` lp15@64006 ` 376` ```qed ``` lp15@64006 ` 377` lp15@64006 ` 378` lp15@64006 ` 379` ak2110@68833 ` 380` ```subsection%important\ Some technical lemmas about extending maps from cell complexes\ ``` ak2110@68833 ` 381` ak2110@68833 ` 382` ```lemma%unimportant extending_maps_Union_aux: ``` lp15@64006 ` 383` ``` assumes fin: "finite \" ``` lp15@64006 ` 384` ``` and "\S. S \ \ \ closed S" ``` lp15@64006 ` 385` ``` and "\S T. \S \ \; T \ \; S \ T\ \ S \ T \ K" ``` lp15@64006 ` 386` ``` and "\S. S \ \ \ \g. continuous_on S g \ g ` S \ T \ (\x \ S \ K. g x = h x)" ``` lp15@64006 ` 387` ``` shows "\g. continuous_on (\\) g \ g ` (\\) \ T \ (\x \ \\ \ K. g x = h x)" ``` lp15@64006 ` 388` ```using assms ``` lp15@64006 ` 389` ```proof (induction \) ``` lp15@64006 ` 390` ``` case empty show ?case by simp ``` lp15@64006 ` 391` ```next ``` lp15@64006 ` 392` ``` case (insert S \) ``` lp15@64006 ` 393` ``` then obtain f where contf: "continuous_on (S) f" and fim: "f ` S \ T" and feq: "\x \ S \ K. f x = h x" ``` lp15@64006 ` 394` ``` by (meson insertI1) ``` lp15@64006 ` 395` ``` obtain g where contg: "continuous_on (\\) g" and gim: "g ` \\ \ T" and geq: "\x \ \\ \ K. g x = h x" ``` lp15@64006 ` 396` ``` using insert by auto ``` lp15@64006 ` 397` ``` have fg: "f x = g x" if "x \ T" "T \ \" "x \ S" for x T ``` lp15@64006 ` 398` ``` proof - ``` lp15@64006 ` 399` ``` have "T \ S \ K \ S = T" ``` lp15@64006 ` 400` ``` using that by (metis (no_types) insert.prems(2) insertCI) ``` lp15@64006 ` 401` ``` then show ?thesis ``` lp15@64006 ` 402` ``` using UnionI feq geq \S \ \\ subsetD that by fastforce ``` lp15@64006 ` 403` ``` qed ``` lp15@64006 ` 404` ``` show ?case ``` lp15@64006 ` 405` ``` apply (rule_tac x="\x. if x \ S then f x else g x" in exI, simp) ``` lp15@64006 ` 406` ``` apply (intro conjI continuous_on_cases) ``` lp15@64006 ` 407` ``` apply (simp_all add: insert closed_Union contf contg) ``` lp15@64006 ` 408` ``` using fim gim feq geq ``` lp15@64006 ` 409` ``` apply (force simp: insert closed_Union contf contg inf_commute intro: fg)+ ``` lp15@64006 ` 410` ``` done ``` lp15@64006 ` 411` ```qed ``` lp15@64006 ` 412` ak2110@68833 ` 413` ```lemma%unimportant extending_maps_Union: ``` lp15@64006 ` 414` ``` assumes fin: "finite \" ``` lp15@64006 ` 415` ``` and "\S. S \ \ \ \g. continuous_on S g \ g ` S \ T \ (\x \ S \ K. g x = h x)" ``` lp15@64006 ` 416` ``` and "\S. S \ \ \ closed S" ``` nipkow@69508 ` 417` ``` and K: "\X Y. \X \ \; Y \ \; \ X \ Y; \ Y \ X\ \ X \ Y \ K" ``` lp15@64006 ` 418` ``` shows "\g. continuous_on (\\) g \ g ` (\\) \ T \ (\x \ \\ \ K. g x = h x)" ``` lp15@64006 ` 419` ```apply (simp add: Union_maximal_sets [OF fin, symmetric]) ``` lp15@64006 ` 420` ```apply (rule extending_maps_Union_aux) ``` lp15@64006 ` 421` ```apply (simp_all add: Union_maximal_sets [OF fin] assms) ``` lp15@64006 ` 422` ```by (metis K psubsetI) ``` lp15@64006 ` 423` lp15@64006 ` 424` ak2110@68833 ` 425` ```lemma%important extend_map_lemma: ``` lp15@64006 ` 426` ``` assumes "finite \" "\ \ \" "convex T" "bounded T" ``` lp15@64006 ` 427` ``` and poly: "\X. X \ \ \ polytope X" ``` lp15@64006 ` 428` ``` and aff: "\X. X \ \ - \ \ aff_dim X < aff_dim T" ``` lp15@64006 ` 429` ``` and face: "\S T. \S \ \; T \ \\ \ (S \ T) face_of S \ (S \ T) face_of T" ``` lp15@64006 ` 430` ``` and contf: "continuous_on (\\) f" and fim: "f ` (\\) \ rel_frontier T" ``` lp15@64006 ` 431` ``` obtains g where "continuous_on (\\) g" "g ` (\\) \ rel_frontier T" "\x. x \ \\ \ g x = f x" ``` ak2110@68833 ` 432` ```proof%unimportant (cases "\ - \ = {}") ``` lp15@64006 ` 433` ``` case True ``` lp15@64006 ` 434` ``` then have "\\ \ \\" ``` lp15@64006 ` 435` ``` by (simp add: Union_mono) ``` lp15@64006 ` 436` ``` then show ?thesis ``` lp15@64006 ` 437` ``` apply (rule_tac g=f in that) ``` lp15@64006 ` 438` ``` using contf continuous_on_subset apply blast ``` lp15@64006 ` 439` ``` using fim apply blast ``` lp15@64006 ` 440` ``` by simp ``` lp15@64006 ` 441` ```next ``` lp15@64006 ` 442` ``` case False ``` lp15@64006 ` 443` ``` then have "0 \ aff_dim T" ``` lp15@64006 ` 444` ``` by (metis aff aff_dim_empty aff_dim_geq aff_dim_negative_iff all_not_in_conv not_less) ``` lp15@64006 ` 445` ``` then obtain i::nat where i: "int i = aff_dim T" ``` lp15@64006 ` 446` ``` by (metis nonneg_eq_int) ``` lp15@64006 ` 447` ``` have Union_empty_eq: "\{D. D = {} \ P D} = {}" for P :: "'a set \ bool" ``` lp15@64006 ` 448` ``` by auto ``` lp15@64006 ` 449` ``` have extendf: "\g. continuous_on (\(\ \ {D. \C \ \. D face_of C \ aff_dim D < i})) g \ ``` lp15@64006 ` 450` ``` g ` (\ (\ \ {D. \C \ \. D face_of C \ aff_dim D < i})) \ rel_frontier T \ ``` lp15@64006 ` 451` ``` (\x \ \\. g x = f x)" ``` lp15@64006 ` 452` ``` if "i \ aff_dim T" for i::nat ``` lp15@64006 ` 453` ``` using that ``` lp15@64006 ` 454` ``` proof (induction i) ``` lp15@64006 ` 455` ``` case 0 then show ?case ``` lp15@64006 ` 456` ``` apply (simp add: Union_empty_eq) ``` lp15@64006 ` 457` ``` apply (rule_tac x=f in exI) ``` lp15@64006 ` 458` ``` apply (intro conjI) ``` lp15@64006 ` 459` ``` using contf continuous_on_subset apply blast ``` lp15@64006 ` 460` ``` using fim apply blast ``` lp15@64006 ` 461` ``` by simp ``` lp15@64006 ` 462` ``` next ``` lp15@64006 ` 463` ``` case (Suc p) ``` lp15@64006 ` 464` ``` with \bounded T\ have "rel_frontier T \ {}" ``` lp15@64006 ` 465` ``` by (auto simp: rel_frontier_eq_empty affine_bounded_eq_lowdim [of T]) ``` lp15@64006 ` 466` ``` then obtain t where t: "t \ rel_frontier T" by auto ``` lp15@64006 ` 467` ``` have ple: "int p \ aff_dim T" using Suc.prems by force ``` lp15@64006 ` 468` ``` obtain h where conth: "continuous_on (\(\ \ {D. \C \ \. D face_of C \ aff_dim D < p})) h" ``` lp15@64006 ` 469` ``` and him: "h ` (\ (\ \ {D. \C \ \. D face_of C \ aff_dim D < p})) ``` lp15@64006 ` 470` ``` \ rel_frontier T" ``` lp15@64006 ` 471` ``` and heq: "\x. x \ \\ \ h x = f x" ``` lp15@64006 ` 472` ``` using Suc.IH [OF ple] by auto ``` lp15@64006 ` 473` ``` let ?Faces = "{D. \C \ \. D face_of C \ aff_dim D \ p}" ``` lp15@64006 ` 474` ``` have extendh: "\g. continuous_on D g \ ``` lp15@64006 ` 475` ``` g ` D \ rel_frontier T \ ``` lp15@64006 ` 476` ``` (\x \ D \ \(\ \ {D. \C \ \. D face_of C \ aff_dim D < p}). g x = h x)" ``` lp15@64006 ` 477` ``` if D: "D \ \ \ ?Faces" for D ``` lp15@64006 ` 478` ``` proof (cases "D \ \(\ \ {D. \C \ \. D face_of C \ aff_dim D < p})") ``` lp15@64006 ` 479` ``` case True ``` lp15@64006 ` 480` ``` then show ?thesis ``` lp15@64006 ` 481` ``` apply (rule_tac x=h in exI) ``` lp15@64006 ` 482` ``` apply (intro conjI) ``` lp15@64006 ` 483` ``` apply (blast intro: continuous_on_subset [OF conth]) ``` lp15@64006 ` 484` ``` using him apply blast ``` lp15@64006 ` 485` ``` by simp ``` lp15@64006 ` 486` ``` next ``` lp15@64006 ` 487` ``` case False ``` lp15@64006 ` 488` ``` note notDsub = False ``` lp15@64006 ` 489` ``` show ?thesis ``` lp15@64006 ` 490` ``` proof (cases "\a. D = {a}") ``` lp15@64006 ` 491` ``` case True ``` lp15@64006 ` 492` ``` then obtain a where "D = {a}" by auto ``` lp15@64006 ` 493` ``` with notDsub t show ?thesis ``` lp15@64006 ` 494` ``` by (rule_tac x="\x. t" in exI) simp ``` lp15@64006 ` 495` ``` next ``` lp15@64006 ` 496` ``` case False ``` lp15@64006 ` 497` ``` have "D \ {}" using notDsub by auto ``` lp15@64006 ` 498` ``` have Dnotin: "D \ \ \ {D. \C \ \. D face_of C \ aff_dim D < p}" ``` lp15@64006 ` 499` ``` using notDsub by auto ``` lp15@64006 ` 500` ``` then have "D \ \" by simp ``` lp15@64006 ` 501` ``` have "D \ ?Faces - {D. \C \ \. D face_of C \ aff_dim D < p}" ``` lp15@64006 ` 502` ``` using Dnotin that by auto ``` lp15@64006 ` 503` ``` then obtain C where "C \ \" "D face_of C" and affD: "aff_dim D = int p" ``` lp15@64006 ` 504` ``` by auto ``` lp15@64006 ` 505` ``` then have "bounded D" ``` lp15@64006 ` 506` ``` using face_of_polytope_polytope poly polytope_imp_bounded by blast ``` lp15@64006 ` 507` ``` then have [simp]: "\ affine D" ``` lp15@64006 ` 508` ``` using affine_bounded_eq_trivial False \D \ {}\ \bounded D\ by blast ``` lp15@64006 ` 509` ``` have "{F. F facet_of D} \ {E. E face_of C \ aff_dim E < int p}" ``` lp15@64006 ` 510` ``` apply clarify ``` lp15@64006 ` 511` ``` apply (metis \D face_of C\ affD eq_iff face_of_trans facet_of_def zle_diff1_eq) ``` lp15@64006 ` 512` ``` done ``` lp15@64006 ` 513` ``` moreover have "polyhedron D" ``` lp15@64006 ` 514` ``` using \C \ \\ \D face_of C\ face_of_polytope_polytope poly polytope_imp_polyhedron by auto ``` lp15@64006 ` 515` ``` ultimately have relf_sub: "rel_frontier D \ \ {E. E face_of C \ aff_dim E < p}" ``` lp15@64006 ` 516` ``` by (simp add: rel_frontier_of_polyhedron Union_mono) ``` lp15@64006 ` 517` ``` then have him_relf: "h ` rel_frontier D \ rel_frontier T" ``` lp15@64006 ` 518` ``` using \C \ \\ him by blast ``` lp15@64006 ` 519` ``` have "convex D" ``` lp15@64006 ` 520` ``` by (simp add: \polyhedron D\ polyhedron_imp_convex) ``` lp15@64006 ` 521` ``` have affD_lessT: "aff_dim D < aff_dim T" ``` lp15@64006 ` 522` ``` using Suc.prems affD by linarith ``` lp15@64006 ` 523` ``` have contDh: "continuous_on (rel_frontier D) h" ``` lp15@64006 ` 524` ``` using \C \ \\ relf_sub by (blast intro: continuous_on_subset [OF conth]) ``` lp15@64006 ` 525` ``` then have *: "(\c. homotopic_with (\x. True) (rel_frontier D) (rel_frontier T) h (\x. c)) = ``` lp15@64006 ` 526` ``` (\g. continuous_on UNIV g \ range g \ rel_frontier T \ ``` lp15@64006 ` 527` ``` (\x\rel_frontier D. g x = h x))" ``` lp15@64006 ` 528` ``` apply (rule nullhomotopic_into_rel_frontier_extension [OF closed_rel_frontier]) ``` lp15@64006 ` 529` ``` apply (simp_all add: assms rel_frontier_eq_empty him_relf) ``` lp15@64006 ` 530` ``` done ``` lp15@64006 ` 531` ``` have "(\c. homotopic_with (\x. True) (rel_frontier D) ``` lp15@64006 ` 532` ``` (rel_frontier T) h (\x. c))" ``` lp15@64006 ` 533` ``` by (metis inessential_spheremap_lowdim_gen ``` lp15@64006 ` 534` ``` [OF \convex D\ \bounded D\ \convex T\ \bounded T\ affD_lessT contDh him_relf]) ``` lp15@64006 ` 535` ``` then obtain g where contg: "continuous_on UNIV g" ``` lp15@64006 ` 536` ``` and gim: "range g \ rel_frontier T" ``` lp15@64006 ` 537` ``` and gh: "\x. x \ rel_frontier D \ g x = h x" ``` lp15@64006 ` 538` ``` by (metis *) ``` lp15@64006 ` 539` ``` have "D \ E \ rel_frontier D" ``` nipkow@67399 ` 540` ``` if "E \ \ \ {D. Bex \ ((face_of) D) \ aff_dim D < int p}" for E ``` lp15@64006 ` 541` ``` proof (rule face_of_subset_rel_frontier) ``` lp15@64006 ` 542` ``` show "D \ E face_of D" ``` lp15@64006 ` 543` ``` using that \C \ \\ \D face_of C\ face ``` lp15@64006 ` 544` ``` apply auto ``` lp15@64006 ` 545` ``` apply (meson face_of_Int_subface \\ \ \\ face_of_refl_eq poly polytope_imp_convex subsetD) ``` lp15@64006 ` 546` ``` using face_of_Int_subface apply blast ``` lp15@64006 ` 547` ``` done ``` lp15@64006 ` 548` ``` show "D \ E \ D" ``` lp15@64006 ` 549` ``` using that notDsub by auto ``` lp15@64006 ` 550` ``` qed ``` lp15@64006 ` 551` ``` then show ?thesis ``` lp15@64006 ` 552` ``` apply (rule_tac x=g in exI) ``` lp15@64006 ` 553` ``` apply (intro conjI ballI) ``` lp15@64006 ` 554` ``` using continuous_on_subset contg apply blast ``` lp15@64006 ` 555` ``` using gim apply blast ``` lp15@64006 ` 556` ``` using gh by fastforce ``` lp15@64006 ` 557` ``` qed ``` lp15@64006 ` 558` ``` qed ``` lp15@64006 ` 559` ``` have intle: "i < 1 + int j \ i \ int j" for i j ``` lp15@64006 ` 560` ``` by auto ``` lp15@64006 ` 561` ``` have "finite \" ``` lp15@64006 ` 562` ``` using \finite \\ \\ \ \\ rev_finite_subset by blast ``` lp15@64006 ` 563` ``` then have fin: "finite (\ \ ?Faces)" ``` lp15@64006 ` 564` ``` apply simp ``` lp15@64006 ` 565` ``` apply (rule_tac B = "\{{D. D face_of C}| C. C \ \}" in finite_subset) ``` lp15@64006 ` 566` ``` by (auto simp: \finite \\ finite_polytope_faces poly) ``` lp15@64006 ` 567` ``` have clo: "closed S" if "S \ \ \ ?Faces" for S ``` lp15@64006 ` 568` ``` using that \\ \ \\ face_of_polytope_polytope poly polytope_imp_closed by blast ``` lp15@64006 ` 569` ``` have K: "X \ Y \ \(\ \ {D. \C\\. D face_of C \ aff_dim D < int p})" ``` nipkow@69508 ` 570` ``` if "X \ \ \ ?Faces" "Y \ \ \ ?Faces" "\ Y \ X" for X Y ``` lp15@64006 ` 571` ``` proof - ``` lp15@64006 ` 572` ``` have ff: "X \ Y face_of X \ X \ Y face_of Y" ``` lp15@64006 ` 573` ``` if XY: "X face_of D" "Y face_of E" and DE: "D \ \" "E \ \" for D E ``` lp15@64006 ` 574` ``` apply (rule face_of_Int_subface [OF _ _ XY]) ``` lp15@64006 ` 575` ``` apply (auto simp: face DE) ``` lp15@64006 ` 576` ``` done ``` lp15@64006 ` 577` ``` show ?thesis ``` lp15@64006 ` 578` ``` using that ``` lp15@64006 ` 579` ``` apply auto ``` lp15@64006 ` 580` ``` apply (drule_tac x="X \ Y" in spec, safe) ``` lp15@64006 ` 581` ``` using ff face_of_imp_convex [of X] face_of_imp_convex [of Y] ``` lp15@64006 ` 582` ``` apply (fastforce dest: face_of_aff_dim_lt) ``` lp15@64006 ` 583` ``` by (meson face_of_trans ff) ``` lp15@64006 ` 584` ``` qed ``` lp15@64006 ` 585` ``` obtain g where "continuous_on (\(\ \ ?Faces)) g" ``` lp15@64006 ` 586` ``` "g ` \(\ \ ?Faces) \ rel_frontier T" ``` lp15@64006 ` 587` ``` "(\x \ \(\ \ ?Faces) \ ``` lp15@64006 ` 588` ``` \(\ \ {D. \C\\. D face_of C \ aff_dim D < p}). g x = h x)" ``` lp15@64006 ` 589` ``` apply (rule exE [OF extending_maps_Union [OF fin extendh clo K]], blast+) ``` lp15@64006 ` 590` ``` done ``` lp15@64006 ` 591` ``` then show ?case ``` lp15@64006 ` 592` ``` apply (simp add: intle local.heq [symmetric], blast) ``` lp15@64006 ` 593` ``` done ``` lp15@64006 ` 594` ``` qed ``` lp15@64006 ` 595` ``` have eq: "\(\ \ {D. \C \ \. D face_of C \ aff_dim D < i}) = \\" ``` lp15@64006 ` 596` ``` proof ``` lp15@64006 ` 597` ``` show "\(\ \ {D. \C\\. D face_of C \ aff_dim D < int i}) \ \\" ``` lp15@64006 ` 598` ``` apply (rule Union_subsetI) ``` lp15@64006 ` 599` ``` using \\ \ \\ face_of_imp_subset apply force ``` lp15@64006 ` 600` ``` done ``` lp15@64006 ` 601` ``` show "\\ \ \(\ \ {D. \C\\. D face_of C \ aff_dim D < i})" ``` lp15@64006 ` 602` ``` apply (rule Union_mono) ``` lp15@64006 ` 603` ``` using face apply (fastforce simp: aff i) ``` lp15@64006 ` 604` ``` done ``` lp15@64006 ` 605` ``` qed ``` lp15@64006 ` 606` ``` have "int i \ aff_dim T" by (simp add: i) ``` lp15@64006 ` 607` ``` then show ?thesis ``` lp15@64006 ` 608` ``` using extendf [of i] unfolding eq by (metis that) ``` lp15@64006 ` 609` ```qed ``` lp15@64006 ` 610` ak2110@68833 ` 611` ```lemma%unimportant extend_map_lemma_cofinite0: ``` lp15@64006 ` 612` ``` assumes "finite \" ``` lp15@64006 ` 613` ``` and "pairwise (\S T. S \ T \ K) \" ``` lp15@64006 ` 614` ``` and "\S. S \ \ \ \a g. a \ U \ continuous_on (S - {a}) g \ g ` (S - {a}) \ T \ (\x \ S \ K. g x = h x)" ``` lp15@64006 ` 615` ``` and "\S. S \ \ \ closed S" ``` lp15@64006 ` 616` ``` shows "\C g. finite C \ disjnt C U \ card C \ card \ \ ``` lp15@64006 ` 617` ``` continuous_on (\\ - C) g \ g ` (\\ - C) \ T ``` lp15@64006 ` 618` ``` \ (\x \ (\\ - C) \ K. g x = h x)" ``` lp15@64006 ` 619` ``` using assms ``` lp15@64006 ` 620` ```proof induction ``` lp15@64006 ` 621` ``` case empty then show ?case ``` lp15@64006 ` 622` ``` by force ``` lp15@64006 ` 623` ```next ``` lp15@64006 ` 624` ``` case (insert X \) ``` lp15@64006 ` 625` ``` then have "closed X" and clo: "\X. X \ \ \ closed X" ``` lp15@64006 ` 626` ``` and \: "\S. S \ \ \ \a g. a \ U \ continuous_on (S - {a}) g \ g ` (S - {a}) \ T \ (\x \ S \ K. g x = h x)" ``` lp15@64006 ` 627` ``` and pwX: "\Y. Y \ \ \ Y \ X \ X \ Y \ K \ Y \ X \ K" ``` lp15@64006 ` 628` ``` and pwF: "pairwise (\ S T. S \ T \ K) \" ``` lp15@64006 ` 629` ``` by (simp_all add: pairwise_insert) ``` lp15@64006 ` 630` ``` obtain C g where C: "finite C" "disjnt C U" "card C \ card \" ``` lp15@64006 ` 631` ``` and contg: "continuous_on (\\ - C) g" ``` lp15@64006 ` 632` ``` and gim: "g ` (\\ - C) \ T" ``` lp15@64006 ` 633` ``` and gh: "\x. x \ (\\ - C) \ K \ g x = h x" ``` lp15@64006 ` 634` ``` using insert.IH [OF pwF \ clo] by auto ``` lp15@64006 ` 635` ``` obtain a f where "a \ U" ``` lp15@64006 ` 636` ``` and contf: "continuous_on (X - {a}) f" ``` lp15@64006 ` 637` ``` and fim: "f ` (X - {a}) \ T" ``` lp15@64006 ` 638` ``` and fh: "(\x \ X \ K. f x = h x)" ``` lp15@64006 ` 639` ``` using insert.prems by (meson insertI1) ``` lp15@64006 ` 640` ``` show ?case ``` lp15@64006 ` 641` ``` proof (intro exI conjI) ``` lp15@64006 ` 642` ``` show "finite (insert a C)" ``` lp15@64006 ` 643` ``` by (simp add: C) ``` lp15@64006 ` 644` ``` show "disjnt (insert a C) U" ``` lp15@64006 ` 645` ``` using C \a \ U\ by simp ``` lp15@64006 ` 646` ``` show "card (insert a C) \ card (insert X \)" ``` lp15@64006 ` 647` ``` by (simp add: C card_insert_if insert.hyps le_SucI) ``` lp15@64006 ` 648` ``` have "closed (\\)" ``` lp15@64006 ` 649` ``` using clo insert.hyps by blast ``` lp15@64006 ` 650` ``` have "continuous_on (X - insert a C \ (\\ - insert a C)) (\x. if x \ X then f x else g x)" ``` lp15@64006 ` 651` ``` apply (rule continuous_on_cases_local) ``` lp15@64006 ` 652` ``` apply (simp_all add: closedin_closed) ``` lp15@64006 ` 653` ``` using \closed X\ apply blast ``` lp15@64006 ` 654` ``` using \closed (\\)\ apply blast ``` lp15@64006 ` 655` ``` using contf apply (force simp: elim: continuous_on_subset) ``` lp15@64006 ` 656` ``` using contg apply (force simp: elim: continuous_on_subset) ``` lp15@64006 ` 657` ``` using fh gh insert.hyps pwX by fastforce ``` lp15@64006 ` 658` ``` then show "continuous_on (\insert X \ - insert a C) (\a. if a \ X then f a else g a)" ``` lp15@64006 ` 659` ``` by (blast intro: continuous_on_subset) ``` lp15@64006 ` 660` ``` show "\x\(\insert X \ - insert a C) \ K. (if x \ X then f x else g x) = h x" ``` lp15@64006 ` 661` ``` using gh by (auto simp: fh) ``` lp15@64006 ` 662` ``` show "(\a. if a \ X then f a else g a) ` (\insert X \ - insert a C) \ T" ``` lp15@64006 ` 663` ``` using fim gim by auto force ``` lp15@64006 ` 664` ``` qed ``` lp15@64006 ` 665` ```qed ``` lp15@64006 ` 666` lp15@64006 ` 667` ak2110@68833 ` 668` ```lemma%unimportant extend_map_lemma_cofinite1: ``` lp15@64006 ` 669` ```assumes "finite \" ``` lp15@64006 ` 670` ``` and \: "\X. X \ \ \ \a g. a \ U \ continuous_on (X - {a}) g \ g ` (X - {a}) \ T \ (\x \ X \ K. g x = h x)" ``` lp15@64006 ` 671` ``` and clo: "\X. X \ \ \ closed X" ``` nipkow@69508 ` 672` ``` and K: "\X Y. \X \ \; Y \ \; \ X \ Y; \ Y \ X\ \ X \ Y \ K" ``` lp15@64006 ` 673` ``` obtains C g where "finite C" "disjnt C U" "card C \ card \" "continuous_on (\\ - C) g" ``` lp15@64006 ` 674` ``` "g ` (\\ - C) \ T" ``` lp15@64006 ` 675` ``` "\x. x \ (\\ - C) \ K \ g x = h x" ``` lp15@64006 ` 676` ```proof - ``` lp15@64006 ` 677` ``` let ?\ = "{X \ \. \Y\\. \ X \ Y}" ``` lp15@64006 ` 678` ``` have [simp]: "\?\ = \\" ``` lp15@64006 ` 679` ``` by (simp add: Union_maximal_sets assms) ``` lp15@64006 ` 680` ``` have fin: "finite ?\" ``` lp15@64006 ` 681` ``` by (force intro: finite_subset [OF _ \finite \\]) ``` lp15@64006 ` 682` ``` have pw: "pairwise (\ S T. S \ T \ K) ?\" ``` lp15@64006 ` 683` ``` by (simp add: pairwise_def) (metis K psubsetI) ``` lp15@64006 ` 684` ``` have "card {X \ \. \Y\\. \ X \ Y} \ card \" ``` lp15@64006 ` 685` ``` by (simp add: \finite \\ card_mono) ``` lp15@64006 ` 686` ``` moreover ``` lp15@64006 ` 687` ``` obtain C g where "finite C \ disjnt C U \ card C \ card ?\ \ ``` lp15@64006 ` 688` ``` continuous_on (\?\ - C) g \ g ` (\?\ - C) \ T ``` lp15@64006 ` 689` ``` \ (\x \ (\?\ - C) \ K. g x = h x)" ``` lp15@64006 ` 690` ``` apply (rule exE [OF extend_map_lemma_cofinite0 [OF fin pw, of U T h]]) ``` lp15@64006 ` 691` ``` apply (fastforce intro!: clo \)+ ``` lp15@64006 ` 692` ``` done ``` lp15@64006 ` 693` ``` ultimately show ?thesis ``` lp15@64006 ` 694` ``` by (rule_tac C=C and g=g in that) auto ``` lp15@64006 ` 695` ```qed ``` lp15@64006 ` 696` lp15@64006 ` 697` ak2110@68833 ` 698` ```lemma%important extend_map_lemma_cofinite: ``` lp15@64006 ` 699` ``` assumes "finite \" "\ \ \" and T: "convex T" "bounded T" ``` lp15@64006 ` 700` ``` and poly: "\X. X \ \ \ polytope X" ``` lp15@64006 ` 701` ``` and contf: "continuous_on (\\) f" and fim: "f ` (\\) \ rel_frontier T" ``` lp15@64006 ` 702` ``` and face: "\X Y. \X \ \; Y \ \\ \ (X \ Y) face_of X \ (X \ Y) face_of Y" ``` lp15@64006 ` 703` ``` and aff: "\X. X \ \ - \ \ aff_dim X \ aff_dim T" ``` lp15@64006 ` 704` ``` obtains C g where ``` lp15@64006 ` 705` ``` "finite C" "disjnt C (\\)" "card C \ card \" "continuous_on (\\ - C) g" ``` lp15@64006 ` 706` ``` "g ` (\ \ - C) \ rel_frontier T" "\x. x \ \\ \ g x = f x" ``` ak2110@68833 ` 707` ```proof%unimportant - ``` lp15@64006 ` 708` ``` define \ where "\ \ \ \ {D. \C \ \ - \. D face_of C \ aff_dim D < aff_dim T}" ``` lp15@64006 ` 709` ``` have "finite \" ``` lp15@64006 ` 710` ``` using assms finite_subset by blast ``` lp15@64006 ` 711` ``` moreover have "finite (\{{D. D face_of C} |C. C \ \})" ``` lp15@64006 ` 712` ``` apply (rule finite_Union) ``` lp15@64006 ` 713` ``` apply (simp add: \finite \\) ``` lp15@64006 ` 714` ``` using finite_polytope_faces poly by auto ``` lp15@64006 ` 715` ``` ultimately have "finite \" ``` lp15@64006 ` 716` ``` apply (simp add: \_def) ``` lp15@64006 ` 717` ``` apply (rule finite_subset [of _ "\ {{D. D face_of C} | C. C \ \}"], auto) ``` lp15@64006 ` 718` ``` done ``` lp15@64006 ` 719` ``` have *: "\X Y. \X \ \; Y \ \\ \ X \ Y face_of X \ X \ Y face_of Y" ``` lp15@64006 ` 720` ``` unfolding \_def ``` lp15@64006 ` 721` ``` apply (elim UnE bexE CollectE DiffE) ``` lp15@64006 ` 722` ``` using subsetD [OF \\ \ \\] apply (simp_all add: face) ``` lp15@64006 ` 723` ``` apply (meson subsetD [OF \\ \ \\] face face_of_Int_subface face_of_imp_subset face_of_refl poly polytope_imp_convex)+ ``` lp15@64006 ` 724` ``` done ``` lp15@64006 ` 725` ``` obtain h where conth: "continuous_on (\\) h" and him: "h ` (\\) \ rel_frontier T" ``` lp15@64006 ` 726` ``` and hf: "\x. x \ \\ \ h x = f x" ``` lp15@64006 ` 727` ``` using \finite \\ ``` lp15@64006 ` 728` ``` unfolding \_def ``` lp15@64006 ` 729` ``` apply (rule extend_map_lemma [OF _ Un_upper1 T _ _ _ contf fim]) ``` lp15@64006 ` 730` ``` using \\ \ \\ face_of_polytope_polytope poly apply fastforce ``` lp15@64006 ` 731` ``` using * apply (auto simp: \_def) ``` lp15@64006 ` 732` ``` done ``` lp15@64006 ` 733` ``` have "bounded (\\)" ``` lp15@64006 ` 734` ``` using \finite \\ \\ \ \\ poly polytope_imp_bounded by blast ``` lp15@64006 ` 735` ``` then have "\\ \ UNIV" ``` lp15@64006 ` 736` ``` by auto ``` lp15@64006 ` 737` ``` then obtain a where a: "a \ \\" ``` lp15@64006 ` 738` ``` by blast ``` lp15@64006 ` 739` ``` have \: "\a g. a \ \\ \ continuous_on (D - {a}) g \ ``` lp15@64006 ` 740` ``` g ` (D - {a}) \ rel_frontier T \ (\x \ D \ \\. g x = h x)" ``` lp15@64006 ` 741` ``` if "D \ \" for D ``` lp15@64006 ` 742` ``` proof (cases "D \ \\") ``` lp15@64006 ` 743` ``` case True ``` lp15@64006 ` 744` ``` then show ?thesis ``` lp15@64006 ` 745` ``` apply (rule_tac x=a in exI) ``` lp15@64006 ` 746` ``` apply (rule_tac x=h in exI) ``` lp15@64006 ` 747` ``` using him apply (blast intro!: \a \ \\\ continuous_on_subset [OF conth]) + ``` lp15@64006 ` 748` ``` done ``` lp15@64006 ` 749` ``` next ``` lp15@64006 ` 750` ``` case False ``` lp15@64006 ` 751` ``` note D_not_subset = False ``` lp15@64006 ` 752` ``` show ?thesis ``` lp15@64006 ` 753` ``` proof (cases "D \ \") ``` lp15@64006 ` 754` ``` case True ``` lp15@64006 ` 755` ``` with D_not_subset show ?thesis ``` lp15@64006 ` 756` ``` by (auto simp: \_def) ``` lp15@64006 ` 757` ``` next ``` lp15@64006 ` 758` ``` case False ``` lp15@64006 ` 759` ``` then have affD: "aff_dim D \ aff_dim T" ``` lp15@64006 ` 760` ``` by (simp add: \D \ \\ aff) ``` lp15@64006 ` 761` ``` show ?thesis ``` lp15@64006 ` 762` ``` proof (cases "rel_interior D = {}") ``` lp15@64006 ` 763` ``` case True ``` lp15@64006 ` 764` ``` with \D \ \\ poly a show ?thesis ``` lp15@64006 ` 765` ``` by (force simp: rel_interior_eq_empty polytope_imp_convex) ``` lp15@64006 ` 766` ``` next ``` lp15@64006 ` 767` ``` case False ``` lp15@64006 ` 768` ``` then obtain b where brelD: "b \ rel_interior D" ``` lp15@64006 ` 769` ``` by blast ``` lp15@64006 ` 770` ``` have "polyhedron D" ``` lp15@64006 ` 771` ``` by (simp add: poly polytope_imp_polyhedron that) ``` lp15@64006 ` 772` ``` have "rel_frontier D retract_of affine hull D - {b}" ``` lp15@64006 ` 773` ``` by (simp add: rel_frontier_retract_of_punctured_affine_hull poly polytope_imp_bounded polytope_imp_convex that brelD) ``` lp15@64006 ` 774` ``` then obtain r where relfD: "rel_frontier D \ affine hull D - {b}" ``` lp15@64006 ` 775` ``` and contr: "continuous_on (affine hull D - {b}) r" ``` lp15@64006 ` 776` ``` and rim: "r ` (affine hull D - {b}) \ rel_frontier D" ``` lp15@64006 ` 777` ``` and rid: "\x. x \ rel_frontier D \ r x = x" ``` lp15@64006 ` 778` ``` by (auto simp: retract_of_def retraction_def) ``` lp15@64006 ` 779` ``` show ?thesis ``` lp15@64006 ` 780` ``` proof (intro exI conjI ballI) ``` lp15@64006 ` 781` ``` show "b \ \\" ``` lp15@64006 ` 782` ``` proof clarify ``` lp15@64006 ` 783` ``` fix E ``` lp15@64006 ` 784` ``` assume "b \ E" "E \ \" ``` lp15@64006 ` 785` ``` then have "E \ D face_of E \ E \ D face_of D" ``` lp15@64006 ` 786` ``` using \\ \ \\ face that by auto ``` lp15@64006 ` 787` ``` with face_of_subset_rel_frontier \E \ \\ \b \ E\ brelD rel_interior_subset [of D] ``` lp15@64006 ` 788` ``` D_not_subset rel_frontier_def \_def ``` lp15@64006 ` 789` ``` show False ``` lp15@64006 ` 790` ``` by blast ``` lp15@64006 ` 791` ``` qed ``` lp15@64006 ` 792` ``` have "r ` (D - {b}) \ r ` (affine hull D - {b})" ``` lp15@64006 ` 793` ``` by (simp add: Diff_mono hull_subset image_mono) ``` lp15@64006 ` 794` ``` also have "... \ rel_frontier D" ``` lp15@64006 ` 795` ``` by (rule rim) ``` lp15@64006 ` 796` ``` also have "... \ \{E. E face_of D \ aff_dim E < aff_dim T}" ``` lp15@64006 ` 797` ``` using affD ``` lp15@64006 ` 798` ``` by (force simp: rel_frontier_of_polyhedron [OF \polyhedron D\] facet_of_def) ``` lp15@64006 ` 799` ``` also have "... \ \(\)" ``` lp15@64006 ` 800` ``` using D_not_subset \_def that by fastforce ``` lp15@64006 ` 801` ``` finally have rsub: "r ` (D - {b}) \ \(\)" . ``` lp15@64006 ` 802` ``` show "continuous_on (D - {b}) (h \ r)" ``` lp15@64006 ` 803` ``` apply (intro conjI \b \ \\\ continuous_on_compose) ``` lp15@64006 ` 804` ``` apply (rule continuous_on_subset [OF contr]) ``` lp15@64006 ` 805` ``` apply (simp add: Diff_mono hull_subset) ``` lp15@64006 ` 806` ``` apply (rule continuous_on_subset [OF conth rsub]) ``` lp15@64006 ` 807` ``` done ``` lp15@64006 ` 808` ``` show "(h \ r) ` (D - {b}) \ rel_frontier T" ``` lp15@64006 ` 809` ``` using brelD him rsub by fastforce ``` lp15@64006 ` 810` ``` show "(h \ r) x = h x" if x: "x \ D \ \\" for x ``` lp15@64006 ` 811` ``` proof - ``` lp15@64006 ` 812` ``` consider A where "x \ D" "A \ \" "x \ A" ``` lp15@64006 ` 813` ``` | A B where "x \ D" "A face_of B" "B \ \" "B \ \" "aff_dim A < aff_dim T" "x \ A" ``` lp15@64006 ` 814` ``` using x by (auto simp: \_def) ``` lp15@64006 ` 815` ``` then have xrel: "x \ rel_frontier D" ``` lp15@64006 ` 816` ``` proof cases ``` lp15@64006 ` 817` ``` case 1 show ?thesis ``` lp15@64006 ` 818` ``` proof (rule face_of_subset_rel_frontier [THEN subsetD]) ``` lp15@64006 ` 819` ``` show "D \ A face_of D" ``` lp15@64006 ` 820` ``` using \A \ \\ \\ \ \\ face \D \ \\ by blast ``` lp15@64006 ` 821` ``` show "D \ A \ D" ``` lp15@64006 ` 822` ``` using \A \ \\ D_not_subset \_def by blast ``` lp15@64006 ` 823` ``` qed (auto simp: 1) ``` lp15@64006 ` 824` ``` next ``` lp15@64006 ` 825` ``` case 2 show ?thesis ``` lp15@64006 ` 826` ``` proof (rule face_of_subset_rel_frontier [THEN subsetD]) ``` lp15@64006 ` 827` ``` show "D \ A face_of D" ``` lp15@64006 ` 828` ``` apply (rule face_of_Int_subface [of D B _ A, THEN conjunct1]) ``` lp15@64006 ` 829` ``` apply (simp_all add: 2 \D \ \\ face) ``` lp15@64006 ` 830` ``` apply (simp add: \polyhedron D\ polyhedron_imp_convex face_of_refl) ``` lp15@64006 ` 831` ``` done ``` lp15@64006 ` 832` ``` show "D \ A \ D" ``` lp15@64006 ` 833` ``` using "2" D_not_subset \_def by blast ``` lp15@64006 ` 834` ``` qed (auto simp: 2) ``` lp15@64006 ` 835` ``` qed ``` lp15@64006 ` 836` ``` show ?thesis ``` lp15@64006 ` 837` ``` by (simp add: rid xrel) ``` lp15@64006 ` 838` ``` qed ``` lp15@64006 ` 839` ``` qed ``` lp15@64006 ` 840` ``` qed ``` lp15@64006 ` 841` ``` qed ``` lp15@64006 ` 842` ``` qed ``` lp15@64006 ` 843` ``` have clo: "\S. S \ \ \ closed S" ``` lp15@64006 ` 844` ``` by (simp add: poly polytope_imp_closed) ``` lp15@64006 ` 845` ``` obtain C g where "finite C" "disjnt C (\\)" "card C \ card \" "continuous_on (\\ - C) g" ``` lp15@64006 ` 846` ``` "g ` (\\ - C) \ rel_frontier T" ``` lp15@64006 ` 847` ``` and gh: "\x. x \ (\\ - C) \ \\ \ g x = h x" ``` lp15@64006 ` 848` ``` proof (rule extend_map_lemma_cofinite1 [OF \finite \\ \ clo]) ``` lp15@64006 ` 849` ``` show "X \ Y \ \\" if XY: "X \ \" "Y \ \" and "\ X \ Y" "\ Y \ X" for X Y ``` lp15@64006 ` 850` ``` proof (cases "X \ \") ``` lp15@64006 ` 851` ``` case True ``` lp15@64006 ` 852` ``` then show ?thesis ``` lp15@64006 ` 853` ``` by (auto simp: \_def) ``` lp15@64006 ` 854` ``` next ``` lp15@64006 ` 855` ``` case False ``` lp15@64006 ` 856` ``` have "X \ Y \ X" ``` lp15@64006 ` 857` ``` using \\ X \ Y\ by blast ``` lp15@64006 ` 858` ``` with XY ``` lp15@64006 ` 859` ``` show ?thesis ``` lp15@64006 ` 860` ``` by (clarsimp simp: \_def) ``` lp15@64006 ` 861` ``` (metis Diff_iff Int_iff aff antisym_conv face face_of_aff_dim_lt face_of_refl ``` lp15@64006 ` 862` ``` not_le poly polytope_imp_convex) ``` lp15@64006 ` 863` ``` qed ``` lp15@64006 ` 864` ``` qed (blast)+ ``` lp15@64006 ` 865` ``` with \\ \ \\ show ?thesis ``` lp15@64006 ` 866` ``` apply (rule_tac C=C and g=g in that) ``` lp15@64006 ` 867` ``` apply (auto simp: disjnt_def hf [symmetric] \_def intro!: gh) ``` lp15@64006 ` 868` ``` done ``` lp15@64006 ` 869` ```qed ``` lp15@64006 ` 870` lp15@64006 ` 871` ```text\The next two proofs are similar\ ``` ak2110@68833 ` 872` ```theorem%important extend_map_cell_complex_to_sphere: ``` lp15@64006 ` 873` ``` assumes "finite \" and S: "S \ \\" "closed S" and T: "convex T" "bounded T" ``` lp15@64006 ` 874` ``` and poly: "\X. X \ \ \ polytope X" ``` lp15@64006 ` 875` ``` and aff: "\X. X \ \ \ aff_dim X < aff_dim T" ``` lp15@64006 ` 876` ``` and face: "\X Y. \X \ \; Y \ \\ \ (X \ Y) face_of X \ (X \ Y) face_of Y" ``` lp15@64006 ` 877` ``` and contf: "continuous_on S f" and fim: "f ` S \ rel_frontier T" ``` lp15@64006 ` 878` ``` obtains g where "continuous_on (\\) g" ``` lp15@64006 ` 879` ``` "g ` (\\) \ rel_frontier T" "\x. x \ S \ g x = f x" ``` ak2110@68833 ` 880` ```proof%unimportant - ``` lp15@64006 ` 881` ``` obtain V g where "S \ V" "open V" "continuous_on V g" and gim: "g ` V \ rel_frontier T" and gf: "\x. x \ S \ g x = f x" ``` lp15@64006 ` 882` ``` using neighbourhood_extension_into_ANR [OF contf fim _ \closed S\] ANR_rel_frontier_convex T by blast ``` lp15@64006 ` 883` ``` have "compact S" ``` lp15@64006 ` 884` ``` by (meson assms compact_Union poly polytope_imp_compact seq_compact_closed_subset seq_compact_eq_compact) ``` lp15@64006 ` 885` ``` then obtain d where "d > 0" and d: "\x y. \x \ S; y \ - V\ \ d \ dist x y" ``` lp15@64006 ` 886` ``` using separate_compact_closed [of S "-V"] \open V\ \S \ V\ by force ``` lp15@64006 ` 887` ``` obtain \ where "finite \" "\\ = \\" ``` lp15@64006 ` 888` ``` and diaG: "\X. X \ \ \ diameter X < d" ``` lp15@64006 ` 889` ``` and polyG: "\X. X \ \ \ polytope X" ``` lp15@64006 ` 890` ``` and affG: "\X. X \ \ \ aff_dim X \ aff_dim T - 1" ``` lp15@64006 ` 891` ``` and faceG: "\X Y. \X \ \; Y \ \\ \ X \ Y face_of X \ X \ Y face_of Y" ``` lp15@64006 ` 892` ``` proof (rule cell_complex_subdivision_exists [OF \d>0\ \finite \\ poly _ face]) ``` lp15@64006 ` 893` ``` show "\X. X \ \ \ aff_dim X \ aff_dim T - 1" ``` lp15@64006 ` 894` ``` by (simp add: aff) ``` lp15@64006 ` 895` ``` qed auto ``` lp15@64006 ` 896` ``` obtain h where conth: "continuous_on (\\) h" and him: "h ` \\ \ rel_frontier T" and hg: "\x. x \ \(\ \ Pow V) \ h x = g x" ``` lp15@64006 ` 897` ``` proof (rule extend_map_lemma [of \ "\ \ Pow V" T g]) ``` lp15@64006 ` 898` ``` show "continuous_on (\(\ \ Pow V)) g" ``` lp15@64006 ` 899` ``` by (metis Union_Int_subset Union_Pow_eq \continuous_on V g\ continuous_on_subset le_inf_iff) ``` lp15@64006 ` 900` ``` qed (use \finite \\ T polyG affG faceG gim in fastforce)+ ``` lp15@64006 ` 901` ``` show ?thesis ``` lp15@64006 ` 902` ``` proof ``` lp15@64006 ` 903` ``` show "continuous_on (\\) h" ``` lp15@64006 ` 904` ``` using \\\ = \\\ conth by auto ``` lp15@64006 ` 905` ``` show "h ` \\ \ rel_frontier T" ``` lp15@64006 ` 906` ``` using \\\ = \\\ him by auto ``` lp15@64006 ` 907` ``` show "h x = f x" if "x \ S" for x ``` lp15@64006 ` 908` ``` proof - ``` lp15@64006 ` 909` ``` have "x \ \\" ``` lp15@64006 ` 910` ``` using \\\ = \\\ \S \ \\\ that by auto ``` lp15@64006 ` 911` ``` then obtain X where "x \ X" "X \ \" by blast ``` lp15@64006 ` 912` ``` then have "diameter X < d" "bounded X" ``` lp15@64006 ` 913` ``` by (auto simp: diaG \X \ \\ polyG polytope_imp_bounded) ``` lp15@64006 ` 914` ``` then have "X \ V" using d [OF \x \ S\] diameter_bounded_bound [OF \bounded X\ \x \ X\] ``` lp15@64006 ` 915` ``` by fastforce ``` lp15@64006 ` 916` ``` have "h x = g x" ``` lp15@64006 ` 917` ``` apply (rule hg) ``` lp15@64006 ` 918` ``` using \X \ \\ \X \ V\ \x \ X\ by blast ``` lp15@64006 ` 919` ``` also have "... = f x" ``` lp15@64006 ` 920` ``` by (simp add: gf that) ``` lp15@64006 ` 921` ``` finally show "h x = f x" . ``` lp15@64006 ` 922` ``` qed ``` lp15@64006 ` 923` ``` qed ``` lp15@64006 ` 924` ```qed ``` lp15@64006 ` 925` lp15@64006 ` 926` ak2110@68833 ` 927` ```theorem%important extend_map_cell_complex_to_sphere_cofinite: ``` lp15@64006 ` 928` ``` assumes "finite \" and S: "S \ \\" "closed S" and T: "convex T" "bounded T" ``` lp15@64006 ` 929` ``` and poly: "\X. X \ \ \ polytope X" ``` lp15@64006 ` 930` ``` and aff: "\X. X \ \ \ aff_dim X \ aff_dim T" ``` lp15@64006 ` 931` ``` and face: "\X Y. \X \ \; Y \ \\ \ (X \ Y) face_of X \ (X \ Y) face_of Y" ``` lp15@64006 ` 932` ``` and contf: "continuous_on S f" and fim: "f ` S \ rel_frontier T" ``` lp15@64006 ` 933` ``` obtains C g where "finite C" "disjnt C S" "continuous_on (\\ - C) g" ``` lp15@64006 ` 934` ``` "g ` (\\ - C) \ rel_frontier T" "\x. x \ S \ g x = f x" ``` ak2110@68833 ` 935` ```proof%unimportant - ``` lp15@64006 ` 936` ``` obtain V g where "S \ V" "open V" "continuous_on V g" and gim: "g ` V \ rel_frontier T" and gf: "\x. x \ S \ g x = f x" ``` lp15@64006 ` 937` ``` using neighbourhood_extension_into_ANR [OF contf fim _ \closed S\] ANR_rel_frontier_convex T by blast ``` lp15@64006 ` 938` ``` have "compact S" ``` lp15@64006 ` 939` ``` by (meson assms compact_Union poly polytope_imp_compact seq_compact_closed_subset seq_compact_eq_compact) ``` lp15@64006 ` 940` ``` then obtain d where "d > 0" and d: "\x y. \x \ S; y \ - V\ \ d \ dist x y" ``` lp15@64006 ` 941` ``` using separate_compact_closed [of S "-V"] \open V\ \S \ V\ by force ``` lp15@64006 ` 942` ``` obtain \ where "finite \" "\\ = \\" ``` lp15@64006 ` 943` ``` and diaG: "\X. X \ \ \ diameter X < d" ``` lp15@64006 ` 944` ``` and polyG: "\X. X \ \ \ polytope X" ``` lp15@64006 ` 945` ``` and affG: "\X. X \ \ \ aff_dim X \ aff_dim T" ``` lp15@64006 ` 946` ``` and faceG: "\X Y. \X \ \; Y \ \\ \ X \ Y face_of X \ X \ Y face_of Y" ``` lp15@64006 ` 947` ``` by (rule cell_complex_subdivision_exists [OF \d>0\ \finite \\ poly aff face]) auto ``` lp15@64006 ` 948` ``` obtain C h where "finite C" and dis: "disjnt C (\(\ \ Pow V))" ``` lp15@64006 ` 949` ``` and card: "card C \ card \" and conth: "continuous_on (\\ - C) h" ``` lp15@64006 ` 950` ``` and him: "h ` (\\ - C) \ rel_frontier T" ``` lp15@64006 ` 951` ``` and hg: "\x. x \ \(\ \ Pow V) \ h x = g x" ``` lp15@64006 ` 952` ``` proof (rule extend_map_lemma_cofinite [of \ "\ \ Pow V" T g]) ``` lp15@64006 ` 953` ``` show "continuous_on (\(\ \ Pow V)) g" ``` lp15@64006 ` 954` ``` by (metis Union_Int_subset Union_Pow_eq \continuous_on V g\ continuous_on_subset le_inf_iff) ``` lp15@64006 ` 955` ``` show "g ` \(\ \ Pow V) \ rel_frontier T" ``` lp15@64006 ` 956` ``` using gim by force ``` lp15@64006 ` 957` ``` qed (auto intro: \finite \\ T polyG affG dest: faceG) ``` lp15@64006 ` 958` ``` have Ssub: "S \ \(\ \ Pow V)" ``` lp15@64006 ` 959` ``` proof ``` lp15@64006 ` 960` ``` fix x ``` lp15@64006 ` 961` ``` assume "x \ S" ``` lp15@64006 ` 962` ``` then have "x \ \\" ``` lp15@64006 ` 963` ``` using \\\ = \\\ \S \ \\\ by auto ``` lp15@64006 ` 964` ``` then obtain X where "x \ X" "X \ \" by blast ``` lp15@64006 ` 965` ``` then have "diameter X < d" "bounded X" ``` lp15@64006 ` 966` ``` by (auto simp: diaG \X \ \\ polyG polytope_imp_bounded) ``` lp15@64006 ` 967` ``` then have "X \ V" using d [OF \x \ S\] diameter_bounded_bound [OF \bounded X\ \x \ X\] ``` lp15@64006 ` 968` ``` by fastforce ``` lp15@64006 ` 969` ``` then show "x \ \(\ \ Pow V)" ``` lp15@64006 ` 970` ``` using \X \ \\ \x \ X\ by blast ``` lp15@64006 ` 971` ``` qed ``` lp15@64006 ` 972` ``` show ?thesis ``` lp15@64006 ` 973` ``` proof ``` lp15@64006 ` 974` ``` show "continuous_on (\\-C) h" ``` lp15@64006 ` 975` ``` using \\\ = \\\ conth by auto ``` lp15@64006 ` 976` ``` show "h ` (\\ - C) \ rel_frontier T" ``` lp15@64006 ` 977` ``` using \\\ = \\\ him by auto ``` lp15@64006 ` 978` ``` show "h x = f x" if "x \ S" for x ``` lp15@64006 ` 979` ``` proof - ``` lp15@64006 ` 980` ``` have "h x = g x" ``` lp15@64006 ` 981` ``` apply (rule hg) ``` lp15@64006 ` 982` ``` using Ssub that by blast ``` lp15@64006 ` 983` ``` also have "... = f x" ``` lp15@64006 ` 984` ``` by (simp add: gf that) ``` lp15@64006 ` 985` ``` finally show "h x = f x" . ``` lp15@64006 ` 986` ``` qed ``` lp15@64006 ` 987` ``` show "disjnt C S" ``` lp15@64006 ` 988` ``` using dis Ssub by (meson disjnt_iff subset_eq) ``` lp15@64006 ` 989` ``` qed (intro \finite C\) ``` lp15@64006 ` 990` ```qed ``` lp15@64006 ` 991` lp15@64006 ` 992` lp15@64006 ` 993` ak2110@68833 ` 994` ```subsection%important\ Special cases and corollaries involving spheres\ ``` ak2110@68833 ` 995` ak2110@68833 ` 996` ```lemma%unimportant disjnt_Diff1: "X \ Y' \ disjnt (X - Y) (X' - Y')" ``` lp15@64006 ` 997` ``` by (auto simp: disjnt_def) ``` lp15@64006 ` 998` ak2110@68833 ` 999` ```proposition%important extend_map_affine_to_sphere_cofinite_simple: ``` lp15@64006 ` 1000` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@64006 ` 1001` ``` assumes "compact S" "convex U" "bounded U" ``` lp15@64006 ` 1002` ``` and aff: "aff_dim T \ aff_dim U" ``` lp15@64006 ` 1003` ``` and "S \ T" and contf: "continuous_on S f" ``` lp15@64006 ` 1004` ``` and fim: "f ` S \ rel_frontier U" ``` lp15@64006 ` 1005` ``` obtains K g where "finite K" "K \ T" "disjnt K S" "continuous_on (T - K) g" ``` lp15@64006 ` 1006` ``` "g ` (T - K) \ rel_frontier U" ``` lp15@64006 ` 1007` ``` "\x. x \ S \ g x = f x" ``` ak2110@68833 ` 1008` ```proof%unimportant - ``` lp15@64006 ` 1009` ``` have "\K g. finite K \ disjnt K S \ continuous_on (T - K) g \ ``` lp15@64006 ` 1010` ``` g ` (T - K) \ rel_frontier U \ (\x \ S. g x = f x)" ``` lp15@64006 ` 1011` ``` if "affine T" "S \ T" and aff: "aff_dim T \ aff_dim U" for T ``` lp15@64006 ` 1012` ``` proof (cases "S = {}") ``` lp15@64006 ` 1013` ``` case True ``` lp15@64006 ` 1014` ``` show ?thesis ``` lp15@64006 ` 1015` ``` proof (cases "rel_frontier U = {}") ``` lp15@64006 ` 1016` ``` case True ``` lp15@64006 ` 1017` ``` with \bounded U\ have "aff_dim U \ 0" ``` lp15@64006 ` 1018` ``` using affine_bounded_eq_lowdim rel_frontier_eq_empty by auto ``` lp15@64006 ` 1019` ``` with aff have "aff_dim T \ 0" by auto ``` lp15@64006 ` 1020` ``` then obtain a where "T \ {a}" ``` lp15@64006 ` 1021` ``` using \affine T\ affine_bounded_eq_lowdim affine_bounded_eq_trivial by auto ``` lp15@64006 ` 1022` ``` then show ?thesis ``` lp15@64006 ` 1023` ``` using \S = {}\ fim ``` lp15@64006 ` 1024` ``` by (metis Diff_cancel contf disjnt_empty2 finite.emptyI finite_insert finite_subset) ``` lp15@64006 ` 1025` ``` next ``` lp15@64006 ` 1026` ``` case False ``` lp15@64006 ` 1027` ``` then obtain a where "a \ rel_frontier U" ``` lp15@64006 ` 1028` ``` by auto ``` lp15@64006 ` 1029` ``` then show ?thesis ``` lp15@64006 ` 1030` ``` using continuous_on_const [of _ a] \S = {}\ by force ``` lp15@64006 ` 1031` ``` qed ``` lp15@64006 ` 1032` ``` next ``` lp15@64006 ` 1033` ``` case False ``` lp15@64006 ` 1034` ``` have "bounded S" ``` lp15@64006 ` 1035` ``` by (simp add: \compact S\ compact_imp_bounded) ``` lp15@64006 ` 1036` ``` then obtain b where b: "S \ cbox (-b) b" ``` lp15@64006 ` 1037` ``` using bounded_subset_cbox_symmetric by blast ``` lp15@64006 ` 1038` ``` define bbox where "bbox \ cbox (-(b+One)) (b+One)" ``` lp15@64006 ` 1039` ``` have "cbox (-b) b \ bbox" ``` lp15@64006 ` 1040` ``` by (auto simp: bbox_def algebra_simps intro!: subset_box_imp) ``` lp15@64006 ` 1041` ``` with b \S \ T\ have "S \ bbox \ T" ``` lp15@64006 ` 1042` ``` by auto ``` lp15@64006 ` 1043` ``` then have Ssub: "S \ \{bbox \ T}" ``` lp15@64006 ` 1044` ``` by auto ``` lp15@64006 ` 1045` ``` then have "aff_dim (bbox \ T) \ aff_dim U" ``` lp15@64006 ` 1046` ``` by (metis aff aff_dim_subset inf_commute inf_le1 order_trans) ``` lp15@64006 ` 1047` ``` obtain K g where K: "finite K" "disjnt K S" ``` lp15@64006 ` 1048` ``` and contg: "continuous_on (\{bbox \ T} - K) g" ``` lp15@64006 ` 1049` ``` and gim: "g ` (\{bbox \ T} - K) \ rel_frontier U" ``` lp15@64006 ` 1050` ``` and gf: "\x. x \ S \ g x = f x" ``` lp15@64006 ` 1051` ``` proof (rule extend_map_cell_complex_to_sphere_cofinite ``` lp15@64006 ` 1052` ``` [OF _ Ssub _ \convex U\ \bounded U\ _ _ _ contf fim]) ``` lp15@64006 ` 1053` ``` show "closed S" ``` lp15@64006 ` 1054` ``` using \compact S\ compact_eq_bounded_closed by auto ``` lp15@64006 ` 1055` ``` show poly: "\X. X \ {bbox \ T} \ polytope X" ``` lp15@64006 ` 1056` ``` by (simp add: polytope_Int_polyhedron bbox_def polytope_interval affine_imp_polyhedron \affine T\) ``` lp15@64006 ` 1057` ``` show "\X Y. \X \ {bbox \ T}; Y \ {bbox \ T}\ \ X \ Y face_of X \ X \ Y face_of Y" ``` lp15@64006 ` 1058` ``` by (simp add:poly face_of_refl polytope_imp_convex) ``` lp15@64006 ` 1059` ``` show "\X. X \ {bbox \ T} \ aff_dim X \ aff_dim U" ``` lp15@64006 ` 1060` ``` by (simp add: \aff_dim (bbox \ T) \ aff_dim U\) ``` lp15@64006 ` 1061` ``` qed auto ``` lp15@64006 ` 1062` ``` define fro where "fro \ \d. frontier(cbox (-(b + d *\<^sub>R One)) (b + d *\<^sub>R One))" ``` lp15@64006 ` 1063` ``` obtain d where d12: "1/2 \ d" "d \ 1" and dd: "disjnt K (fro d)" ``` lp15@64006 ` 1064` ``` proof (rule disjoint_family_elem_disjnt [OF _ \finite K\]) ``` lp15@64006 ` 1065` ``` show "infinite {1/2..1::real}" ``` lp15@64006 ` 1066` ``` by (simp add: infinite_Icc) ``` lp15@64006 ` 1067` ``` have dis1: "disjnt (fro x) (fro y)" if "x b + d *\<^sub>R One" ``` lp15@64006 ` 1073` ``` have cbsub: "cbox (-b) b \ box (-c) c" "cbox (-b) b \ cbox (-c) c" "cbox (-c) c \ bbox" ``` lp15@64006 ` 1074` ``` using d12 by (auto simp: algebra_simps subset_box_imp c_def bbox_def) ``` lp15@64006 ` 1075` ``` have clo_cbT: "closed (cbox (- c) c \ T)" ``` lp15@64006 ` 1076` ``` by (simp add: affine_closed closed_Int closed_cbox \affine T\) ``` lp15@64006 ` 1077` ``` have cpT_ne: "cbox (- c) c \ T \ {}" ``` lp15@64006 ` 1078` ``` using \S \ {}\ b cbsub(2) \S \ T\ by fastforce ``` lp15@64006 ` 1079` ``` have "closest_point (cbox (- c) c \ T) x \ K" if "x \ T" "x \ K" for x ``` lp15@64006 ` 1080` ``` proof (cases "x \ cbox (-c) c") ``` lp15@64006 ` 1081` ``` case True with that show ?thesis ``` lp15@64006 ` 1082` ``` by (simp add: closest_point_self) ``` lp15@64006 ` 1083` ``` next ``` lp15@64006 ` 1084` ``` case False ``` lp15@64006 ` 1085` ``` have int_ne: "interior (cbox (-c) c) \ T \ {}" ``` lp15@64006 ` 1086` ``` using \S \ {}\ \S \ T\ b \cbox (- b) b \ box (- c) c\ by force ``` lp15@64006 ` 1087` ``` have "convex T" ``` lp15@64006 ` 1088` ``` by (meson \affine T\ affine_imp_convex) ``` lp15@64006 ` 1089` ``` then have "x \ affine hull (cbox (- c) c \ T)" ``` lp15@64006 ` 1090` ``` by (metis Int_commute Int_iff \S \ {}\ \S \ T\ cbsub(1) \x \ T\ affine_hull_convex_Int_nonempty_interior all_not_in_conv b hull_inc inf.orderE interior_cbox) ``` lp15@64006 ` 1091` ``` then have "x \ affine hull (cbox (- c) c \ T) - rel_interior (cbox (- c) c \ T)" ``` lp15@64006 ` 1092` ``` by (meson DiffI False Int_iff rel_interior_subset subsetCE) ``` lp15@64006 ` 1093` ``` then have "closest_point (cbox (- c) c \ T) x \ rel_frontier (cbox (- c) c \ T)" ``` lp15@64006 ` 1094` ``` by (rule closest_point_in_rel_frontier [OF clo_cbT cpT_ne]) ``` lp15@64006 ` 1095` ``` moreover have "(rel_frontier (cbox (- c) c \ T)) \ fro d" ``` lp15@64006 ` 1096` ``` apply (subst convex_affine_rel_frontier_Int [OF _ \affine T\ int_ne]) ``` lp15@64006 ` 1097` ``` apply (auto simp: fro_def c_def) ``` lp15@64006 ` 1098` ``` done ``` lp15@64006 ` 1099` ``` ultimately show ?thesis ``` lp15@64006 ` 1100` ``` using dd by (force simp: disjnt_def) ``` lp15@64006 ` 1101` ``` qed ``` lp15@64006 ` 1102` ``` then have cpt_subset: "closest_point (cbox (- c) c \ T) ` (T - K) \ \{bbox \ T} - K" ``` lp15@64006 ` 1103` ``` using closest_point_in_set [OF clo_cbT cpT_ne] cbsub(3) by force ``` lp15@64006 ` 1104` ``` show ?thesis ``` lp15@64006 ` 1105` ``` proof (intro conjI ballI exI) ``` lp15@64006 ` 1106` ``` have "continuous_on (T - K) (closest_point (cbox (- c) c \ T))" ``` lp15@64006 ` 1107` ``` apply (rule continuous_on_closest_point) ``` lp15@64006 ` 1108` ``` using \S \ {}\ cbsub(2) b that ``` lp15@64006 ` 1109` ``` by (auto simp: affine_imp_convex convex_Int affine_closed closed_Int closed_cbox \affine T\) ``` lp15@64006 ` 1110` ``` then show "continuous_on (T - K) (g \ closest_point (cbox (- c) c \ T))" ``` lp15@64006 ` 1111` ``` by (metis continuous_on_compose continuous_on_subset [OF contg cpt_subset]) ``` lp15@64006 ` 1112` ``` have "(g \ closest_point (cbox (- c) c \ T)) ` (T - K) \ g ` (\{bbox \ T} - K)" ``` lp15@64006 ` 1113` ``` by (metis image_comp image_mono cpt_subset) ``` lp15@64006 ` 1114` ``` also have "... \ rel_frontier U" ``` lp15@64006 ` 1115` ``` by (rule gim) ``` lp15@64006 ` 1116` ``` finally show "(g \ closest_point (cbox (- c) c \ T)) ` (T - K) \ rel_frontier U" . ``` lp15@64006 ` 1117` ``` show "(g \ closest_point (cbox (- c) c \ T)) x = f x" if "x \ S" for x ``` lp15@64006 ` 1118` ``` proof - ``` lp15@64006 ` 1119` ``` have "(g \ closest_point (cbox (- c) c \ T)) x = g x" ``` lp15@64006 ` 1120` ``` unfolding o_def ``` lp15@64006 ` 1121` ``` by (metis IntI \S \ T\ b cbsub(2) closest_point_self subset_eq that) ``` lp15@64006 ` 1122` ``` also have "... = f x" ``` lp15@64006 ` 1123` ``` by (simp add: that gf) ``` lp15@64006 ` 1124` ``` finally show ?thesis . ``` lp15@64006 ` 1125` ``` qed ``` lp15@64006 ` 1126` ``` qed (auto simp: K) ``` lp15@64006 ` 1127` ``` qed ``` lp15@64006 ` 1128` ``` then obtain K g where "finite K" "disjnt K S" ``` lp15@64006 ` 1129` ``` and contg: "continuous_on (affine hull T - K) g" ``` lp15@64006 ` 1130` ``` and gim: "g ` (affine hull T - K) \ rel_frontier U" ``` lp15@64006 ` 1131` ``` and gf: "\x. x \ S \ g x = f x" ``` lp15@64006 ` 1132` ``` by (metis aff affine_affine_hull aff_dim_affine_hull ``` lp15@64006 ` 1133` ``` order_trans [OF \S \ T\ hull_subset [of T affine]]) ``` lp15@64006 ` 1134` ``` then obtain K g where "finite K" "disjnt K S" ``` lp15@64006 ` 1135` ``` and contg: "continuous_on (T - K) g" ``` lp15@64006 ` 1136` ``` and gim: "g ` (T - K) \ rel_frontier U" ``` lp15@64006 ` 1137` ``` and gf: "\x. x \ S \ g x = f x" ``` lp15@64006 ` 1138` ``` by (rule_tac K=K and g=g in that) (auto simp: hull_inc elim: continuous_on_subset) ``` lp15@64006 ` 1139` ``` then show ?thesis ``` lp15@64006 ` 1140` ``` by (rule_tac K="K \ T" and g=g in that) (auto simp: disjnt_iff Diff_Int contg) ``` lp15@64006 ` 1141` ```qed ``` lp15@64006 ` 1142` ak2110@68833 ` 1143` ```subsection%important\Extending maps to spheres\ ``` lp15@64006 ` 1144` lp15@64006 ` 1145` ```(*Up to extend_map_affine_to_sphere_cofinite_gen*) ``` lp15@64006 ` 1146` ak2110@68833 ` 1147` ```lemma%important extend_map_affine_to_sphere1: ``` lp15@64006 ` 1148` ``` fixes f :: "'a::euclidean_space \ 'b::topological_space" ``` lp15@64006 ` 1149` ``` assumes "finite K" "affine U" and contf: "continuous_on (U - K) f" ``` lp15@64006 ` 1150` ``` and fim: "f ` (U - K) \ T" ``` lp15@64006 ` 1151` ``` and comps: "\C. \C \ components(U - S); C \ K \ {}\ \ C \ L \ {}" ``` lp15@64006 ` 1152` ``` and clo: "closedin (subtopology euclidean U) S" and K: "disjnt K S" "K \ U" ``` lp15@64006 ` 1153` ``` obtains g where "continuous_on (U - L) g" "g ` (U - L) \ T" "\x. x \ S \ g x = f x" ``` ak2110@68833 ` 1154` ```proof%unimportant (cases "K = {}") ``` lp15@64006 ` 1155` ``` case True ``` lp15@64006 ` 1156` ``` then show ?thesis ``` lp15@64006 ` 1157` ``` by (metis Diff_empty Diff_subset contf fim continuous_on_subset image_subsetI rev_image_eqI subset_iff that) ``` lp15@64006 ` 1158` ```next ``` lp15@64006 ` 1159` ``` case False ``` lp15@64006 ` 1160` ``` have "S \ U" ``` lp15@64006 ` 1161` ``` using clo closedin_limpt by blast ``` lp15@64006 ` 1162` ``` then have "(U - S) \ K \ {}" ``` lp15@64006 ` 1163` ``` by (metis Diff_triv False Int_Diff K disjnt_def inf.absorb_iff2 inf_commute) ``` lp15@64006 ` 1164` ``` then have "\(components (U - S)) \ K \ {}" ``` lp15@64006 ` 1165` ``` using Union_components by simp ``` lp15@64006 ` 1166` ``` then obtain C0 where C0: "C0 \ components (U - S)" "C0 \ K \ {}" ``` lp15@64006 ` 1167` ``` by blast ``` lp15@64006 ` 1168` ``` have "convex U" ``` lp15@64006 ` 1169` ``` by (simp add: affine_imp_convex \affine U\) ``` lp15@64006 ` 1170` ``` then have "locally connected U" ``` lp15@64006 ` 1171` ``` by (rule convex_imp_locally_connected) ``` lp15@64006 ` 1172` ``` have "\a g. a \ C \ a \ L \ continuous_on (S \ (C - {a})) g \ ``` lp15@64006 ` 1173` ``` g ` (S \ (C - {a})) \ T \ (\x \ S. g x = f x)" ``` lp15@64006 ` 1174` ``` if C: "C \ components (U - S)" and CK: "C \ K \ {}" for C ``` lp15@64006 ` 1175` ``` proof - ``` lp15@64006 ` 1176` ``` have "C \ U-S" "C \ L \ {}" ``` lp15@64006 ` 1177` ``` by (simp_all add: in_components_subset comps that) ``` lp15@64006 ` 1178` ``` then obtain a where a: "a \ C" "a \ L" by auto ``` lp15@64006 ` 1179` ``` have opeUC: "openin (subtopology euclidean U) C" ``` lp15@64006 ` 1180` ``` proof (rule openin_trans) ``` lp15@64006 ` 1181` ``` show "openin (subtopology euclidean (U-S)) C" ``` lp15@64006 ` 1182` ``` by (simp add: \locally connected U\ clo locally_diff_closed openin_components_locally_connected [OF _ C]) ``` lp15@64006 ` 1183` ``` show "openin (subtopology euclidean U) (U - S)" ``` lp15@64006 ` 1184` ``` by (simp add: clo openin_diff) ``` lp15@64006 ` 1185` ``` qed ``` lp15@64006 ` 1186` ``` then obtain d where "C \ U" "0 < d" and d: "cball a d \ U \ C" ``` lp15@64006 ` 1187` ``` using openin_contains_cball by (metis \a \ C\) ``` lp15@64006 ` 1188` ``` then have "ball a d \ U \ C" ``` lp15@64006 ` 1189` ``` by auto ``` lp15@64006 ` 1190` ``` obtain h k where homhk: "homeomorphism (S \ C) (S \ C) h k" ``` nipkow@69508 ` 1191` ``` and subC: "{x. (\ (h x = x \ k x = x))} \ C" ``` nipkow@69508 ` 1192` ``` and bou: "bounded {x. (\ (h x = x \ k x = x))}" ``` lp15@64006 ` 1193` ``` and hin: "\x. x \ C \ K \ h x \ ball a d \ U" ``` lp15@64006 ` 1194` ``` proof (rule homeomorphism_grouping_points_exists_gen [of C "ball a d \ U" "C \ K" "S \ C"]) ``` lp15@64006 ` 1195` ``` show "openin (subtopology euclidean C) (ball a d \ U)" ``` lp15@66827 ` 1196` ``` by (metis open_ball \C \ U\ \ball a d \ U \ C\ inf.absorb_iff2 inf.orderE inf_assoc open_openin openin_subtopology) ``` lp15@64006 ` 1197` ``` show "openin (subtopology euclidean (affine hull C)) C" ``` lp15@64006 ` 1198` ``` by (metis \a \ C\ \openin (subtopology euclidean U) C\ affine_hull_eq affine_hull_openin all_not_in_conv \affine U\) ``` lp15@64006 ` 1199` ``` show "ball a d \ U \ {}" ``` lp15@64006 ` 1200` ``` using \0 < d\ \C \ U\ \a \ C\ by force ``` lp15@64006 ` 1201` ``` show "finite (C \ K)" ``` lp15@64006 ` 1202` ``` by (simp add: \finite K\) ``` lp15@64006 ` 1203` ``` show "S \ C \ affine hull C" ``` lp15@64006 ` 1204` ``` by (metis \C \ U\ \S \ U\ \a \ C\ opeUC affine_hull_eq affine_hull_openin all_not_in_conv assms(2) sup.bounded_iff) ``` lp15@64006 ` 1205` ``` show "connected C" ``` lp15@64006 ` 1206` ``` by (metis C in_components_connected) ``` lp15@64006 ` 1207` ``` qed auto ``` lp15@64006 ` 1208` ``` have a_BU: "a \ ball a d \ U" ``` lp15@64006 ` 1209` ``` using \0 < d\ \C \ U\ \a \ C\ by auto ``` lp15@64006 ` 1210` ``` have "rel_frontier (cball a d \ U) retract_of (affine hull (cball a d \ U) - {a})" ``` lp15@64006 ` 1211` ``` apply (rule rel_frontier_retract_of_punctured_affine_hull) ``` lp15@64006 ` 1212` ``` apply (auto simp: \convex U\ convex_Int) ``` lp15@64006 ` 1213` ``` by (metis \affine U\ convex_cball empty_iff interior_cball a_BU rel_interior_convex_Int_affine) ``` lp15@64006 ` 1214` ``` moreover have "rel_frontier (cball a d \ U) = frontier (cball a d) \ U" ``` lp15@64006 ` 1215` ``` apply (rule convex_affine_rel_frontier_Int) ``` lp15@64006 ` 1216` ``` using a_BU by (force simp: \affine U\)+ ``` lp15@64006 ` 1217` ``` moreover have "affine hull (cball a d \ U) = U" ``` lp15@64006 ` 1218` ``` by (metis \convex U\ a_BU affine_hull_convex_Int_nonempty_interior affine_hull_eq \affine U\ equals0D inf.commute interior_cball) ``` lp15@64006 ` 1219` ``` ultimately have "frontier (cball a d) \ U retract_of (U - {a})" ``` lp15@64006 ` 1220` ``` by metis ``` lp15@64006 ` 1221` ``` then obtain r where contr: "continuous_on (U - {a}) r" ``` lp15@64006 ` 1222` ``` and rim: "r ` (U - {a}) \ sphere a d" "r ` (U - {a}) \ U" ``` lp15@64006 ` 1223` ``` and req: "\x. x \ sphere a d \ U \ r x = x" ``` lp15@64006 ` 1224` ``` using \affine U\ by (auto simp: retract_of_def retraction_def hull_same) ``` lp15@64006 ` 1225` ``` define j where "j \ \x. if x \ ball a d then r x else x" ``` lp15@64006 ` 1226` ``` have kj: "\x. x \ S \ k (j x) = x" ``` lp15@64006 ` 1227` ``` using \C \ U - S\ \S \ U\ \ball a d \ U \ C\ j_def subC by auto ``` lp15@64006 ` 1228` ``` have Uaeq: "U - {a} = (cball a d - {a}) \ U \ (U - ball a d)" ``` lp15@64006 ` 1229` ``` using \0 < d\ by auto ``` lp15@64006 ` 1230` ``` have jim: "j ` (S \ (C - {a})) \ (S \ C) - ball a d" ``` lp15@64006 ` 1231` ``` proof clarify ``` lp15@64006 ` 1232` ``` fix y assume "y \ S \ (C - {a})" ``` lp15@64006 ` 1233` ``` then have "y \ U - {a}" ``` lp15@64006 ` 1234` ``` using \C \ U - S\ \S \ U\ \a \ C\ by auto ``` lp15@64006 ` 1235` ``` then have "r y \ sphere a d" ``` lp15@64006 ` 1236` ``` using rim by auto ``` lp15@64006 ` 1237` ``` then show "j y \ S \ C - ball a d" ``` lp15@64006 ` 1238` ``` apply (simp add: j_def) ``` lp15@64006 ` 1239` ``` using \r y \ sphere a d\ \y \ U - {a}\ \y \ S \ (C - {a})\ d rim by fastforce ``` lp15@64006 ` 1240` ``` qed ``` lp15@64006 ` 1241` ``` have contj: "continuous_on (U - {a}) j" ``` lp15@64006 ` 1242` ``` unfolding j_def Uaeq ``` lp15@64006 ` 1243` ``` proof (intro continuous_on_cases_local continuous_on_id, simp_all add: req closedin_closed Uaeq [symmetric]) ``` lp15@64006 ` 1244` ``` show "\T. closed T \ (cball a d - {a}) \ U = (U - {a}) \ T" ``` lp15@64006 ` 1245` ``` apply (rule_tac x="(cball a d) \ U" in exI) ``` lp15@64006 ` 1246` ``` using affine_closed \affine U\ by blast ``` lp15@64006 ` 1247` ``` show "\T. closed T \ U - ball a d = (U - {a}) \ T" ``` lp15@64006 ` 1248` ``` apply (rule_tac x="U - ball a d" in exI) ``` lp15@64006 ` 1249` ``` using \0 < d\ by (force simp: affine_closed \affine U\ closed_Diff) ``` lp15@64006 ` 1250` ``` show "continuous_on ((cball a d - {a}) \ U) r" ``` lp15@64006 ` 1251` ``` by (force intro: continuous_on_subset [OF contr]) ``` lp15@64006 ` 1252` ``` qed ``` lp15@64006 ` 1253` ``` have fT: "x \ U - K \ f x \ T" for x ``` lp15@64006 ` 1254` ``` using fim by blast ``` lp15@64006 ` 1255` ``` show ?thesis ``` lp15@64006 ` 1256` ``` proof (intro conjI exI) ``` lp15@64006 ` 1257` ``` show "continuous_on (S \ (C - {a})) (f \ k \ j)" ``` lp15@64006 ` 1258` ``` proof (intro continuous_on_compose) ``` lp15@64006 ` 1259` ``` show "continuous_on (S \ (C - {a})) j" ``` lp15@64006 ` 1260` ``` apply (rule continuous_on_subset [OF contj]) ``` lp15@64006 ` 1261` ``` using \C \ U - S\ \S \ U\ \a \ C\ by force ``` lp15@64006 ` 1262` ``` show "continuous_on (j ` (S \ (C - {a}))) k" ``` lp15@64006 ` 1263` ``` apply (rule continuous_on_subset [OF homeomorphism_cont2 [OF homhk]]) ``` lp15@64006 ` 1264` ``` using jim \C \ U - S\ \S \ U\ \ball a d \ U \ C\ j_def by fastforce ``` lp15@64006 ` 1265` ``` show "continuous_on (k ` j ` (S \ (C - {a}))) f" ``` lp15@64006 ` 1266` ``` proof (clarify intro!: continuous_on_subset [OF contf]) ``` lp15@64006 ` 1267` ``` fix y assume "y \ S \ (C - {a})" ``` lp15@64006 ` 1268` ``` have ky: "k y \ S \ C" ``` lp15@64006 ` 1269` ``` using homeomorphism_image2 [OF homhk] \y \ S \ (C - {a})\ by blast ``` lp15@64006 ` 1270` ``` have jy: "j y \ S \ C - ball a d" ``` lp15@64006 ` 1271` ``` using Un_iff \y \ S \ (C - {a})\ jim by auto ``` lp15@64006 ` 1272` ``` show "k (j y) \ U - K" ``` lp15@64006 ` 1273` ``` apply safe ``` lp15@64006 ` 1274` ``` using \C \ U\ \S \ U\ homeomorphism_image2 [OF homhk] jy apply blast ``` lp15@64006 ` 1275` ``` by (metis DiffD1 DiffD2 Int_iff Un_iff \disjnt K S\ disjnt_def empty_iff hin homeomorphism_apply2 homeomorphism_image2 homhk imageI jy) ``` lp15@64006 ` 1276` ``` qed ``` lp15@64006 ` 1277` ``` qed ``` lp15@64006 ` 1278` ``` have ST: "\x. x \ S \ (f \ k \ j) x \ T" ``` lp15@64006 ` 1279` ``` apply (simp add: kj) ``` lp15@64006 ` 1280` ``` apply (metis DiffI \S \ U\ \disjnt K S\ subsetD disjnt_iff fim image_subset_iff) ``` lp15@64006 ` 1281` ``` done ``` lp15@64006 ` 1282` ``` moreover have "(f \ k \ j) x \ T" if "x \ C" "x \ a" "x \ S" for x ``` lp15@64006 ` 1283` ``` proof - ``` lp15@64006 ` 1284` ``` have rx: "r x \ sphere a d" ``` lp15@64006 ` 1285` ``` using \C \ U\ rim that by fastforce ``` lp15@64006 ` 1286` ``` have jj: "j x \ S \ C - ball a d" ``` lp15@64006 ` 1287` ``` using jim that by blast ``` lp15@64006 ` 1288` ``` have "k (j x) = j x \ k (j x) \ C \ j x \ C" ``` lp15@64006 ` 1289` ``` by (metis Diff_iff Int_iff Un_iff \S \ U\ subsetD d j_def jj rx sphere_cball that(1)) ``` lp15@64006 ` 1290` ``` then have "k (j x) \ C" ``` lp15@64006 ` 1291` ``` using homeomorphism_apply2 [OF homhk, of "j x"] \C \ U\ \S \ U\ a rx ``` lp15@64006 ` 1292` ``` by (metis (mono_tags, lifting) Diff_iff subsetD jj mem_Collect_eq subC) ``` lp15@64006 ` 1293` ``` with jj \C \ U\ show ?thesis ``` lp15@64006 ` 1294` ``` apply safe ``` lp15@64006 ` 1295` ``` using ST j_def apply fastforce ``` lp15@64006 ` 1296` ``` apply (auto simp: not_less intro!: fT) ``` lp15@64006 ` 1297` ``` by (metis DiffD1 DiffD2 Int_iff hin homeomorphism_apply2 [OF homhk] jj) ``` lp15@64006 ` 1298` ``` qed ``` lp15@64006 ` 1299` ``` ultimately show "(f \ k \ j) ` (S \ (C - {a})) \ T" ``` lp15@64006 ` 1300` ``` by force ``` lp15@64006 ` 1301` ``` show "\x\S. (f \ k \ j) x = f x" using kj by simp ``` lp15@64006 ` 1302` ``` qed (auto simp: a) ``` lp15@64006 ` 1303` ``` qed ``` lp15@64006 ` 1304` ``` then obtain a h where ``` lp15@64006 ` 1305` ``` ah: "\C. \C \ components (U - S); C \ K \ {}\ ``` lp15@64006 ` 1306` ``` \ a C \ C \ a C \ L \ continuous_on (S \ (C - {a C})) (h C) \ ``` lp15@64006 ` 1307` ``` h C ` (S \ (C - {a C})) \ T \ (\x \ S. h C x = f x)" ``` lp15@64006 ` 1308` ``` using that by metis ``` lp15@64006 ` 1309` ``` define F where "F \ {C \ components (U - S). C \ K \ {}}" ``` lp15@64006 ` 1310` ``` define G where "G \ {C \ components (U - S). C \ K = {}}" ``` lp15@64006 ` 1311` ``` define UF where "UF \ (\C\F. C - {a C})" ``` lp15@64006 ` 1312` ``` have "C0 \ F" ``` lp15@64006 ` 1313` ``` by (auto simp: F_def C0) ``` lp15@64006 ` 1314` ``` have "finite F" ``` lp15@64006 ` 1315` ``` proof (subst finite_image_iff [of "\C. C \ K" F, symmetric]) ``` lp15@64006 ` 1316` ``` show "inj_on (\C. C \ K) F" ``` lp15@64006 ` 1317` ``` unfolding F_def inj_on_def ``` lp15@64006 ` 1318` ``` using components_nonoverlap by blast ``` lp15@64006 ` 1319` ``` show "finite ((\C. C \ K) ` F)" ``` lp15@64006 ` 1320` ``` unfolding F_def ``` lp15@64006 ` 1321` ``` by (rule finite_subset [of _ "Pow K"]) (auto simp: \finite K\) ``` lp15@64006 ` 1322` ``` qed ``` lp15@64006 ` 1323` ``` obtain g where contg: "continuous_on (S \ UF) g" ``` lp15@64006 ` 1324` ``` and gh: "\x i. \i \ F; x \ (S \ UF) \ (S \ (i - {a i}))\ ``` lp15@64006 ` 1325` ``` \ g x = h i x" ``` lp15@64006 ` 1326` ``` proof (rule pasting_lemma_exists_closed [OF \finite F\, of "S \ UF" "\C. S \ (C - {a C})" h]) ``` lp15@64006 ` 1327` ``` show "S \ UF \ (\C\F. S \ (C - {a C}))" ``` lp15@64006 ` 1328` ``` using \C0 \ F\ by (force simp: UF_def) ``` lp15@64006 ` 1329` ``` show "closedin (subtopology euclidean (S \ UF)) (S \ (C - {a C}))" ``` lp15@64006 ` 1330` ``` if "C \ F" for C ``` lp15@64006 ` 1331` ``` proof (rule closedin_closed_subset [of U "S \ C"]) ``` lp15@64006 ` 1332` ``` show "closedin (subtopology euclidean U) (S \ C)" ``` lp15@64006 ` 1333` ``` apply (rule closedin_Un_complement_component [OF \locally connected U\ clo]) ``` lp15@64006 ` 1334` ``` using F_def that by blast ``` lp15@64006 ` 1335` ``` next ``` lp15@64006 ` 1336` ``` have "x = a C'" if "C' \ F" "x \ C'" "x \ U" for x C' ``` lp15@64006 ` 1337` ``` proof - ``` lp15@64006 ` 1338` ``` have "\A. x \ \A \ C' \ A" ``` lp15@64006 ` 1339` ``` using \x \ C'\ by blast ``` lp15@64006 ` 1340` ``` with that show "x = a C'" ``` lp15@64006 ` 1341` ``` by (metis (lifting) DiffD1 F_def Union_components mem_Collect_eq) ``` lp15@64006 ` 1342` ``` qed ``` lp15@64006 ` 1343` ``` then show "S \ UF \ U" ``` lp15@64006 ` 1344` ``` using \S \ U\ by (force simp: UF_def) ``` lp15@64006 ` 1345` ``` next ``` lp15@64006 ` 1346` ``` show "S \ (C - {a C}) = (S \ C) \ (S \ UF)" ``` lp15@64006 ` 1347` ``` using F_def UF_def components_nonoverlap that by auto ``` lp15@64006 ` 1348` ``` qed ``` lp15@64006 ` 1349` ``` next ``` lp15@64006 ` 1350` ``` show "continuous_on (S \ (C' - {a C'})) (h C')" if "C' \ F" for C' ``` lp15@64006 ` 1351` ``` using ah F_def that by blast ``` lp15@64006 ` 1352` ``` show "\i j x. \i \ F; j \ F; ``` lp15@64006 ` 1353` ``` x \ (S \ UF) \ (S \ (i - {a i})) \ (S \ (j - {a j}))\ ``` lp15@64006 ` 1354` ``` \ h i x = h j x" ``` lp15@64006 ` 1355` ``` using components_eq by (fastforce simp: components_eq F_def ah) ``` lp15@64006 ` 1356` ``` qed blast ``` lp15@64006 ` 1357` ``` have SU': "S \ \G \ (S \ UF) \ U" ``` lp15@64006 ` 1358` ``` using \S \ U\ in_components_subset by (auto simp: F_def G_def UF_def) ``` lp15@64006 ` 1359` ``` have clo1: "closedin (subtopology euclidean (S \ \G \ (S \ UF))) (S \ \G)" ``` lp15@64006 ` 1360` ``` proof (rule closedin_closed_subset [OF _ SU']) ``` lp15@64006 ` 1361` ``` have *: "\C. C \ F \ openin (subtopology euclidean U) C" ``` lp15@64006 ` 1362` ``` unfolding F_def ``` lp15@64006 ` 1363` ``` by clarify (metis (no_types, lifting) \locally connected U\ clo closedin_def locally_diff_closed openin_components_locally_connected openin_trans topspace_euclidean_subtopology) ``` lp15@64006 ` 1364` ``` show "closedin (subtopology euclidean U) (U - UF)" ``` lp15@64006 ` 1365` ``` unfolding UF_def ``` lp15@64006 ` 1366` ``` by (force intro: openin_delete *) ``` lp15@64006 ` 1367` ``` show "S \ \G = (U - UF) \ (S \ \G \ (S \ UF))" ``` lp15@64006 ` 1368` ``` using \S \ U\ apply (auto simp: F_def G_def UF_def) ``` lp15@64006 ` 1369` ``` apply (metis Diff_iff UnionI Union_components) ``` lp15@64006 ` 1370` ``` apply (metis DiffD1 UnionI Union_components) ``` lp15@64006 ` 1371` ``` by (metis (no_types, lifting) IntI components_nonoverlap empty_iff) ``` lp15@64006 ` 1372` ``` qed ``` lp15@64006 ` 1373` ``` have clo2: "closedin (subtopology euclidean (S \ \G \ (S \ UF))) (S \ UF)" ``` lp15@64006 ` 1374` ``` proof (rule closedin_closed_subset [OF _ SU']) ``` lp15@64006 ` 1375` ``` show "closedin (subtopology euclidean U) (\C\F. S \ C)" ``` lp15@64006 ` 1376` ``` apply (rule closedin_Union) ``` lp15@64006 ` 1377` ``` apply (simp add: \finite F\) ``` lp15@64006 ` 1378` ``` using F_def \locally connected U\ clo closedin_Un_complement_component by blast ``` lp15@64006 ` 1379` ``` show "S \ UF = (\C\F. S \ C) \ (S \ \G \ (S \ UF))" ``` lp15@64006 ` 1380` ``` using \S \ U\ apply (auto simp: F_def G_def UF_def) ``` lp15@64006 ` 1381` ``` using C0 apply blast ``` lp15@64006 ` 1382` ``` by (metis components_nonoverlap disjnt_def disjnt_iff) ``` lp15@64006 ` 1383` ``` qed ``` lp15@64006 ` 1384` ``` have SUG: "S \ \G \ U - K" ``` lp15@64006 ` 1385` ``` using \S \ U\ K apply (auto simp: G_def disjnt_iff) ``` lp15@64006 ` 1386` ``` by (meson Diff_iff subsetD in_components_subset) ``` lp15@64006 ` 1387` ``` then have contf': "continuous_on (S \ \G) f" ``` lp15@64006 ` 1388` ``` by (rule continuous_on_subset [OF contf]) ``` lp15@64006 ` 1389` ``` have contg': "continuous_on (S \ UF) g" ``` lp15@64006 ` 1390` ``` apply (rule continuous_on_subset [OF contg]) ``` lp15@64006 ` 1391` ``` using \S \ U\ by (auto simp: F_def G_def) ``` lp15@64006 ` 1392` ``` have "\x. \S \ U; x \ S\ \ f x = g x" ``` lp15@64006 ` 1393` ``` by (subst gh) (auto simp: ah C0 intro: \C0 \ F\) ``` lp15@64006 ` 1394` ``` then have f_eq_g: "\x. x \ S \ UF \ x \ S \ \G \ f x = g x" ``` lp15@64006 ` 1395` ``` using \S \ U\ apply (auto simp: F_def G_def UF_def dest: in_components_subset) ``` lp15@64006 ` 1396` ``` using components_eq by blast ``` lp15@64006 ` 1397` ``` have cont: "continuous_on (S \ \G \ (S \ UF)) (\x. if x \ S \ \G then f x else g x)" ``` lp15@64006 ` 1398` ``` by (blast intro: continuous_on_cases_local [OF clo1 clo2 contf' contg' f_eq_g, of "\x. x \ S \ \G"]) ``` lp15@64006 ` 1399` ``` show ?thesis ``` lp15@64006 ` 1400` ``` proof ``` lp15@64006 ` 1401` ``` have UF: "\F - L \ UF" ``` lp15@64006 ` 1402` ``` unfolding F_def UF_def using ah by blast ``` lp15@64006 ` 1403` ``` have "U - S - L = \(components (U - S)) - L" ``` lp15@64006 ` 1404` ``` by simp ``` lp15@64006 ` 1405` ``` also have "... = \F \ \G - L" ``` lp15@64006 ` 1406` ``` unfolding F_def G_def by blast ``` lp15@64006 ` 1407` ``` also have "... \ UF \ \G" ``` lp15@64006 ` 1408` ``` using UF by blast ``` lp15@64006 ` 1409` ``` finally have "U - L \ S \ \G \ (S \ UF)" ``` lp15@64006 ` 1410` ``` by blast ``` lp15@64006 ` 1411` ``` then show "continuous_on (U - L) (\x. if x \ S \ \G then f x else g x)" ``` lp15@64006 ` 1412` ``` by (rule continuous_on_subset [OF cont]) ``` lp15@64006 ` 1413` ``` have "((U - L) \ {x. x \ S \ (\xa\G. x \ xa)}) \ ((U - L) \ (-S \ UF))" ``` lp15@64006 ` 1414` ``` using \U - L \ S \ \G \ (S \ UF)\ by auto ``` lp15@64006 ` 1415` ``` moreover have "g ` ((U - L) \ (-S \ UF)) \ T" ``` lp15@64006 ` 1416` ``` proof - ``` lp15@64006 ` 1417` ``` have "g x \ T" if "x \ U" "x \ L" "x \ S" "C \ F" "x \ C" "x \ a C" for x C ``` lp15@64006 ` 1418` ``` proof (subst gh) ``` lp15@64006 ` 1419` ``` show "x \ (S \ UF) \ (S \ (C - {a C}))" ``` lp15@64006 ` 1420` ``` using that by (auto simp: UF_def) ``` lp15@64006 ` 1421` ``` show "h C x \ T" ``` lp15@64006 ` 1422` ``` using ah that by (fastforce simp add: F_def) ``` lp15@64006 ` 1423` ``` qed (rule that) ``` lp15@64006 ` 1424` ``` then show ?thesis ``` lp15@64006 ` 1425` ``` by (force simp: UF_def) ``` lp15@64006 ` 1426` ``` qed ``` lp15@64006 ` 1427` ``` ultimately have "g ` ((U - L) \ {x. x \ S \ (\xa\G. x \ xa)}) \ T" ``` lp15@64006 ` 1428` ``` using image_mono order_trans by blast ``` lp15@64006 ` 1429` ``` moreover have "f ` ((U - L) \ (S \ \G)) \ T" ``` lp15@64006 ` 1430` ``` using fim SUG by blast ``` lp15@64006 ` 1431` ``` ultimately show "(\x. if x \ S \ \G then f x else g x) ` (U - L) \ T" ``` lp15@64006 ` 1432` ``` by force ``` lp15@64006 ` 1433` ``` show "\x. x \ S \ (if x \ S \ \G then f x else g x) = f x" ``` lp15@64006 ` 1434` ``` by (simp add: F_def G_def) ``` lp15@64006 ` 1435` ``` qed ``` lp15@64006 ` 1436` ```qed ``` lp15@64006 ` 1437` lp15@64006 ` 1438` ak2110@68833 ` 1439` ```lemma%important extend_map_affine_to_sphere2: ``` lp15@64006 ` 1440` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@64006 ` 1441` ``` assumes "compact S" "convex U" "bounded U" "affine T" "S \ T" ``` lp15@64006 ` 1442` ``` and affTU: "aff_dim T \ aff_dim U" ``` lp15@64006 ` 1443` ``` and contf: "continuous_on S f" ``` lp15@64006 ` 1444` ``` and fim: "f ` S \ rel_frontier U" ``` lp15@64006 ` 1445` ``` and ovlap: "\C. C \ components(T - S) \ C \ L \ {}" ``` lp15@64006 ` 1446` ``` obtains K g where "finite K" "K \ L" "K \ T" "disjnt K S" ``` lp15@64006 ` 1447` ``` "continuous_on (T - K) g" "g ` (T - K) \ rel_frontier U" ``` lp15@64006 ` 1448` ``` "\x. x \ S \ g x = f x" ``` ak2110@68833 ` 1449` ```proof%unimportant - ``` lp15@64006 ` 1450` ``` obtain K g where K: "finite K" "K \ T" "disjnt K S" ``` lp15@64006 ` 1451` ``` and contg: "continuous_on (T - K) g" ``` lp15@64006 ` 1452` ``` and gim: "g ` (T - K) \ rel_frontier U" ``` lp15@64006 ` 1453` ``` and gf: "\x. x \ S \ g x = f x" ``` lp15@64006 ` 1454` ``` using assms extend_map_affine_to_sphere_cofinite_simple by metis ``` lp15@64006 ` 1455` ``` have "(\y C. C \ components (T - S) \ x \ C \ y \ C \ y \ L)" if "x \ K" for x ``` lp15@64006 ` 1456` ``` proof - ``` lp15@64006 ` 1457` ``` have "x \ T-S" ``` lp15@64006 ` 1458` ``` using \K \ T\ \disjnt K S\ disjnt_def that by fastforce ``` lp15@64006 ` 1459` ``` then obtain C where "C \ components(T - S)" "x \ C" ``` lp15@64006 ` 1460` ``` by (metis UnionE Union_components) ``` lp15@64006 ` 1461` ``` with ovlap [of C] show ?thesis ``` lp15@64006 ` 1462` ``` by blast ``` lp15@64006 ` 1463` ``` qed ``` lp15@64006 ` 1464` ``` then obtain \ where \: "\x. x \ K \ \C. C \ components (T - S) \ x \ C \ \ x \ C \ \ x \ L" ``` lp15@64006 ` 1465` ``` by metis ``` lp15@64006 ` 1466` ``` obtain h where conth: "continuous_on (T - \ ` K) h" ``` lp15@64006 ` 1467` ``` and him: "h ` (T - \ ` K) \ rel_frontier U" ``` lp15@64006 ` 1468` ``` and hg: "\x. x \ S \ h x = g x" ``` lp15@64006 ` 1469` ``` proof (rule extend_map_affine_to_sphere1 [OF \finite K\ \affine T\ contg gim, of S "\ ` K"]) ``` lp15@64006 ` 1470` ``` show cloTS: "closedin (subtopology euclidean T) S" ``` lp15@64006 ` 1471` ``` by (simp add: \compact S\ \S \ T\ closed_subset compact_imp_closed) ``` lp15@64006 ` 1472` ``` show "\C. \C \ components (T - S); C \ K \ {}\ \ C \ \ ` K \ {}" ``` lp15@64006 ` 1473` ``` using \ components_eq by blast ``` lp15@64006 ` 1474` ``` qed (use K in auto) ``` lp15@64006 ` 1475` ``` show ?thesis ``` lp15@64006 ` 1476` ``` proof ``` lp15@64006 ` 1477` ``` show *: "\ ` K \ L" ``` lp15@64006 ` 1478` ``` using \ by blast ``` lp15@64006 ` 1479` ``` show "finite (\ ` K)" ``` lp15@64006 ` 1480` ``` by (simp add: K) ``` lp15@64006 ` 1481` ``` show "\ ` K \ T" ``` lp15@64006 ` 1482` ``` by clarify (meson \ Diff_iff contra_subsetD in_components_subset) ``` lp15@64006 ` 1483` ``` show "continuous_on (T - \ ` K) h" ``` lp15@64006 ` 1484` ``` by (rule conth) ``` lp15@64006 ` 1485` ``` show "disjnt (\ ` K) S" ``` lp15@64006 ` 1486` ``` using K ``` lp15@64006 ` 1487` ``` apply (auto simp: disjnt_def) ``` lp15@64006 ` 1488` ``` by (metis \ DiffD2 UnionI Union_components) ``` lp15@64006 ` 1489` ``` qed (simp_all add: him hg gf) ``` lp15@64006 ` 1490` ```qed ``` lp15@64006 ` 1491` lp15@64006 ` 1492` ak2110@68833 ` 1493` ```proposition%important extend_map_affine_to_sphere_cofinite_gen: ``` lp15@64006 ` 1494` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@64006 ` 1495` ``` assumes SUT: "compact S" "convex U" "bounded U" "affine T" "S \ T" ``` lp15@64006 ` 1496` ``` and aff: "aff_dim T \ aff_dim U" ``` lp15@64006 ` 1497` ``` and contf: "continuous_on S f" ``` lp15@64006 ` 1498` ``` and fim: "f ` S \ rel_frontier U" ``` lp15@64006 ` 1499` ``` and dis: "\C. \C \ components(T - S); bounded C\ \ C \ L \ {}" ``` lp15@64006 ` 1500` ``` obtains K g where "finite K" "K \ L" "K \ T" "disjnt K S" "continuous_on (T - K) g" ``` lp15@64006 ` 1501` ``` "g ` (T - K) \ rel_frontier U" ``` lp15@64006 ` 1502` ``` "\x. x \ S \ g x = f x" ``` ak2110@68833 ` 1503` ```proof%unimportant (cases "S = {}") ``` lp15@64006 ` 1504` ``` case True ``` lp15@64006 ` 1505` ``` show ?thesis ``` lp15@64006 ` 1506` ``` proof (cases "rel_frontier U = {}") ``` lp15@64006 ` 1507` ``` case True ``` lp15@64006 ` 1508` ``` with aff have "aff_dim T \ 0" ``` lp15@64006 ` 1509` ``` apply (simp add: rel_frontier_eq_empty) ``` lp15@64006 ` 1510` ``` using affine_bounded_eq_lowdim \bounded U\ order_trans by auto ``` lp15@64006 ` 1511` ``` with aff_dim_geq [of T] consider "aff_dim T = -1" | "aff_dim T = 0" ``` lp15@64006 ` 1512` ``` by linarith ``` lp15@64006 ` 1513` ``` then show ?thesis ``` lp15@64006 ` 1514` ``` proof cases ``` lp15@64006 ` 1515` ``` assume "aff_dim T = -1" ``` lp15@64006 ` 1516` ``` then have "T = {}" ``` lp15@64006 ` 1517` ``` by (simp add: aff_dim_empty) ``` lp15@64006 ` 1518` ``` then show ?thesis ``` lp15@64006 ` 1519` ``` by (rule_tac K="{}" in that) auto ``` lp15@64006 ` 1520` ``` next ``` lp15@64006 ` 1521` ``` assume "aff_dim T = 0" ``` lp15@64006 ` 1522` ``` then obtain a where "T = {a}" ``` lp15@64006 ` 1523` ``` using aff_dim_eq_0 by blast ``` lp15@64006 ` 1524` ``` then have "a \ L" ``` lp15@64006 ` 1525` ``` using dis [of "{a}"] \S = {}\ by (auto simp: in_components_self) ``` lp15@64006 ` 1526` ``` with \S = {}\ \T = {a}\ show ?thesis ``` lp15@64006 ` 1527` ``` by (rule_tac K="{a}" and g=f in that) auto ``` lp15@64006 ` 1528` ``` qed ``` lp15@64006 ` 1529` ``` next ``` lp15@64006 ` 1530` ``` case False ``` lp15@64006 ` 1531` ``` then obtain y where "y \ rel_frontier U" ``` lp15@64006 ` 1532` ``` by auto ``` lp15@64006 ` 1533` ``` with \S = {}\ show ?thesis ``` lp15@64006 ` 1534` ``` by (rule_tac K="{}" and g="\x. y" in that) (auto simp: continuous_on_const) ``` lp15@64006 ` 1535` ``` qed ``` lp15@64006 ` 1536` ```next ``` lp15@64006 ` 1537` ``` case False ``` lp15@64006 ` 1538` ``` have "bounded S" ``` lp15@64006 ` 1539` ``` by (simp add: assms compact_imp_bounded) ``` lp15@64006 ` 1540` ``` then obtain b where b: "S \ cbox (-b) b" ``` lp15@64006 ` 1541` ``` using bounded_subset_cbox_symmetric by blast ``` nipkow@69508 ` 1542` ``` define LU where "LU \ L \ (\ {C \ components (T - S). \bounded C} - cbox (-(b+One)) (b+One))" ``` lp15@64006 ` 1543` ``` obtain K g where "finite K" "K \ LU" "K \ T" "disjnt K S" ``` lp15@64006 ` 1544` ``` and contg: "continuous_on (T - K) g" ``` lp15@64006 ` 1545` ``` and gim: "g ` (T - K) \ rel_frontier U" ``` lp15@64006 ` 1546` ``` and gf: "\x. x \ S \ g x = f x" ``` lp15@64006 ` 1547` ``` proof (rule extend_map_affine_to_sphere2 [OF SUT aff contf fim]) ``` lp15@64006 ` 1548` ``` show "C \ LU \ {}" if "C \ components (T - S)" for C ``` lp15@64006 ` 1549` ``` proof (cases "bounded C") ``` lp15@64006 ` 1550` ``` case True ``` lp15@64006 ` 1551` ``` with dis that show ?thesis ``` lp15@64006 ` 1552` ``` unfolding LU_def by fastforce ``` lp15@64006 ` 1553` ``` next ``` lp15@64006 ` 1554` ``` case False ``` lp15@64006 ` 1555` ``` then have "\ bounded (\{C \ components (T - S). \ bounded C})" ``` lp15@64006 ` 1556` ``` by (metis (no_types, lifting) Sup_upper bounded_subset mem_Collect_eq that) ``` lp15@64006 ` 1557` ``` then show ?thesis ``` lp15@64006 ` 1558` ``` apply (clarsimp simp: LU_def Int_Un_distrib Diff_Int_distrib Int_UN_distrib) ``` lp15@64006 ` 1559` ``` by (metis (no_types, lifting) False Sup_upper bounded_cbox bounded_subset inf.orderE mem_Collect_eq that) ``` lp15@64006 ` 1560` ``` qed ``` lp15@64006 ` 1561` ``` qed blast ``` lp15@64006 ` 1562` ``` have *: False if "x \ cbox (- b - m *\<^sub>R One) (b + m *\<^sub>R One)" ``` lp15@64006 ` 1563` ``` "x \ box (- b - n *\<^sub>R One) (b + n *\<^sub>R One)" ``` lp15@64006 ` 1564` ``` "0 \ m" "m < n" "n \ 1" for m n x ``` lp15@64006 ` 1565` ``` using that by (auto simp: mem_box algebra_simps) ``` lp15@64006 ` 1566` ``` have "disjoint_family_on (\d. frontier (cbox (- b - d *\<^sub>R One) (b + d *\<^sub>R One))) {1 / 2..1}" ``` lp15@64006 ` 1567` ``` by (auto simp: disjoint_family_on_def neq_iff frontier_def dest: *) ``` lp15@64006 ` 1568` ``` then obtain d where d12: "1/2 \ d" "d \ 1" ``` lp15@64006 ` 1569` ``` and ddis: "disjnt K (frontier (cbox (-(b + d *\<^sub>R One)) (b + d *\<^sub>R One)))" ``` lp15@64006 ` 1570` ``` using disjoint_family_elem_disjnt [of "{1/2..1::real}" K "\d. frontier (cbox (-(b + d *\<^sub>R One)) (b + d *\<^sub>R One))"] ``` lp15@64006 ` 1571` ``` by (auto simp: \finite K\) ``` lp15@64006 ` 1572` ``` define c where "c \ b + d *\<^sub>R One" ``` lp15@64006 ` 1573` ``` have cbsub: "cbox (-b) b \ box (-c) c" ``` lp15@64006 ` 1574` ``` "cbox (-b) b \ cbox (-c) c" ``` lp15@64006 ` 1575` ``` "cbox (-c) c \ cbox (-(b+One)) (b+One)" ``` lp15@64006 ` 1576` ``` using d12 by (simp_all add: subset_box c_def inner_diff_left inner_left_distrib) ``` lp15@64006 ` 1577` ``` have clo_cT: "closed (cbox (- c) c \ T)" ``` lp15@64006 ` 1578` ``` using affine_closed \affine T\ by blast ``` lp15@64006 ` 1579` ``` have cT_ne: "cbox (- c) c \ T \ {}" ``` lp15@64006 ` 1580` ``` using \S \ {}\ \S \ T\ b cbsub by fastforce ``` lp15@64006 ` 1581` ``` have S_sub_cc: "S \ cbox (- c) c" ``` lp15@64006 ` 1582` ``` using \cbox (- b) b \ cbox (- c) c\ b by auto ``` lp15@64006 ` 1583` ``` show ?thesis ``` lp15@64006 ` 1584` ``` proof ``` lp15@64006 ` 1585` ``` show "finite (K \ cbox (-(b+One)) (b+One))" ``` lp15@64006 ` 1586` ``` using \finite K\ by blast ``` lp15@64006 ` 1587` ``` show "K \ cbox (- (b + One)) (b + One) \ L" ``` lp15@64006 ` 1588` ``` using \K \ LU\ by (auto simp: LU_def) ``` lp15@64006 ` 1589` ``` show "K \ cbox (- (b + One)) (b + One) \ T" ``` lp15@64006 ` 1590` ``` using \K \ T\ by auto ``` lp15@64006 ` 1591` ``` show "disjnt (K \ cbox (- (b + One)) (b + One)) S" ``` lp15@64006 ` 1592` ``` using \disjnt K S\ by (simp add: disjnt_def disjoint_eq_subset_Compl inf.coboundedI1) ``` lp15@64006 ` 1593` ``` have cloTK: "closest_point (cbox (- c) c \ T) x \ T - K" ``` lp15@64006 ` 1594` ``` if "x \ T" and Knot: "x \ K \ x \ cbox (- b - One) (b + One)" for x ``` lp15@64006 ` 1595` ``` proof (cases "x \ cbox (- c) c") ``` lp15@64006 ` 1596` ``` case True ``` lp15@64006 ` 1597` ``` with \x \ T\ show ?thesis ``` lp15@64006 ` 1598` ``` using cbsub(3) Knot by (force simp: closest_point_self) ``` lp15@64006 ` 1599` ``` next ``` lp15@64006 ` 1600` ``` case False ``` lp15@64006 ` 1601` ``` have clo_in_rf: "closest_point (cbox (- c) c \ T) x \ rel_frontier (cbox (- c) c \ T)" ``` lp15@64006 ` 1602` ``` proof (intro closest_point_in_rel_frontier [OF clo_cT cT_ne] DiffI notI) ``` lp15@64006 ` 1603` ``` have "T \ interior (cbox (- c) c) \ {}" ``` lp15@64006 ` 1604` ``` using \S \ {}\ \S \ T\ b cbsub(1) by fastforce ``` lp15@64006 ` 1605` ``` then show "x \ affine hull (cbox (- c) c \ T)" ``` lp15@64006 ` 1606` ``` by (simp add: Int_commute affine_hull_affine_Int_nonempty_interior \affine T\ hull_inc that(1)) ``` lp15@64006 ` 1607` ``` next ``` lp15@64006 ` 1608` ``` show "False" if "x \ rel_interior (cbox (- c) c \ T)" ``` lp15@64006 ` 1609` ``` proof - ``` lp15@64006 ` 1610` ``` have "interior (cbox (- c) c) \ T \ {}" ``` lp15@64006 ` 1611` ``` using \S \ {}\ \S \ T\ b cbsub(1) by fastforce ``` lp15@64006 ` 1612` ``` then have "affine hull (T \ cbox (- c) c) = T" ``` lp15@64006 ` 1613` ``` using affine_hull_convex_Int_nonempty_interior [of T "cbox (- c) c"] ``` lp15@64006 ` 1614` ``` by (simp add: affine_imp_convex \affine T\ inf_commute) ``` lp15@64006 ` 1615` ``` then show ?thesis ``` lp15@64006 ` 1616` ``` by (meson subsetD le_inf_iff rel_interior_subset that False) ``` lp15@64006 ` 1617` ``` qed ``` lp15@64006 ` 1618` ``` qed ``` lp15@64006 ` 1619` ``` have "closest_point (cbox (- c) c \ T) x \ K" ``` lp15@64006 ` 1620` ``` proof ``` lp15@64006 ` 1621` ``` assume inK: "closest_point (cbox (- c) c \ T) x \ K" ``` lp15@64006 ` 1622` ``` have "\x. x \ K \ x \ frontier (cbox (- (b + d *\<^sub>R One)) (b + d *\<^sub>R One))" ``` lp15@64006 ` 1623` ``` by (metis ddis disjnt_iff) ``` lp15@64006 ` 1624` ``` then show False ``` lp15@64006 ` 1625` ``` by (metis DiffI Int_iff \affine T\ cT_ne c_def clo_cT clo_in_rf closest_point_in_set ``` lp15@64006 ` 1626` ``` convex_affine_rel_frontier_Int convex_box(1) empty_iff frontier_cbox inK interior_cbox) ``` lp15@64006 ` 1627` ``` qed ``` lp15@64006 ` 1628` ``` then show ?thesis ``` lp15@64006 ` 1629` ``` using cT_ne clo_cT closest_point_in_set by blast ``` lp15@64006 ` 1630` ``` qed ``` lp15@64006 ` 1631` ``` show "continuous_on (T - K \ cbox (- (b + One)) (b + One)) (g \ closest_point (cbox (-c) c \ T))" ``` lp15@64006 ` 1632` ``` apply (intro continuous_on_compose continuous_on_closest_point continuous_on_subset [OF contg]) ``` lp15@64006 ` 1633` ``` apply (simp_all add: clo_cT affine_imp_convex \affine T\ convex_Int cT_ne) ``` lp15@64006 ` 1634` ``` using cloTK by blast ``` lp15@64006 ` 1635` ``` have "g (closest_point (cbox (- c) c \ T) x) \ rel_frontier U" ``` lp15@64006 ` 1636` ``` if "x \ T" "x \ K \ x \ cbox (- b - One) (b + One)" for x ``` lp15@64006 ` 1637` ``` apply (rule gim [THEN subsetD]) ``` lp15@64006 ` 1638` ``` using that cloTK by blast ``` lp15@64006 ` 1639` ``` then show "(g \ closest_point (cbox (- c) c \ T)) ` (T - K \ cbox (- (b + One)) (b + One)) ``` lp15@64006 ` 1640` ``` \ rel_frontier U" ``` lp15@64006 ` 1641` ``` by force ``` lp15@64006 ` 1642` ``` show "\x. x \ S \ (g \ closest_point (cbox (- c) c \ T)) x = f x" ``` lp15@64006 ` 1643` ``` by simp (metis (mono_tags, lifting) IntI \S \ T\ cT_ne clo_cT closest_point_refl gf subsetD S_sub_cc) ``` lp15@64006 ` 1644` ``` qed ``` lp15@64006 ` 1645` ```qed ``` lp15@64006 ` 1646` lp15@64006 ` 1647` ak2110@68833 ` 1648` ```corollary%important extend_map_affine_to_sphere_cofinite: ``` lp15@64006 ` 1649` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@64006 ` 1650` ``` assumes SUT: "compact S" "affine T" "S \ T" ``` lp15@64006 ` 1651` ``` and aff: "aff_dim T \ DIM('b)" and "0 \ r" ``` lp15@64006 ` 1652` ``` and contf: "continuous_on S f" ``` lp15@64006 ` 1653` ``` and fim: "f ` S \ sphere a r" ``` lp15@64006 ` 1654` ``` and dis: "\C. \C \ components(T - S); bounded C\ \ C \ L \ {}" ``` lp15@64006 ` 1655` ``` obtains K g where "finite K" "K \ L" "K \ T" "disjnt K S" "continuous_on (T - K) g" ``` lp15@64006 ` 1656` ``` "g ` (T - K) \ sphere a r" "\x. x \ S \ g x = f x" ``` ak2110@68833 ` 1657` ```proof%unimportant (cases "r = 0") ``` lp15@64006 ` 1658` ``` case True ``` lp15@64006 ` 1659` ``` with fim show ?thesis ``` lp15@64006 ` 1660` ``` by (rule_tac K="{}" and g = "\x. a" in that) (auto simp: continuous_on_const) ``` lp15@64006 ` 1661` ```next ``` lp15@64006 ` 1662` ``` case False ``` lp15@64006 ` 1663` ``` with assms have "0 < r" by auto ``` lp15@64006 ` 1664` ``` then have "aff_dim T \ aff_dim (cball a r)" ``` lp15@64006 ` 1665` ``` by (simp add: aff aff_dim_cball) ``` lp15@64006 ` 1666` ``` then show ?thesis ``` lp15@64006 ` 1667` ``` apply (rule extend_map_affine_to_sphere_cofinite_gen ``` lp15@64006 ` 1668` ``` [OF \compact S\ convex_cball bounded_cball \affine T\ \S \ T\ _ contf]) ``` lp15@64006 ` 1669` ``` using fim apply (auto simp: assms False that dest: dis) ``` lp15@64006 ` 1670` ``` done ``` lp15@64006 ` 1671` ```qed ``` lp15@64006 ` 1672` ak2110@68833 ` 1673` ```corollary%important extend_map_UNIV_to_sphere_cofinite: ``` lp15@64006 ` 1674` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@64006 ` 1675` ``` assumes aff: "DIM('a) \ DIM('b)" and "0 \ r" ``` lp15@64006 ` 1676` ``` and SUT: "compact S" ``` lp15@64006 ` 1677` ``` and contf: "continuous_on S f" ``` lp15@64006 ` 1678` ``` and fim: "f ` S \ sphere a r" ``` lp15@64006 ` 1679` ``` and dis: "\C. \C \ components(- S); bounded C\ \ C \ L \ {}" ``` lp15@64006 ` 1680` ``` obtains K g where "finite K" "K \ L" "disjnt K S" "continuous_on (- K) g" ``` lp15@64006 ` 1681` ``` "g ` (- K) \ sphere a r" "\x. x \ S \ g x = f x" ``` lp15@64006 ` 1682` ```apply (rule extend_map_affine_to_sphere_cofinite ``` lp15@64006 ` 1683` ``` [OF \compact S\ affine_UNIV subset_UNIV _ \0 \ r\ contf fim dis]) ``` lp15@64006 ` 1684` ``` apply (auto simp: assms that Compl_eq_Diff_UNIV [symmetric]) ``` lp15@64006 ` 1685` ```done ``` lp15@64006 ` 1686` ak2110@68833 ` 1687` ```corollary%important extend_map_UNIV_to_sphere_no_bounded_component: ``` lp15@64006 ` 1688` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@64006 ` 1689` ``` assumes aff: "DIM('a) \ DIM('b)" and "0 \ r" ``` lp15@64006 ` 1690` ``` and SUT: "compact S" ``` lp15@64006 ` 1691` ``` and contf: "continuous_on S f" ``` lp15@64006 ` 1692` ``` and fim: "f ` S \ sphere a r" ``` lp15@64006 ` 1693` ``` and dis: "\C. C \ components(- S) \ \ bounded C" ``` lp15@64006 ` 1694` ``` obtains g where "continuous_on UNIV g" "g ` UNIV \ sphere a r" "\x. x \ S \ g x = f x" ``` lp15@64006 ` 1695` ```apply (rule extend_map_UNIV_to_sphere_cofinite [OF aff \0 \ r\ \compact S\ contf fim, of "{}"]) ``` lp15@64006 ` 1696` ``` apply (auto simp: that dest: dis) ``` lp15@64006 ` 1697` ```done ``` lp15@64006 ` 1698` ak2110@68833 ` 1699` ```theorem%important Borsuk_separation_theorem_gen: ``` lp15@64006 ` 1700` ``` fixes S :: "'a::euclidean_space set" ``` lp15@64006 ` 1701` ``` assumes "compact S" ``` nipkow@69508 ` 1702` ``` shows "(\c \ components(- S). \bounded c) \ ``` lp15@64006 ` 1703` ``` (\f. continuous_on S f \ f ` S \ sphere (0::'a) 1 ``` lp15@64006 ` 1704` ``` \ (\c. homotopic_with (\x. True) S (sphere 0 1) f (\x. c)))" ``` lp15@64006 ` 1705` ``` (is "?lhs = ?rhs") ``` ak2110@68833 ` 1706` ```proof%unimportant ``` lp15@64006 ` 1707` ``` assume L [rule_format]: ?lhs ``` lp15@64006 ` 1708` ``` show ?rhs ``` lp15@64006 ` 1709` ``` proof clarify ``` lp15@64006 ` 1710` ``` fix f :: "'a \ 'a" ``` lp15@64006 ` 1711` ``` assume contf: "continuous_on S f" and fim: "f ` S \ sphere 0 1" ``` lp15@64006 ` 1712` ``` obtain g where contg: "continuous_on UNIV g" and gim: "range g \ sphere 0 1" ``` lp15@64006 ` 1713` ``` and gf: "\x. x \ S \ g x = f x" ``` lp15@64006 ` 1714` ``` by (rule extend_map_UNIV_to_sphere_no_bounded_component [OF _ _ \compact S\ contf fim L]) auto ``` lp15@64006 ` 1715` ``` then show "\c. homotopic_with (\x. True) S (sphere 0 1) f (\x. c)" ``` lp15@64006 ` 1716` ``` using nullhomotopic_from_contractible [OF contg gim] ``` lp15@64006 ` 1717` ``` by (metis assms compact_imp_closed contf empty_iff fim homotopic_with_equal nullhomotopic_into_sphere_extension) ``` lp15@64006 ` 1718` ``` qed ``` lp15@64006 ` 1719` ```next ``` lp15@64006 ` 1720` ``` assume R [rule_format]: ?rhs ``` lp15@64006 ` 1721` ``` show ?lhs ``` lp15@64006 ` 1722` ``` unfolding components_def ``` lp15@64006 ` 1723` ``` proof clarify ``` lp15@64006 ` 1724` ``` fix a ``` lp15@64006 ` 1725` ``` assume "a \ S" and a: "bounded (connected_component_set (- S) a)" ``` lp15@64006 ` 1726` ``` have cont: "continuous_on S (\x. inverse(norm(x - a)) *\<^sub>R (x - a))" ``` lp15@64006 ` 1727` ``` apply (intro continuous_intros) ``` lp15@64006 ` 1728` ``` using \a \ S\ by auto ``` lp15@64006 ` 1729` ``` have im: "(\x. inverse(norm(x - a)) *\<^sub>R (x - a)) ` S \ sphere 0 1" ``` lp15@64006 ` 1730` ``` by clarsimp (metis \a \ S\ eq_iff_diff_eq_0 left_inverse norm_eq_zero) ``` lp15@64006 ` 1731` ``` show False ``` lp15@64006 ` 1732` ``` using R cont im Borsuk_map_essential_bounded_component [OF \compact S\ \a \ S\] a by blast ``` lp15@64006 ` 1733` ``` qed ``` lp15@64006 ` 1734` ```qed ``` lp15@64006 ` 1735` lp15@64006 ` 1736` ak2110@68833 ` 1737` ```corollary%important Borsuk_separation_theorem: ``` lp15@64006 ` 1738` ``` fixes S :: "'a::euclidean_space set" ``` lp15@64006 ` 1739` ``` assumes "compact S" and 2: "2 \ DIM('a)" ``` lp15@64006 ` 1740` ``` shows "connected(- S) \ ``` lp15@64006 ` 1741` ``` (\f. continuous_on S f \ f ` S \ sphere (0::'a) 1 ``` lp15@64006 ` 1742` ``` \ (\c. homotopic_with (\x. True) S (sphere 0 1) f (\x. c)))" ``` lp15@64006 ` 1743` ``` (is "?lhs = ?rhs") ``` ak2110@68833 ` 1744` ```proof%unimportant ``` lp15@64006 ` 1745` ``` assume L: ?lhs ``` lp15@64006 ` 1746` ``` show ?rhs ``` lp15@64006 ` 1747` ``` proof (cases "S = {}") ``` lp15@64006 ` 1748` ``` case True ``` lp15@64006 ` 1749` ``` then show ?thesis by auto ``` lp15@64006 ` 1750` ``` next ``` lp15@64006 ` 1751` ``` case False ``` lp15@64006 ` 1752` ``` then have "(\c\components (- S). \ bounded c)" ``` lp15@64006 ` 1753` ``` by (metis L assms(1) bounded_empty cobounded_imp_unbounded compact_imp_bounded in_components_maximal order_refl) ``` lp15@64006 ` 1754` ``` then show ?thesis ``` lp15@64006 ` 1755` ``` by (simp add: Borsuk_separation_theorem_gen [OF \compact S\]) ``` lp15@64006 ` 1756` ``` qed ``` lp15@64006 ` 1757` ```next ``` lp15@64006 ` 1758` ``` assume R: ?rhs ``` lp15@64006 ` 1759` ``` then show ?lhs ``` lp15@64006 ` 1760` ``` apply (simp add: Borsuk_separation_theorem_gen [OF \compact S\, symmetric]) ``` lp15@64006 ` 1761` ``` apply (auto simp: components_def connected_iff_eq_connected_component_set) ``` lp15@64006 ` 1762` ``` using connected_component_in apply fastforce ``` lp15@64006 ` 1763` ``` using cobounded_unique_unbounded_component [OF _ 2, of "-S"] \compact S\ compact_eq_bounded_closed by fastforce ``` lp15@64006 ` 1764` ```qed ``` lp15@64006 ` 1765` lp15@64006 ` 1766` ak2110@68833 ` 1767` ```lemma%unimportant homotopy_eqv_separation: ``` lp15@64006 ` 1768` ``` fixes S :: "'a::euclidean_space set" and T :: "'a set" ``` lp15@64006 ` 1769` ``` assumes "S homotopy_eqv T" and "compact S" and "compact T" ``` lp15@64006 ` 1770` ``` shows "connected(- S) \ connected(- T)" ``` lp15@64006 ` 1771` ```proof - ``` lp15@64006 ` 1772` ``` consider "DIM('a) = 1" | "2 \ DIM('a)" ``` lp15@64006 ` 1773` ``` by (metis DIM_ge_Suc0 One_nat_def Suc_1 dual_order.antisym not_less_eq_eq) ``` lp15@64006 ` 1774` ``` then show ?thesis ``` lp15@64006 ` 1775` ``` proof cases ``` lp15@64006 ` 1776` ``` case 1 ``` lp15@64006 ` 1777` ``` then show ?thesis ``` lp15@64006 ` 1778` ``` using bounded_connected_Compl_1 compact_imp_bounded homotopy_eqv_empty1 homotopy_eqv_empty2 assms by metis ``` lp15@64006 ` 1779` ``` next ``` lp15@64006 ` 1780` ``` case 2 ``` lp15@64006 ` 1781` ``` with assms show ?thesis ``` lp15@64006 ` 1782` ``` by (simp add: Borsuk_separation_theorem homotopy_eqv_cohomotopic_triviality_null) ``` lp15@64006 ` 1783` ``` qed ``` lp15@64006 ` 1784` ```qed ``` lp15@64006 ` 1785` ak2110@68833 ` 1786` ```lemma%important Jordan_Brouwer_separation: ``` lp15@64006 ` 1787` ``` fixes S :: "'a::euclidean_space set" and a::'a ``` lp15@64006 ` 1788` ``` assumes hom: "S homeomorphic sphere a r" and "0 < r" ``` lp15@64006 ` 1789` ``` shows "\ connected(- S)" ``` ak2110@68833 ` 1790` ```proof%unimportant - ``` lp15@64006 ` 1791` ``` have "- sphere a r \ ball a r \ {}" ``` lp15@64006 ` 1792` ``` using \0 < r\ by (simp add: Int_absorb1 subset_eq) ``` lp15@64006 ` 1793` ``` moreover ``` lp15@64006 ` 1794` ``` have eq: "- sphere a r - ball a r = - cball a r" ``` lp15@64006 ` 1795` ``` by auto ``` lp15@64006 ` 1796` ``` have "- cball a r \ {}" ``` lp15@64006 ` 1797` ``` proof - ``` lp15@64006 ` 1798` ``` have "frontier (cball a r) \ {}" ``` lp15@64006 ` 1799` ``` using \0 < r\ by auto ``` lp15@64006 ` 1800` ``` then show ?thesis ``` lp15@64006 ` 1801` ``` by (metis frontier_complement frontier_empty) ``` lp15@64006 ` 1802` ``` qed ``` lp15@64006 ` 1803` ``` with eq have "- sphere a r - ball a r \ {}" ``` lp15@64006 ` 1804` ``` by auto ``` lp15@64006 ` 1805` ``` moreover ``` lp15@64006 ` 1806` ``` have "connected (- S) = connected (- sphere a r)" ``` lp15@64006 ` 1807` ``` proof (rule homotopy_eqv_separation) ``` lp15@64006 ` 1808` ``` show "S homotopy_eqv sphere a r" ``` lp15@64006 ` 1809` ``` using hom homeomorphic_imp_homotopy_eqv by blast ``` lp15@64006 ` 1810` ``` show "compact (sphere a r)" ``` lp15@64006 ` 1811` ``` by simp ``` lp15@64006 ` 1812` ``` then show " compact S" ``` lp15@64006 ` 1813` ``` using hom homeomorphic_compactness by blast ``` lp15@64006 ` 1814` ``` qed ``` lp15@64006 ` 1815` ``` ultimately show ?thesis ``` lp15@64006 ` 1816` ``` using connected_Int_frontier [of "- sphere a r" "ball a r"] by (auto simp: \0 < r\) ``` lp15@64006 ` 1817` ```qed ``` lp15@64006 ` 1818` lp15@64006 ` 1819` ak2110@68833 ` 1820` ```lemma%important Jordan_Brouwer_frontier: ``` lp15@64006 ` 1821` ``` fixes S :: "'a::euclidean_space set" and a::'a ``` lp15@64006 ` 1822` ``` assumes S: "S homeomorphic sphere a r" and T: "T \ components(- S)" and 2: "2 \ DIM('a)" ``` lp15@64006 ` 1823` ``` shows "frontier T = S" ``` ak2110@68833 ` 1824` ```proof%unimportant (cases r rule: linorder_cases) ``` lp15@64006 ` 1825` ``` assume "r < 0" ``` lp15@64006 ` 1826` ``` with S T show ?thesis by auto ``` lp15@64006 ` 1827` ```next ``` lp15@64006 ` 1828` ``` assume "r = 0" ``` lp15@64006 ` 1829` ``` with S T card_eq_SucD obtain b where "S = {b}" ``` lp15@64006 ` 1830` ``` by (auto simp: homeomorphic_finite [of "{a}" S]) ``` lp15@64006 ` 1831` ``` have "components (- {b}) = { -{b}}" ``` lp15@64006 ` 1832` ``` using T \S = {b}\ by (auto simp: components_eq_sing_iff connected_punctured_universe 2) ``` lp15@64006 ` 1833` ``` with T show ?thesis ``` lp15@64006 ` 1834` ``` by (metis \S = {b}\ cball_trivial frontier_cball frontier_complement singletonD sphere_trivial) ``` lp15@64006 ` 1835` ```next ``` lp15@64006 ` 1836` ``` assume "r > 0" ``` lp15@64006 ` 1837` ``` have "compact S" ``` lp15@64006 ` 1838` ``` using homeomorphic_compactness compact_sphere S by blast ``` lp15@64006 ` 1839` ``` show ?thesis ``` lp15@64006 ` 1840` ``` proof (rule frontier_minimal_separating_closed) ``` lp15@64006 ` 1841` ``` show "closed S" ``` lp15@64006 ` 1842` ``` using \compact S\ compact_eq_bounded_closed by blast ``` lp15@64006 ` 1843` ``` show "\ connected (- S)" ``` lp15@64006 ` 1844` ``` using Jordan_Brouwer_separation S \0 < r\ by blast ``` lp15@64006 ` 1845` ``` obtain f g where hom: "homeomorphism S (sphere a r) f g" ``` lp15@64006 ` 1846` ``` using S by (auto simp: homeomorphic_def) ``` lp15@64006 ` 1847` ``` show "connected (- T)" if "closed T" "T \ S" for T ``` lp15@64006 ` 1848` ``` proof - ``` lp15@64006 ` 1849` ``` have "f ` T \ sphere a r" ``` lp15@64006 ` 1850` ``` using \T \ S\ hom homeomorphism_image1 by blast ``` lp15@64006 ` 1851` ``` moreover have "f ` T \ sphere a r" ``` lp15@64006 ` 1852` ``` using \T \ S\ hom ``` lp15@64006 ` 1853` ``` by (metis homeomorphism_image2 homeomorphism_of_subsets order_refl psubsetE) ``` lp15@64006 ` 1854` ``` ultimately have "f ` T \ sphere a r" by blast ``` lp15@64006 ` 1855` ``` then have "connected (- f ` T)" ``` lp15@64006 ` 1856` ``` by (rule psubset_sphere_Compl_connected [OF _ \0 < r\ 2]) ``` lp15@64006 ` 1857` ``` moreover have "compact T" ``` lp15@64006 ` 1858` ``` using \compact S\ bounded_subset compact_eq_bounded_closed that by blast ``` lp15@64006 ` 1859` ``` moreover then have "compact (f ` T)" ``` lp15@64006 ` 1860` ``` by (meson compact_continuous_image continuous_on_subset hom homeomorphism_def psubsetE \T \ S\) ``` lp15@64006 ` 1861` ``` moreover have "T homotopy_eqv f ` T" ``` lp15@64006 ` 1862` ``` by (meson \f ` T \ sphere a r\ dual_order.strict_implies_order hom homeomorphic_def homeomorphic_imp_homotopy_eqv homeomorphism_of_subsets \T \ S\) ``` lp15@64006 ` 1863` ``` ultimately show ?thesis ``` lp15@64006 ` 1864` ``` using homotopy_eqv_separation [of T "f`T"] by blast ``` lp15@64006 ` 1865` ``` qed ``` lp15@64006 ` 1866` ``` qed (rule T) ``` lp15@64006 ` 1867` ```qed ``` lp15@64006 ` 1868` ak2110@68833 ` 1869` ```lemma%important Jordan_Brouwer_nonseparation: ``` lp15@64006 ` 1870` ``` fixes S :: "'a::euclidean_space set" and a::'a ``` lp15@64006 ` 1871` ``` assumes S: "S homeomorphic sphere a r" and "T \ S" and 2: "2 \ DIM('a)" ``` lp15@64006 ` 1872` ``` shows "connected(- T)" ``` ak2110@68833 ` 1873` ```proof%unimportant - ``` lp15@64006 ` 1874` ``` have *: "connected(C \ (S - T))" if "C \ components(- S)" for C ``` lp15@64006 ` 1875` ``` proof (rule connected_intermediate_closure) ``` lp15@64006 ` 1876` ``` show "connected C" ``` lp15@64006 ` 1877` ``` using in_components_connected that by auto ``` lp15@64006 ` 1878` ``` have "S = frontier C" ``` lp15@64006 ` 1879` ``` using "2" Jordan_Brouwer_frontier S that by blast ``` lp15@64006 ` 1880` ``` with closure_subset show "C \ (S - T) \ closure C" ``` lp15@64006 ` 1881` ``` by (auto simp: frontier_def) ``` lp15@64006 ` 1882` ``` qed auto ``` lp15@64006 ` 1883` ``` have "components(- S) \ {}" ``` lp15@64006 ` 1884` ``` by (metis S bounded_empty cobounded_imp_unbounded compact_eq_bounded_closed compact_sphere ``` lp15@64006 ` 1885` ``` components_eq_empty homeomorphic_compactness) ``` lp15@64006 ` 1886` ``` then have "- T = (\C \ components(- S). C \ (S - T))" ``` lp15@64006 ` 1887` ``` using Union_components [of "-S"] \T \ S\ by auto ``` lp15@64006 ` 1888` ``` then show ?thesis ``` lp15@64006 ` 1889` ``` apply (rule ssubst) ``` lp15@64006 ` 1890` ``` apply (rule connected_Union) ``` lp15@64006 ` 1891` ``` using \T \ S\ apply (auto simp: *) ``` lp15@64006 ` 1892` ``` done ``` lp15@64006 ` 1893` ```qed ``` lp15@64006 ` 1894` ak2110@68833 ` 1895` ```subsection%important\ Invariance of domain and corollaries\ ``` ak2110@68833 ` 1896` ak2110@68833 ` 1897` ```lemma%unimportant invariance_of_domain_ball: ``` lp15@64122 ` 1898` ``` fixes f :: "'a \ 'a::euclidean_space" ``` lp15@64122 ` 1899` ``` assumes contf: "continuous_on (cball a r) f" and "0 < r" ``` lp15@64122 ` 1900` ``` and inj: "inj_on f (cball a r)" ``` lp15@64122 ` 1901` ``` shows "open(f ` ball a r)" ``` lp15@64122 ` 1902` ```proof (cases "DIM('a) = 1") ``` lp15@64122 ` 1903` ``` case True ``` lp15@64122 ` 1904` ``` obtain h::"'a\real" and k ``` lp15@64122 ` 1905` ``` where "linear h" "linear k" "h ` UNIV = UNIV" "k ` UNIV = UNIV" ``` lp15@64122 ` 1906` ``` "\x. norm(h x) = norm x" "\x. norm(k x) = norm x" ``` lp15@64122 ` 1907` ``` "\x. k(h x) = x" "\x. h(k x) = x" ``` lp15@64122 ` 1908` ``` apply (rule isomorphisms_UNIV_UNIV [where 'M='a and 'N=real]) ``` lp15@64122 ` 1909` ``` using True ``` lp15@64122 ` 1910` ``` apply force ``` lp15@64122 ` 1911` ``` by (metis UNIV_I UNIV_eq_I imageI) ``` lp15@64122 ` 1912` ``` have cont: "continuous_on S h" "continuous_on T k" for S T ``` lp15@64122 ` 1913` ``` by (simp_all add: \linear h\ \linear k\ linear_continuous_on linear_linear) ``` lp15@64122 ` 1914` ``` have "continuous_on (h ` cball a r) (h \ f \ k)" ``` lp15@64122 ` 1915` ``` apply (intro continuous_on_compose cont continuous_on_subset [OF contf]) ``` lp15@64122 ` 1916` ``` apply (auto simp: \\x. k (h x) = x\) ``` lp15@64122 ` 1917` ``` done ``` lp15@64122 ` 1918` ``` moreover have "is_interval (h ` cball a r)" ``` lp15@64122 ` 1919` ``` by (simp add: is_interval_connected_1 \linear h\ linear_continuous_on linear_linear connected_continuous_image) ``` lp15@64122 ` 1920` ``` moreover have "inj_on (h \ f \ k) (h ` cball a r)" ``` lp15@64122 ` 1921` ``` using inj by (simp add: inj_on_def) (metis \\x. k (h x) = x\) ``` lp15@64122 ` 1922` ``` ultimately have *: "\T. \open T; T \ h ` cball a r\ \ open ((h \ f \ k) ` T)" ``` lp15@64122 ` 1923` ``` using injective_eq_1d_open_map_UNIV by blast ``` lp15@64122 ` 1924` ``` have "open ((h \ f \ k) ` (h ` ball a r))" ``` lp15@64122 ` 1925` ``` by (rule *) (auto simp: \linear h\ \range h = UNIV\ open_surjective_linear_image) ``` lp15@64122 ` 1926` ``` then have "open ((h \ f) ` ball a r)" ``` lp15@64122 ` 1927` ``` by (simp add: image_comp \\x. k (h x) = x\ cong: image_cong) ``` lp15@64122 ` 1928` ``` then show ?thesis ``` lp15@64122 ` 1929` ``` apply (simp add: image_comp [symmetric]) ``` lp15@64122 ` 1930` ``` apply (metis open_bijective_linear_image_eq \linear h\ \\x. k (h x) = x\ \range h = UNIV\ bijI inj_on_def) ``` lp15@64122 ` 1931` ``` done ``` lp15@64122 ` 1932` ```next ``` lp15@64122 ` 1933` ``` case False ``` lp15@64122 ` 1934` ``` then have 2: "DIM('a) \ 2" ``` lp15@64122 ` 1935` ``` by (metis DIM_ge_Suc0 One_nat_def Suc_1 antisym not_less_eq_eq) ``` lp15@64122 ` 1936` ``` have fimsub: "f ` ball a r \ - f ` sphere a r" ``` lp15@64122 ` 1937` ``` using inj by clarsimp (metis inj_onD less_eq_real_def mem_cball order_less_irrefl) ``` lp15@64122 ` 1938` ``` have hom: "f ` sphere a r homeomorphic sphere a r" ``` lp15@64122 ` 1939` ``` by (meson compact_sphere contf continuous_on_subset homeomorphic_compact homeomorphic_sym inj inj_on_subset sphere_cball) ``` lp15@64122 ` 1940` ``` then have nconn: "\ connected (- f ` sphere a r)" ``` lp15@64122 ` 1941` ``` by (rule Jordan_Brouwer_separation) (auto simp: \0 < r\) ``` lp15@64122 ` 1942` ``` obtain C where C: "C \ components (- f ` sphere a r)" and "bounded C" ``` lp15@64122 ` 1943` ``` apply (rule cobounded_has_bounded_component [OF _ nconn]) ``` lp15@64122 ` 1944` ``` apply (simp_all add: 2) ``` lp15@64122 ` 1945` ``` by (meson compact_imp_bounded compact_continuous_image_eq compact_sphere contf inj sphere_cball) ``` lp15@64122 ` 1946` ``` moreover have "f ` (ball a r) = C" ``` lp15@64122 ` 1947` ``` proof ``` lp15@64122 ` 1948` ``` have "C \ {}" ``` lp15@64122 ` 1949` ``` by (rule in_components_nonempty [OF C]) ``` lp15@64122 ` 1950` ``` show "C \ f ` ball a r" ``` lp15@64122 ` 1951` ``` proof (rule ccontr) ``` lp15@64122 ` 1952` ``` assume nonsub: "\ C \ f ` ball a r" ``` lp15@64122 ` 1953` ``` have "- f ` cball a r \ C" ``` lp15@64122 ` 1954` ``` proof (rule components_maximal [OF C]) ``` lp15@64122 ` 1955` ``` have "f ` cball a r homeomorphic cball a r" ``` lp15@64122 ` 1956` ``` using compact_cball contf homeomorphic_compact homeomorphic_sym inj by blast ``` lp15@64122 ` 1957` ``` then show "connected (- f ` cball a r)" ``` lp15@64122 ` 1958` ``` by (auto intro: connected_complement_homeomorphic_convex_compact 2) ``` lp15@64122 ` 1959` ``` show "- f ` cball a r \ - f ` sphere a r" ``` lp15@64122 ` 1960` ``` by auto ``` lp15@64122 ` 1961` ``` then show "C \ - f ` cball a r \ {}" ``` lp15@64122 ` 1962` ``` using \C \ {}\ in_components_subset [OF C] nonsub ``` lp15@64122 ` 1963` ``` using image_iff by fastforce ``` lp15@64122 ` 1964` ``` qed ``` lp15@64122 ` 1965` ``` then have "bounded (- f ` cball a r)" ``` lp15@64122 ` 1966` ``` using bounded_subset \bounded C\ by auto ``` lp15@64122 ` 1967` ``` then have "\ bounded (f ` cball a r)" ``` lp15@64122 ` 1968` ``` using cobounded_imp_unbounded by blast ``` lp15@64122 ` 1969` ``` then show "False" ``` lp15@64122 ` 1970` ``` using compact_continuous_image [OF contf] compact_cball compact_imp_bounded by blast ``` lp15@64122 ` 1971` ``` qed ``` lp15@64122 ` 1972` ``` with \C \ {}\ have "C \ f ` ball a r \ {}" ``` lp15@64122 ` 1973` ``` by (simp add: inf.absorb_iff1) ``` lp15@64122 ` 1974` ``` then show "f ` ball a r \ C" ``` lp15@64122 ` 1975` ``` by (metis components_maximal [OF C _ fimsub] connected_continuous_image ball_subset_cball connected_ball contf continuous_on_subset) ``` lp15@64122 ` 1976` ``` qed ``` lp15@64122 ` 1977` ``` moreover have "open (- f ` sphere a r)" ``` lp15@64122 ` 1978` ``` using hom compact_eq_bounded_closed compact_sphere homeomorphic_compactness by blast ``` lp15@64122 ` 1979` ``` ultimately show ?thesis ``` lp15@64122 ` 1980` ``` using open_components by blast ``` lp15@64122 ` 1981` ```qed ``` lp15@64122 ` 1982` lp15@64122 ` 1983` lp15@64122 ` 1984` ```text\Proved by L. E. J. Brouwer (1912)\ ``` ak2110@68833 ` 1985` ```theorem%important invariance_of_domain: ``` lp15@64122 ` 1986` ``` fixes f :: "'a \ 'a::euclidean_space" ``` lp15@64122 ` 1987` ``` assumes "continuous_on S f" "open S" "inj_on f S" ``` lp15@64122 ` 1988` ``` shows "open(f ` S)" ``` lp15@64122 ` 1989` ``` unfolding open_subopen [of "f`S"] ``` ak2110@68833 ` 1990` ```proof%unimportant clarify ``` lp15@64122 ` 1991` ``` fix a ``` lp15@64122 ` 1992` ``` assume "a \ S" ``` lp15@64122 ` 1993` ``` obtain \ where "\ > 0" and \: "cball a \ \ S" ``` lp15@64122 ` 1994` ``` using \open S\ \a \ S\ open_contains_cball_eq by blast ``` lp15@64122 ` 1995` ``` show "\T. open T \ f a \ T \ T \ f ` S" ``` lp15@64122 ` 1996` ``` proof (intro exI conjI) ``` lp15@64122 ` 1997` ``` show "open (f ` (ball a \))" ``` lp15@64122 ` 1998` ``` by (meson \ \0 < \\ assms continuous_on_subset inj_on_subset invariance_of_domain_ball) ``` lp15@64122 ` 1999` ``` show "f a \ f ` ball a \" ``` lp15@64122 ` 2000` ``` by (simp add: \0 < \\) ``` lp15@64122 ` 2001` ``` show "f ` ball a \ \ f ` S" ``` lp15@64122 ` 2002` ``` using \ ball_subset_cball by blast ``` lp15@64122 ` 2003` ``` qed ``` lp15@64122 ` 2004` ```qed ``` lp15@64122 ` 2005` ak2110@68833 ` 2006` ```lemma%unimportant inv_of_domain_ss0: ``` lp15@64122 ` 2007` ``` fixes f :: "'a \ 'a::euclidean_space" ``` lp15@64122 ` 2008` ``` assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U \ S" ``` lp15@64122 ` 2009` ``` and "subspace S" and dimS: "dim S = DIM('b::euclidean_space)" ``` lp15@64122 ` 2010` ``` and ope: "openin (subtopology euclidean S) U" ``` lp15@64122 ` 2011` ``` shows "openin (subtopology euclidean S) (f ` U)" ``` lp15@64122 ` 2012` ```proof - ``` lp15@64122 ` 2013` ``` have "U \ S" ``` lp15@64122 ` 2014` ``` using ope openin_imp_subset by blast ``` lp15@64122 ` 2015` ``` have "(UNIV::'b set) homeomorphic S" ``` immler@68072 ` 2016` ``` by (simp add: \subspace S\ dimS homeomorphic_subspaces) ``` lp15@64122 ` 2017` ``` then obtain h k where homhk: "homeomorphism (UNIV::'b set) S h k" ``` lp15@64122 ` 2018` ``` using homeomorphic_def by blast ``` lp15@64122 ` 2019` ``` have homkh: "homeomorphism S (k ` S) k h" ``` lp15@64122 ` 2020` ``` using homhk homeomorphism_image2 homeomorphism_sym by fastforce ``` lp15@64122 ` 2021` ``` have "open ((k \ f \ h) ` k ` U)" ``` lp15@64122 ` 2022` ``` proof (rule invariance_of_domain) ``` lp15@64122 ` 2023` ``` show "continuous_on (k ` U) (k \ f \ h)" ``` lp15@64122 ` 2024` ``` proof (intro continuous_intros) ``` lp15@64122 ` 2025` ``` show "continuous_on (k ` U) h" ``` lp15@64122 ` 2026` ``` by (meson continuous_on_subset [OF homeomorphism_cont1 [OF homhk]] top_greatest) ``` lp15@64122 ` 2027` ``` show "continuous_on (h ` k ` U) f" ``` lp15@64122 ` 2028` ``` apply (rule continuous_on_subset [OF contf], clarify) ``` lp15@64122 ` 2029` ``` apply (metis homhk homeomorphism_def ope openin_imp_subset rev_subsetD) ``` lp15@64122 ` 2030` ``` done ``` lp15@64122 ` 2031` ``` show "continuous_on (f ` h ` k ` U) k" ``` lp15@64122 ` 2032` ``` apply (rule continuous_on_subset [OF homeomorphism_cont2 [OF homhk]]) ``` lp15@64122 ` 2033` ``` using fim homhk homeomorphism_apply2 ope openin_subset by fastforce ``` lp15@64122 ` 2034` ``` qed ``` lp15@64122 ` 2035` ``` have ope_iff: "\T. open T \ openin (subtopology euclidean (k ` S)) T" ``` lp15@64122 ` 2036` ``` using homhk homeomorphism_image2 open_openin by fastforce ``` lp15@64122 ` 2037` ``` show "open (k ` U)" ``` lp15@64122 ` 2038` ``` by (simp add: ope_iff homeomorphism_imp_open_map [OF homkh ope]) ``` lp15@64122 ` 2039` ``` show "inj_on (k \ f \ h) (k ` U)" ``` lp15@64122 ` 2040` ``` apply (clarsimp simp: inj_on_def) ``` lp15@64122 ` 2041` ``` by (metis subsetD fim homeomorphism_apply2 [OF homhk] image_subset_iff inj_on_eq_iff injf \U \ S\) ``` lp15@64122 ` 2042` ``` qed ``` lp15@64122 ` 2043` ``` moreover ``` lp15@64122 ` 2044` ``` have eq: "f ` U = h ` (k \ f \ h \ k) ` U" ``` lp15@64122 ` 2045` ``` apply (auto simp: image_comp [symmetric]) ``` lp15@64122 ` 2046` ``` apply (metis homkh \U \ S\ fim homeomorphism_image2 homeomorphism_of_subsets homhk imageI subset_UNIV) ``` lp15@64122 ` 2047` ``` by (metis \U \ S\ subsetD fim homeomorphism_def homhk image_eqI) ``` lp15@64122 ` 2048` ``` ultimately show ?thesis ``` lp15@64122 ` 2049` ``` by (metis (no_types, hide_lams) homeomorphism_imp_open_map homhk image_comp open_openin subtopology_UNIV) ``` lp15@64122 ` 2050` ```qed ``` lp15@64122 ` 2051` ak2110@68833 ` 2052` ```lemma%unimportant inv_of_domain_ss1: ``` lp15@64122 ` 2053` ``` fixes f :: "'a \ 'a::euclidean_space" ``` lp15@64122 ` 2054` ``` assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U \ S" ``` lp15@64122 ` 2055` ``` and "subspace S" ``` lp15@64122 ` 2056` ``` and ope: "openin (subtopology euclidean S) U" ``` lp15@64122 ` 2057` ``` shows "openin (subtopology euclidean S) (f ` U)" ``` lp15@64122 ` 2058` ```proof - ``` lp15@64122 ` 2059` ``` define S' where "S' \ {y. \x \ S. orthogonal x y}" ``` lp15@64122 ` 2060` ``` have "subspace S'" ``` lp15@64122 ` 2061` ``` by (simp add: S'_def subspace_orthogonal_to_vectors) ``` lp15@64122 ` 2062` ``` define g where "g \ \z::'a*'a. ((f \ fst)z, snd z)" ``` lp15@64122 ` 2063` ``` have "openin (subtopology euclidean (S \ S')) (g ` (U \ S'))" ``` lp15@64122 ` 2064` ``` proof (rule inv_of_domain_ss0) ``` lp15@64122 ` 2065` ``` show "continuous_on (U \ S') g" ``` lp15@64122 ` 2066` ``` apply (simp add: g_def) ``` lp15@64122 ` 2067` ``` apply (intro continuous_intros continuous_on_compose2 [OF contf continuous_on_fst], auto) ``` lp15@64122 ` 2068` ``` done ``` lp15@64122 ` 2069` ``` show "g ` (U \ S') \ S \ S'" ``` lp15@64122 ` 2070` ``` using fim by (auto simp: g_def) ``` lp15@64122 ` 2071` ``` show "inj_on g (U \ S')" ``` lp15@64122 ` 2072` ``` using injf by (auto simp: g_def inj_on_def) ``` lp15@64122 ` 2073` ``` show "subspace (S \ S')" ``` lp15@64122 ` 2074` ``` by (simp add: \subspace S'\ \subspace S\ subspace_Times) ``` lp15@64122 ` 2075` ``` show "openin (subtopology euclidean (S \ S')) (U \ S')" ``` lp15@64122 ` 2076` ``` by (simp add: openin_Times [OF ope]) ``` lp15@64122 ` 2077` ``` have "dim (S \ S') = dim S + dim S'" ``` lp15@64122 ` 2078` ``` by (simp add: \subspace S'\ \subspace S\ dim_Times) ``` lp15@64122 ` 2079` ``` also have "... = DIM('a)" ``` lp15@64122 ` 2080` ``` using dim_subspace_orthogonal_to_vectors [OF \subspace S\ subspace_UNIV] ``` lp15@64122 ` 2081` ``` by (simp add: add.commute S'_def) ``` lp15@64122 ` 2082` ``` finally show "dim (S \ S') = DIM('a)" . ``` lp15@64122 ` 2083` ``` qed ``` lp15@64122 ` 2084` ``` moreover have "g ` (U \ S') = f ` U \ S'" ``` lp15@64122 ` 2085` ``` by (auto simp: g_def image_iff) ``` lp15@64122 ` 2086` ``` moreover have "0 \ S'" ``` lp15@64122 ` 2087` ``` using \subspace S'\ subspace_affine by blast ``` lp15@64122 ` 2088` ``` ultimately show ?thesis ``` lp15@64122 ` 2089` ``` by (auto simp: openin_Times_eq) ``` lp15@64122 ` 2090` ```qed ``` lp15@64122 ` 2091` lp15@64122 ` 2092` ak2110@68833 ` 2093` ```corollary%important invariance_of_domain_subspaces: ``` lp15@64122 ` 2094` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@64122 ` 2095` ``` assumes ope: "openin (subtopology euclidean U) S" ``` lp15@64122 ` 2096` ``` and "subspace U" "subspace V" and VU: "dim V \ dim U" ``` lp15@64122 ` 2097` ``` and contf: "continuous_on S f" and fim: "f ` S \ V" ``` lp15@64122 ` 2098` ``` and injf: "inj_on f S" ``` lp15@64122 ` 2099` ``` shows "openin (subtopology euclidean V) (f ` S)" ``` ak2110@68833 ` 2100` ```proof%unimportant - ``` lp15@64122 ` 2101` ``` obtain V' where "subspace V'" "V' \ U" "dim V' = dim V" ``` lp15@64122 ` 2102` ``` using choose_subspace_of_subspace [OF VU] ``` immler@68072 ` 2103` ``` by (metis span_eq_iff \subspace U\) ``` lp15@64122 ` 2104` ``` then have "V homeomorphic V'" ``` lp15@64122 ` 2105` ``` by (simp add: \subspace V\ homeomorphic_subspaces) ``` lp15@64122 ` 2106` ``` then obtain h k where homhk: "homeomorphism V V' h k" ``` lp15@64122 ` 2107` ``` using homeomorphic_def by blast ``` lp15@64122 ` 2108` ``` have eq: "f ` S = k ` (h \ f) ` S" ``` lp15@64122 ` 2109` ``` proof - ``` lp15@64122 ` 2110` ``` have "k ` h ` f ` S = f ` S" ``` lp15@64122 ` 2111` ``` by (meson fim homeomorphism_def homeomorphism_of_subsets homhk subset_refl) ``` lp15@64122 ` 2112` ``` then show ?thesis ``` lp15@64122 ` 2113` ``` by (simp add: image_comp) ``` lp15@64122 ` 2114` ``` qed ``` lp15@64122 ` 2115` ``` show ?thesis ``` lp15@64122 ` 2116` ``` unfolding eq ``` lp15@64122 ` 2117` ``` proof (rule homeomorphism_imp_open_map) ``` lp15@64122 ` 2118` ``` show homkh: "homeomorphism V' V k h" ``` lp15@64122 ` 2119` ``` by (simp add: homeomorphism_symD homhk) ``` lp15@64122 ` 2120` ``` have hfV': "(h \ f) ` S \ V'" ``` lp15@64122 ` 2121` ``` using fim homeomorphism_image1 homhk by fastforce ``` lp15@64122 ` 2122` ``` moreover have "openin (subtopology euclidean U) ((h \ f) ` S)" ``` lp15@64122 ` 2123` ``` proof (rule inv_of_domain_ss1) ``` lp15@64122 ` 2124` ``` show "continuous_on S (h \ f)" ``` lp15@64122 ` 2125` ``` by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_cont1 homhk) ``` lp15@64122 ` 2126` ``` show "inj_on (h \ f) S" ``` lp15@64122 ` 2127` ``` apply (clarsimp simp: inj_on_def) ``` lp15@64122 ` 2128` ``` by (metis fim homeomorphism_apply2 [OF homkh] image_subset_iff inj_onD injf) ``` lp15@64122 ` 2129` ``` show "(h \ f) ` S \ U" ``` lp15@64122 ` 2130` ``` using \V' \ U\ hfV' by auto ``` lp15@64122 ` 2131` ``` qed (auto simp: assms) ``` lp15@64122 ` 2132` ``` ultimately show "openin (subtopology euclidean V') ((h \ f) ` S)" ``` lp15@64122 ` 2133` ``` using openin_subset_trans \V' \ U\ by force ``` lp15@64122 ` 2134` ``` qed ``` lp15@64122 ` 2135` ```qed ``` lp15@64122 ` 2136` ak2110@68833 ` 2137` ```corollary%important invariance_of_dimension_subspaces: ``` lp15@64122 ` 2138` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@64122 ` 2139` ``` assumes ope: "openin (subtopology euclidean U) S" ``` lp15@64122 ` 2140` ``` and "subspace U" "subspace V" ``` lp15@64122 ` 2141` ``` and contf: "continuous_on S f" and fim: "f ` S \ V" ``` lp15@64122 ` 2142` ``` and injf: "inj_on f S" and "S \ {}" ``` lp15@64122 ` 2143` ``` shows "dim U \ dim V" ``` ak2110@68833 ` 2144` ```proof%unimportant - ``` lp15@64122 ` 2145` ``` have "False" if "dim V < dim U" ``` lp15@64122 ` 2146` ``` proof - ``` lp15@64122 ` 2147` ``` obtain T where "subspace T" "T \ U" "dim T = dim V" ``` lp15@64122 ` 2148` ``` using choose_subspace_of_subspace [of "dim V" U] ``` immler@68072 ` 2149` ``` by (metis \dim V < dim U\ assms(2) order.strict_implies_order span_eq_iff) ``` lp15@64122 ` 2150` ``` then have "V homeomorphic T" ``` lp15@64122 ` 2151` ``` by (simp add: \subspace V\ homeomorphic_subspaces) ``` lp15@64122 ` 2152` ``` then obtain h k where homhk: "homeomorphism V T h k" ``` lp15@64122 ` 2153` ``` using homeomorphic_def by blast ``` lp15@64122 ` 2154` ``` have "continuous_on S (h \ f)" ``` lp15@64122 ` 2155` ``` by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_cont1 homhk) ``` lp15@64122 ` 2156` ``` moreover have "(h \ f) ` S \ U" ``` lp15@64122 ` 2157` ``` using \T \ U\ fim homeomorphism_image1 homhk by fastforce ``` lp15@64122 ` 2158` ``` moreover have "inj_on (h \ f) S" ``` lp15@64122 ` 2159` ``` apply (clarsimp simp: inj_on_def) ``` lp15@64122 ` 2160` ``` by (metis fim homeomorphism_apply1 homhk image_subset_iff inj_onD injf) ``` lp15@64122 ` 2161` ``` ultimately have ope_hf: "openin (subtopology euclidean U) ((h \ f) ` S)" ``` lp15@64122 ` 2162` ``` using invariance_of_domain_subspaces [OF ope \subspace U\ \subspace U\] by auto ``` lp15@64122 ` 2163` ``` have "(h \ f) ` S \ T" ``` lp15@64122 ` 2164` ``` using fim homeomorphism_image1 homhk by fastforce ``` lp15@64122 ` 2165` ``` then show ?thesis ``` lp15@64122 ` 2166` ``` by (metis dim_openin \dim T = dim V\ ope_hf \subspace U\ \S \ {}\ dim_subset image_is_empty not_le that) ``` lp15@64122 ` 2167` ``` qed ``` lp15@64122 ` 2168` ``` then show ?thesis ``` lp15@64122 ` 2169` ``` using not_less by blast ``` lp15@64122 ` 2170` ```qed ``` lp15@64122 ` 2171` ak2110@68833 ` 2172` ```corollary%important invariance_of_domain_affine_sets: ``` lp15@64122 ` 2173` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@64122 ` 2174` ``` assumes ope: "openin (subtopology euclidean U) S" ``` lp15@64122 ` 2175` ``` and aff: "affine U" "affine V" "aff_dim V \ aff_dim U" ``` lp15@64122 ` 2176` ``` and contf: "continuous_on S f" and fim: "f ` S \ V" ``` lp15@64122 ` 2177` ``` and injf: "inj_on f S" ``` lp15@64122 ` 2178` ``` shows "openin (subtopology euclidean V) (f ` S)" ``` ak2110@68833 ` 2179` ```proof%unimportant (cases "S = {}") ``` lp15@64122 ` 2180` ``` case True ``` lp15@64122 ` 2181` ``` then show ?thesis by auto ``` lp15@64122 ` 2182` ```next ``` lp15@64122 ` 2183` ``` case False ``` lp15@64122 ` 2184` ``` obtain a b where "a \ S" "a \ U" "b \ V" ``` lp15@64122 ` 2185` ``` using False fim ope openin_contains_cball by fastforce ``` nipkow@67399 ` 2186` ``` have "openin (subtopology euclidean ((+) (- b) ` V)) (((+) (- b) \ f \ (+) a) ` (+) (- a) ` S)" ``` lp15@64122 ` 2187` ``` proof (rule invariance_of_domain_subspaces) ``` nipkow@67399 ` 2188` ``` show "openin (subtopology euclidean ((+) (- a) ` U)) ((+) (- a) ` S)" ``` lp15@64122 ` 2189` ``` by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois) ``` nipkow@67399 ` 2190` ``` show "subspace ((+) (- a) ` U)" ``` lp15@64122 ` 2191` ``` by (simp add: \a \ U\ affine_diffs_subspace \affine U\) ``` nipkow@67399 ` 2192` ``` show "subspace ((+) (- b) ` V)" ``` lp15@64122 ` 2193` ``` by (simp add: \b \ V\ affine_diffs_subspace \affine V\) ``` nipkow@67399 ` 2194` ``` show "dim ((+) (- b) ` V) \ dim ((+) (- a) ` U)" ``` lp15@64122 ` 2195` ``` by (metis \a \ U\ \b \ V\ aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff) ``` nipkow@67399 ` 2196` ``` show "continuous_on ((+) (- a) ` S) ((+) (- b) \ f \ (+) a)" ``` lp15@64122 ` 2197` ``` by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois) ``` nipkow@67399 ` 2198` ``` show "((+) (- b) \ f \ (+) a) ` (+) (- a) ` S \ (+) (- b) ` V" ``` lp15@64122 ` 2199` ``` using fim by auto ``` nipkow@67399 ` 2200` ``` show "inj_on ((+) (- b) \ f \ (+) a) ((+) (- a) ` S)" ``` lp15@64122 ` 2201` ``` by (auto simp: inj_on_def) (meson inj_onD injf) ``` lp15@64122 ` 2202` ``` qed ``` lp15@64122 ` 2203` ``` then show ?thesis ``` lp15@64122 ` 2204` ``` by (metis (no_types, lifting) homeomorphism_imp_open_map homeomorphism_translation image_comp translation_galois) ``` lp15@64122 ` 2205` ```qed ``` lp15@64122 ` 2206` ak2110@68833 ` 2207` ```corollary%important invariance_of_dimension_affine_sets: ``` lp15@64122 ` 2208` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@64122 ` 2209` ``` assumes ope: "openin (subtopology euclidean U) S" ``` lp15@64122 ` 2210` ``` and aff: "affine U" "affine V" ``` lp15@64122 ` 2211` ``` and contf: "continuous_on S f" and fim: "f ` S \ V" ``` lp15@64122 ` 2212` ``` and injf: "inj_on f S" and "S \ {}" ``` lp15@64122 ` 2213` ``` shows "aff_dim U \ aff_dim V" ``` ak2110@68833 ` 2214` ```proof%unimportant - ``` lp15@64122 ` 2215` ``` obtain a b where "a \ S" "a \ U" "b \ V" ``` lp15@64122 ` 2216` ``` using \S \ {}\ fim ope openin_contains_cball by fastforce ``` nipkow@67399 ` 2217` ``` have "dim ((+) (- a) ` U) \ dim ((+) (- b) ` V)" ``` lp15@64122 ` 2218` ``` proof (rule invariance_of_dimension_subspaces) ``` nipkow@67399 ` 2219` ``` show "openin (subtopology euclidean ((+) (- a) ` U)) ((+) (- a) ` S)" ``` lp15@64122 ` 2220` ``` by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois) ``` nipkow@67399 ` 2221` ``` show "subspace ((+) (- a) ` U)" ``` lp15@64122 ` 2222` ``` by (simp add: \a \ U\ affine_diffs_subspace \affine U\) ``` nipkow@67399 ` 2223` ``` show "subspace ((+) (- b) ` V)" ``` lp15@64122 ` 2224` ``` by (simp add: \b \ V\ affine_diffs_subspace \affine V\) ``` nipkow@67399 ` 2225` ``` show "continuous_on ((+) (- a) ` S) ((+) (- b) \ f \ (+) a)" ``` lp15@64122 ` 2226` ``` by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois) ``` nipkow@67399 ` 2227` ``` show "((+) (- b) \ f \ (+) a) ` (+) (- a) ` S \ (+) (- b) ` V" ``` lp15@64122 ` 2228` ``` using fim by auto ``` nipkow@67399 ` 2229` ``` show "inj_on ((+) (- b) \ f \ (+) a) ((+) (- a) ` S)" ``` lp15@64122 ` 2230` ``` by (auto simp: inj_on_def) (meson inj_onD injf) ``` lp15@64122 ` 2231` ``` qed (use \S \ {}\ in auto) ``` lp15@64122 ` 2232` ``` then show ?thesis ``` lp15@64122 ` 2233` ``` by (metis \a \ U\ \b \ V\ aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff) ``` lp15@64122 ` 2234` ```qed ``` lp15@64122 ` 2235` ak2110@68833 ` 2236` ```corollary%important invariance_of_dimension: ``` lp15@64122 ` 2237` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@64122 ` 2238` ``` assumes contf: "continuous_on S f" and "open S" ``` lp15@64122 ` 2239` ``` and injf: "inj_on f S" and "S \ {}" ``` lp15@64122 ` 2240` ``` shows "DIM('a) \ DIM('b)" ``` ak2110@68833 ` 2241` ``` using%unimportant invariance_of_dimension_subspaces [of UNIV S UNIV f] assms ``` lp15@64122 ` 2242` ``` by auto ``` lp15@64122 ` 2243` lp15@64122 ` 2244` ak2110@68833 ` 2245` ```corollary%important continuous_injective_image_subspace_dim_le: ``` lp15@64122 ` 2246` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@64122 ` 2247` ``` assumes "subspace S" "subspace T" ``` lp15@64122 ` 2248` ``` and contf: "continuous_on S f" and fim: "f ` S \ T" ``` lp15@64122 ` 2249` ``` and injf: "inj_on f S" ``` lp15@64122 ` 2250` ``` shows "dim S \ dim T" ``` lp15@64122 ` 2251` ``` apply (rule invariance_of_dimension_subspaces [of S S _ f]) ``` ak2110@68833 ` 2252` ``` using%unimportant assms by (auto simp: subspace_affine) ``` ak2110@68833 ` 2253` ak2110@68833 ` 2254` ```lemma%unimportant invariance_of_dimension_convex_domain: ``` lp15@64122 ` 2255` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@64122 ` 2256` ``` assumes "convex S" ``` lp15@64122 ` 2257` ``` and contf: "continuous_on S f" and fim: "f ` S \ affine hull T" ``` lp15@64122 ` 2258` ``` and injf: "inj_on f S" ``` lp15@64122 ` 2259` ``` shows "aff_dim S \ aff_dim T" ``` lp15@64122 ` 2260` ```proof (cases "S = {}") ``` lp15@64122 ` 2261` ``` case True ``` lp15@64122 ` 2262` ``` then show ?thesis by (simp add: aff_dim_geq) ``` lp15@64122 ` 2263` ```next ``` lp15@64122 ` 2264` ``` case False ``` lp15@64122 ` 2265` ``` have "aff_dim (affine hull S) \ aff_dim (affine hull T)" ``` lp15@64122 ` 2266` ``` proof (rule invariance_of_dimension_affine_sets) ``` lp15@64122 ` 2267` ``` show "openin (subtopology euclidean (affine hull S)) (rel_interior S)" ``` lp15@64122 ` 2268` ``` by (simp add: openin_rel_interior) ``` lp15@64122 ` 2269` ``` show "continuous_on (rel_interior S) f" ``` lp15@64122 ` 2270` ``` using contf continuous_on_subset rel_interior_subset by blast ``` lp15@64122 ` 2271` ``` show "f ` rel_interior S \ affine hull T" ``` lp15@64122 ` 2272` ``` using fim rel_interior_subset by blast ``` lp15@64122 ` 2273` ``` show "inj_on f (rel_interior S)" ``` lp15@64122 ` 2274` ``` using inj_on_subset injf rel_interior_subset by blast ``` lp15@64122 ` 2275` ``` show "rel_interior S \ {}" ``` lp15@64122 ` 2276` ``` by (simp add: False \convex S\ rel_interior_eq_empty) ``` lp15@64122 ` 2277` ``` qed auto ``` lp15@64122 ` 2278` ``` then show ?thesis ``` lp15@64122 ` 2279` ``` by simp ``` lp15@64122 ` 2280` ```qed ``` lp15@64122 ` 2281` lp15@64122 ` 2282` ak2110@68833 ` 2283` ```lemma%unimportant homeomorphic_convex_sets_le: ``` lp15@64122 ` 2284` ``` assumes "convex S" "S homeomorphic T" ``` lp15@64122 ` 2285` ``` shows "aff_dim S \ aff_dim T" ``` lp15@64122 ` 2286` ```proof - ``` lp15@64122 ` 2287` ``` obtain h k where homhk: "homeomorphism S T h k" ``` lp15@64122 ` 2288` ``` using homeomorphic_def assms by blast ``` lp15@64122 ` 2289` ``` show ?thesis ``` lp15@64122 ` 2290` ``` proof (rule invariance_of_dimension_convex_domain [OF \convex S\]) ``` lp15@64122 ` 2291` ``` show "continuous_on S h" ``` lp15@64122 ` 2292` ``` using homeomorphism_def homhk by blast ``` lp15@64122 ` 2293` ``` show "h ` S \ affine hull T" ``` lp15@64122 ` 2294` ``` by (metis homeomorphism_def homhk hull_subset) ``` lp15@64122 ` 2295` ``` show "inj_on h S" ``` lp15@64122 ` 2296` ``` by (meson homeomorphism_apply1 homhk inj_on_inverseI) ``` lp15@64122 ` 2297` ``` qed ``` lp15@64122 ` 2298` ```qed ``` lp15@64122 ` 2299` ak2110@68833 ` 2300` ```lemma%unimportant homeomorphic_convex_sets: ``` lp15@64122 ` 2301` ``` assumes "convex S" "convex T" "S homeomorphic T" ``` lp15@64122 ` 2302` ``` shows "aff_dim S = aff_dim T" ``` lp15@64122 ` 2303` ``` by (meson assms dual_order.antisym homeomorphic_convex_sets_le homeomorphic_sym) ``` lp15@64122 ` 2304` ak2110@68833 ` 2305` ```lemma%unimportant homeomorphic_convex_compact_sets_eq: ``` lp15@64122 ` 2306` ``` assumes "convex S" "compact S" "convex T" "compact T" ``` lp15@64122 ` 2307` ``` shows "S homeomorphic T \ aff_dim S = aff_dim T" ``` lp15@64122 ` 2308` ``` by (meson assms homeomorphic_convex_compact_sets homeomorphic_convex_sets) ``` lp15@64122 ` 2309` ak2110@68833 ` 2310` ```lemma%unimportant invariance_of_domain_gen: ``` lp15@64122 ` 2311` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@64122 ` 2312` ``` assumes "open S" "continuous_on S f" "inj_on f S" "DIM('b) \ DIM('a)" ``` lp15@64122 ` 2313` ``` shows "open(f ` S)" ``` lp15@64122 ` 2314` ``` using invariance_of_domain_subspaces [of UNIV S UNIV f] assms by auto ``` lp15@64122 ` 2315` ak2110@68833 ` 2316` ```lemma%unimportant injective_into_1d_imp_open_map_UNIV: ``` lp15@64122 ` 2317` ``` fixes f :: "'a::euclidean_space \ real" ``` lp15@64122 ` 2318` ``` assumes "open T" "continuous_on S f" "inj_on f S" "T \ S" ``` lp15@64122 ` 2319` ``` shows "open (f ` T)" ``` lp15@64122 ` 2320` ``` apply (rule invariance_of_domain_gen [OF \open T\]) ``` lp15@64122 ` 2321` ``` using assms apply (auto simp: elim: continuous_on_subset subset_inj_on) ``` lp15@64122 ` 2322` ``` done ``` lp15@64122 ` 2323` ak2110@68833 ` 2324` ```lemma%unimportant continuous_on_inverse_open: ``` lp15@64122 ` 2325` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@64122 ` 2326` ``` assumes "open S" "continuous_on S f" "DIM('b) \ DIM('a)" and gf: "\x. x \ S \ g(f x) = x" ``` lp15@64122 ` 2327` ``` shows "continuous_on (f ` S) g" ``` lp15@64122 ` 2328` ```proof (clarsimp simp add: continuous_openin_preimage_eq) ``` lp15@64122 ` 2329` ``` fix T :: "'a set" ``` lp15@64122 ` 2330` ``` assume "open T" ``` lp15@66884 ` 2331` ``` have eq: "f ` S \ g -` T = f ` (S \ T)" ``` lp15@64122 ` 2332` ``` by (auto simp: gf) ``` lp15@66884 ` 2333` ``` show "openin (subtopology euclidean (f ` S)) (f ` S \ g -` T)" ``` lp15@64122 ` 2334` ``` apply (subst eq) ``` lp15@64122 ` 2335` ``` apply (rule open_openin_trans) ``` lp15@64122 ` 2336` ``` apply (rule invariance_of_domain_gen) ``` lp15@64122 ` 2337` ``` using assms ``` lp15@64122 ` 2338` ``` apply auto ``` lp15@64122 ` 2339` ``` using inj_on_inverseI apply auto[1] ``` lp15@64122 ` 2340` ``` by (metis \open T\ continuous_on_subset inj_onI inj_on_subset invariance_of_domain_gen openin_open openin_open_eq) ``` lp15@64122 ` 2341` ```qed ``` lp15@64122 ` 2342` ak2110@68833 ` 2343` ```lemma%unimportant invariance_of_domain_homeomorphism: ``` lp15@64122 ` 2344` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@64122 ` 2345` ``` assumes "open S" "continuous_on S f" "DIM('b) \ DIM('a)" "inj_on f S" ``` lp15@64122 ` 2346` ``` obtains g where "homeomorphism S (f ` S) f g" ``` lp15@64122 ` 2347` ```proof ``` lp15@64122 ` 2348` ``` show "homeomorphism S (f ` S) f (inv_into S f)" ``` lp15@64122 ` 2349` ``` by (simp add: assms continuous_on_inverse_open homeomorphism_def) ``` lp15@64122 ` 2350` ```qed ``` lp15@64122 ` 2351` ak2110@68833 ` 2352` ```corollary%important invariance_of_domain_homeomorphic: ``` lp15@64122 ` 2353` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@64122 ` 2354` ``` assumes "open S" "continuous_on S f" "DIM('b) \ DIM('a)" "inj_on f S" ```