imports Weierstrass_Theorems Polytope Complex_Transcendental

section ‹Extending Continous Maps, Invariance of Domain, etc› text‹Ported from HOL Light (moretop.ml) by L C Paulson› theory Further_Topology imports Equivalence_Lebesgue_Henstock_Integration Weierstrass_Theorems Polytope Complex_Transcendental begin subsection‹A map from a sphere to a higher dimensional sphere is nullhomotopic› lemma spheremap_lemma1: fixes f :: "'a::euclidean_space ⇒ 'a::euclidean_space" assumes "subspace S" "subspace T" and dimST: "dim S < dim T" and "S ⊆ T" and diff_f: "f differentiable_on sphere 0 1 ∩ S" shows "f ` (sphere 0 1 ∩ S) ≠ sphere 0 1 ∩ T" proof assume fim: "f ` (sphere 0 1 ∩ S) = sphere 0 1 ∩ T" have inS: "⋀x. ⟦x ∈ S; x ≠ 0⟧ ⟹ (x /⇩_{R}norm x) ∈ S" using subspace_mul ‹subspace S› by blast have subS01: "(λx. x /⇩_{R}norm x) ` (S - {0}) ⊆ sphere 0 1 ∩ S" using ‹subspace S› subspace_mul by fastforce then have diff_f': "f differentiable_on (λx. x /⇩_{R}norm x) ` (S - {0})" by (rule differentiable_on_subset [OF diff_f]) define g where "g ≡ λx. norm x *⇩_{R}f(inverse(norm x) *⇩_{R}x)" have gdiff: "g differentiable_on S - {0}" unfolding g_def by (rule diff_f' derivative_intros differentiable_on_compose [where f=f] | force)+ have geq: "g ` (S - {0}) = T - {0}" proof have "g ` (S - {0}) ⊆ T" apply (auto simp: g_def subspace_mul [OF ‹subspace T›]) apply (metis (mono_tags, lifting) DiffI subS01 subspace_mul [OF ‹subspace T›] fim image_subset_iff inf_le2 singletonD) done moreover have "g ` (S - {0}) ⊆ UNIV - {0}" proof (clarsimp simp: g_def) fix y assume "y ∈ S" and f0: "f (y /⇩_{R}norm y) = 0" then have "y ≠ 0 ⟹ y /⇩_{R}norm y ∈ sphere 0 1 ∩ S" by (auto simp: subspace_mul [OF ‹subspace S›]) then show "y = 0" by (metis fim f0 Int_iff image_iff mem_sphere_0 norm_eq_zero zero_neq_one) qed ultimately show "g ` (S - {0}) ⊆ T - {0}" by auto next have *: "sphere 0 1 ∩ T ⊆ f ` (sphere 0 1 ∩ S)" using fim by (simp add: image_subset_iff) have "x ∈ (λx. norm x *⇩_{R}f (x /⇩_{R}norm x)) ` (S - {0})" if "x ∈ T" "x ≠ 0" for x proof - have "x /⇩_{R}norm x ∈ T" using ‹subspace T› subspace_mul that by blast then show ?thesis using * [THEN subsetD, of "x /⇩_{R}norm x"] that apply clarsimp apply (rule_tac x="norm x *⇩_{R}xa" in image_eqI, simp) apply (metis norm_eq_zero right_inverse scaleR_one scaleR_scaleR) using ‹subspace S› subspace_mul apply force done qed then have "T - {0} ⊆ (λx. norm x *⇩_{R}f (x /⇩_{R}norm x)) ` (S - {0})" by force then show "T - {0} ⊆ g ` (S - {0})" by (simp add: g_def) qed define T' where "T' ≡ {y. ∀x ∈ T. orthogonal x y}" have "subspace T'" by (simp add: subspace_orthogonal_to_vectors T'_def) have dim_eq: "dim T' + dim T = DIM('a)" using dim_subspace_orthogonal_to_vectors [of T UNIV] ‹subspace T› by (simp add: T'_def) have "∃v1 v2. v1 ∈ span T ∧ (∀w ∈ span T. orthogonal v2 w) ∧ x = v1 + v2" for x by (force intro: orthogonal_subspace_decomp_exists [of T x]) then obtain p1 p2 where p1span: "p1 x ∈ span T" and "⋀w. w ∈ span T ⟹ orthogonal (p2 x) w" and eq: "p1 x + p2 x = x" for x by metis then have p1: "⋀z. p1 z ∈ T" and ortho: "⋀w. w ∈ T ⟹ orthogonal (p2 x) w" for x using span_eq_iff ‹subspace T› by blast+ then have p2: "⋀z. p2 z ∈ T'" by (simp add: T'_def orthogonal_commute) have p12_eq: "⋀x y. ⟦x ∈ T; y ∈ T'⟧ ⟹ p1(x + y) = x ∧ p2(x + y) = y" proof (rule orthogonal_subspace_decomp_unique [OF eq p1span, where T=T']) show "⋀x y. ⟦x ∈ T; y ∈ T'⟧ ⟹ p2 (x + y) ∈ span T'" using span_eq_iff p2 ‹subspace T'› by blast show "⋀a b. ⟦a ∈ T; b ∈ T'⟧ ⟹ orthogonal a b" using T'_def by blast qed (auto simp: span_base) then have "⋀c x. p1 (c *⇩_{R}x) = c *⇩_{R}p1 x ∧ p2 (c *⇩_{R}x) = c *⇩_{R}p2 x" proof - fix c :: real and x :: 'a have f1: "c *⇩_{R}x = c *⇩_{R}p1 x + c *⇩_{R}p2 x" by (metis eq pth_6) have f2: "c *⇩_{R}p2 x ∈ T'" by (simp add: ‹subspace T'› p2 subspace_scale) have "c *⇩_{R}p1 x ∈ T" by (metis (full_types) assms(2) p1span span_eq_iff subspace_scale) then show "p1 (c *⇩_{R}x) = c *⇩_{R}p1 x ∧ p2 (c *⇩_{R}x) = c *⇩_{R}p2 x" using f2 f1 p12_eq by presburger qed moreover have lin_add: "⋀x y. p1 (x + y) = p1 x + p1 y ∧ p2 (x + y) = p2 x + p2 y" proof (rule orthogonal_subspace_decomp_unique [OF _ p1span, where T=T']) show "⋀x y. p1 (x + y) + p2 (x + y) = p1 x + p1 y + (p2 x + p2 y)" by (simp add: add.assoc add.left_commute eq) show "⋀a b. ⟦a ∈ T; b ∈ T'⟧ ⟹ orthogonal a b" using T'_def by blast qed (auto simp: p1span p2 span_base span_add) ultimately have "linear p1" "linear p2" by unfold_locales auto have "(λz. g (p1 z)) differentiable_on {x + y |x y. x ∈ S - {0} ∧ y ∈ T'}" apply (rule differentiable_on_compose [where f=g]) apply (rule linear_imp_differentiable_on [OF ‹linear p1›]) apply (rule differentiable_on_subset [OF gdiff]) using p12_eq ‹S ⊆ T› apply auto done then have diff: "(λx. g (p1 x) + p2 x) differentiable_on {x + y |x y. x ∈ S - {0} ∧ y ∈ T'}" by (intro derivative_intros linear_imp_differentiable_on [OF ‹linear p2›]) have "dim {x + y |x y. x ∈ S - {0} ∧ y ∈ T'} ≤ dim {x + y |x y. x ∈ S ∧ y ∈ T'}" by (blast intro: dim_subset) also have "... = dim S + dim T' - dim (S ∩ T')" using dim_sums_Int [OF ‹subspace S› ‹subspace T'›] by (simp add: algebra_simps) also have "... < DIM('a)" using dimST dim_eq by auto finally have neg: "negligible {x + y |x y. x ∈ S - {0} ∧ y ∈ T'}" by (rule negligible_lowdim) have "negligible ((λx. g (p1 x) + p2 x) ` {x + y |x y. x ∈ S - {0} ∧ y ∈ T'})" by (rule negligible_differentiable_image_negligible [OF order_refl neg diff]) then have "negligible {x + y |x y. x ∈ g ` (S - {0}) ∧ y ∈ T'}" proof (rule negligible_subset) have "⟦t' ∈ T'; s ∈ S; s ≠ 0⟧ ⟹ g s + t' ∈ (λx. g (p1 x) + p2 x) ` {x + t' |x t'. x ∈ S ∧ x ≠ 0 ∧ t' ∈ T'}" for t' s apply (rule_tac x="s + t'" in image_eqI) using ‹S ⊆ T› p12_eq by auto then show "{x + y |x y. x ∈ g ` (S - {0}) ∧ y ∈ T'} ⊆ (λx. g (p1 x) + p2 x) ` {x + y |x y. x ∈ S - {0} ∧ y ∈ T'}" by auto qed moreover have "- T' ⊆ {x + y |x y. x ∈ g ` (S - {0}) ∧ y ∈ T'}" proof clarsimp fix z assume "z ∉ T'" show "∃x y. z = x + y ∧ x ∈ g ` (S - {0}) ∧ y ∈ T'" apply (rule_tac x="p1 z" in exI) apply (rule_tac x="p2 z" in exI) apply (simp add: p1 eq p2 geq) by (metis ‹z ∉ T'› add.left_neutral eq p2) qed ultimately have "negligible (-T')" using negligible_subset by blast moreover have "negligible T'" using negligible_lowdim 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) ultimately have "negligible (-T' ∪ T')" by (metis negligible_Un_eq) then show False using negligible_Un_eq non_negligible_UNIV by simp qed lemma spheremap_lemma2: fixes f :: "'a::euclidean_space ⇒ 'a::euclidean_space" assumes ST: "subspace S" "subspace T" "dim S < dim T" and "S ⊆ T" and contf: "continuous_on (sphere 0 1 ∩ S) f" and fim: "f ` (sphere 0 1 ∩ S) ⊆ sphere 0 1 ∩ T" shows "∃c. homotopic_with (λx. True) (sphere 0 1 ∩ S) (sphere 0 1 ∩ T) f (λx. c)" proof - have [simp]: "⋀x. ⟦norm x = 1; x ∈ S⟧ ⟹ norm (f x) = 1" using fim by (simp add: image_subset_iff) have "compact (sphere 0 1 ∩ S)" by (simp add: ‹subspace S› closed_subspace compact_Int_closed) then obtain g where pfg: "polynomial_function g" and gim: "g ` (sphere 0 1 ∩ S) ⊆ T" and g12: "⋀x. x ∈ sphere 0 1 ∩ S ⟹ norm(f x - g x) < 1/2" apply (rule Stone_Weierstrass_polynomial_function_subspace [OF _ contf _ ‹subspace T›, of "1/2"]) using fim apply auto done have gnz: "g x ≠ 0" if "x ∈ sphere 0 1 ∩ S" for x proof - have "norm (f x) = 1" using fim that by (simp add: image_subset_iff) then show ?thesis using g12 [OF that] by auto qed have diffg: "g differentiable_on sphere 0 1 ∩ S" by (metis pfg differentiable_on_polynomial_function) define h where "h ≡ λx. inverse(norm(g x)) *⇩_{R}g x" have h: "x ∈ sphere 0 1 ∩ S ⟹ h x ∈ sphere 0 1 ∩ T" for x unfolding h_def using gnz [of x] by (auto simp: subspace_mul [OF ‹subspace T›] subsetD [OF gim]) have diffh: "h differentiable_on sphere 0 1 ∩ S" unfolding h_def apply (intro derivative_intros diffg differentiable_on_compose [OF diffg]) using gnz apply auto done have homfg: "homotopic_with (λz. True) (sphere 0 1 ∩ S) (T - {0}) f g" proof (rule homotopic_with_linear [OF contf]) show "continuous_on (sphere 0 1 ∩ S) g" using pfg by (simp add: differentiable_imp_continuous_on diffg) next have non0fg: "0 ∉ closed_segment (f x) (g x)" if "norm x = 1" "x ∈ S" for x proof - have "f x ∈ sphere 0 1" using fim that by (simp add: image_subset_iff) moreover have "norm(f x - g x) < 1/2" apply (rule g12) using that by force ultimately show ?thesis by (auto simp: norm_minus_commute dest: segment_bound) qed show "⋀x. x ∈ sphere 0 1 ∩ S ⟹ closed_segment (f x) (g x) ⊆ T - {0}" apply (simp add: subset_Diff_insert non0fg) apply (simp add: segment_convex_hull) apply (rule hull_minimal) using fim image_eqI gim apply force apply (rule subspace_imp_convex [OF ‹subspace T›]) done qed obtain d where d: "d ∈ (sphere 0 1 ∩ T) - h ` (sphere 0 1 ∩ S)" using h spheremap_lemma1 [OF ST ‹S ⊆ T› diffh] by force then have non0hd: "0 ∉ closed_segment (h x) (- d)" if "norm x = 1" "x ∈ S" for x using midpoint_between [of 0 "h x" "-d"] that h [of x] by (auto simp: between_mem_segment midpoint_def) have conth: "continuous_on (sphere 0 1 ∩ S) h" using differentiable_imp_continuous_on diffh by blast have hom_hd: "homotopic_with (λz. True) (sphere 0 1 ∩ S) (T - {0}) h (λx. -d)" apply (rule homotopic_with_linear [OF conth continuous_on_const]) apply (simp add: subset_Diff_insert non0hd) apply (simp add: segment_convex_hull) apply (rule hull_minimal) using h d apply (force simp: subspace_neg [OF ‹subspace T›]) apply (rule subspace_imp_convex [OF ‹subspace T›]) done have conT0: "continuous_on (T - {0}) (λy. inverse(norm y) *⇩_{R}y)" by (intro continuous_intros) auto have sub0T: "(λy. y /⇩_{R}norm y) ` (T - {0}) ⊆ sphere 0 1 ∩ T" by (fastforce simp: assms(2) subspace_mul) obtain c where homhc: "homotopic_with (λz. True) (sphere 0 1 ∩ S) (sphere 0 1 ∩ T) h (λx. c)" apply (rule_tac c="-d" in that) apply (rule homotopic_with_eq) apply (rule homotopic_compose_continuous_left [OF hom_hd conT0 sub0T]) using d apply (auto simp: h_def) done show ?thesis apply (rule_tac x=c in exI) apply (rule homotopic_with_trans [OF _ homhc]) apply (rule homotopic_with_eq) apply (rule homotopic_compose_continuous_left [OF homfg conT0 sub0T]) apply (auto simp: h_def) done qed lemma spheremap_lemma3: assumes "bounded S" "convex S" "subspace U" and affSU: "aff_dim S ≤ dim U" obtains T where "subspace T" "T ⊆ U" "S ≠ {} ⟹ aff_dim T = aff_dim S" "(rel_frontier S) homeomorphic (sphere 0 1 ∩ T)" proof (cases "S = {}") case True with ‹subspace U› subspace_0 show ?thesis by (rule_tac T = "{0}" in that) auto next case False then obtain a where "a ∈ S" by auto then have affS: "aff_dim S = int (dim ((λx. -a+x) ` S))" by (metis hull_inc aff_dim_eq_dim) with affSU have "dim ((λx. -a+x) ` S) ≤ dim U" by linarith with choose_subspace_of_subspace obtain T where "subspace T" "T ⊆ span U" and dimT: "dim T = dim ((λx. -a+x) ` S)" . show ?thesis proof (rule that [OF ‹subspace T›]) show "T ⊆ U" using span_eq_iff ‹subspace U› ‹T ⊆ span U› by blast show "aff_dim T = aff_dim S" using dimT ‹subspace T› affS aff_dim_subspace by fastforce show "rel_frontier S homeomorphic sphere 0 1 ∩ T" proof - have "aff_dim (ball 0 1 ∩ T) = aff_dim (T)" 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) then have affS_eq: "aff_dim S = aff_dim (ball 0 1 ∩ T)" using ‹aff_dim T = aff_dim S› by simp have "rel_frontier S homeomorphic rel_frontier(ball 0 1 ∩ T)" apply (rule homeomorphic_rel_frontiers_convex_bounded_sets [OF ‹convex S› ‹bounded S›]) apply (simp add: ‹subspace T› convex_Int subspace_imp_convex) apply (simp add: bounded_Int) apply (rule affS_eq) done also have "... = frontier (ball 0 1) ∩ T" apply (rule convex_affine_rel_frontier_Int [OF convex_ball]) apply (simp add: ‹subspace T› subspace_imp_affine) using ‹subspace T› subspace_0 by force also have "... = sphere 0 1 ∩ T" by auto finally show ?thesis . qed qed qed proposition inessential_spheremap_lowdim_gen: fixes f :: "'M::euclidean_space ⇒ 'a::euclidean_space" assumes "convex S" "bounded S" "convex T" "bounded T" and affST: "aff_dim S < aff_dim T" and contf: "continuous_on (rel_frontier S) f" and fim: "f ` (rel_frontier S) ⊆ rel_frontier T" obtains c where "homotopic_with (λz. True) (rel_frontier S) (rel_frontier T) f (λx. c)" proof (cases "S = {}") case True then show ?thesis by (simp add: that) next case False then show ?thesis proof (cases "T = {}") case True then show ?thesis using fim that by auto next case False obtain T':: "'a set" where "subspace T'" and affT': "aff_dim T' = aff_dim T" and homT: "rel_frontier T homeomorphic sphere 0 1 ∩ T'" apply (rule spheremap_lemma3 [OF ‹bounded T› ‹convex T› subspace_UNIV, where 'b='a]) apply (simp add: aff_dim_le_DIM) using ‹T ≠ {}› by blast with homeomorphic_imp_homotopy_eqv have relT: "sphere 0 1 ∩ T' homotopy_eqv rel_frontier T" using homotopy_eqv_sym by blast have "aff_dim S ≤ int (dim T')" using affT' ‹subspace T'› affST aff_dim_subspace by force with spheremap_lemma3 [OF ‹bounded S› ‹convex S› ‹subspace T'›] ‹S ≠ {}› obtain S':: "'a set" where "subspace S'" "S' ⊆ T'" and affS': "aff_dim S' = aff_dim S" and homT: "rel_frontier S homeomorphic sphere 0 1 ∩ S'" by metis with homeomorphic_imp_homotopy_eqv have relS: "sphere 0 1 ∩ S' homotopy_eqv rel_frontier S" using homotopy_eqv_sym by blast have dimST': "dim S' < dim T'" by (metis ‹S' ⊆ T'› ‹subspace S'› ‹subspace T'› affS' affST affT' less_irrefl not_le subspace_dim_equal) have "∃c. homotopic_with (λz. True) (rel_frontier S) (rel_frontier T) f (λx. c)" apply (rule homotopy_eqv_homotopic_triviality_null_imp [OF relT contf fim]) apply (rule homotopy_eqv_cohomotopic_triviality_null[OF relS, THEN iffD1, rule_format]) apply (metis dimST' ‹subspace S'› ‹subspace T'› ‹S' ⊆ T'› spheremap_lemma2, blast) done with that show ?thesis by blast qed qed lemma inessential_spheremap_lowdim: fixes f :: "'M::euclidean_space ⇒ 'a::euclidean_space" assumes "DIM('M) < DIM('a)" and f: "continuous_on (sphere a r) f" "f ` (sphere a r) ⊆ (sphere b s)" obtains c where "homotopic_with (λz. True) (sphere a r) (sphere b s) f (λx. c)" proof (cases "s ≤ 0") case True then show ?thesis by (meson nullhomotopic_into_contractible f contractible_sphere that) next case False show ?thesis proof (cases "r ≤ 0") case True then show ?thesis by (meson f nullhomotopic_from_contractible contractible_sphere that) next case False with ‹~ s ≤ 0› have "r > 0" "s > 0" by auto show ?thesis apply (rule inessential_spheremap_lowdim_gen [of "cball a r" "cball b s" f]) using ‹0 < r› ‹0 < s› assms(1) apply (simp_all add: f aff_dim_cball) using that by blast qed qed subsection‹ Some technical lemmas about extending maps from cell complexes› lemma extending_maps_Union_aux: assumes fin: "finite ℱ" and "⋀S. S ∈ ℱ ⟹ closed S" and "⋀S T. ⟦S ∈ ℱ; T ∈ ℱ; S ≠ T⟧ ⟹ S ∩ T ⊆ K" and "⋀S. S ∈ ℱ ⟹ ∃g. continuous_on S g ∧ g ` S ⊆ T ∧ (∀x ∈ S ∩ K. g x = h x)" shows "∃g. continuous_on (⋃ℱ) g ∧ g ` (⋃ℱ) ⊆ T ∧ (∀x ∈ ⋃ℱ ∩ K. g x = h x)" using assms proof (induction ℱ) case empty show ?case by simp next case (insert S ℱ) then obtain f where contf: "continuous_on (S) f" and fim: "f ` S ⊆ T" and feq: "∀x ∈ S ∩ K. f x = h x" by (meson insertI1) obtain g where contg: "continuous_on (⋃ℱ) g" and gim: "g ` ⋃ℱ ⊆ T" and geq: "∀x ∈ ⋃ℱ ∩ K. g x = h x" using insert by auto have fg: "f x = g x" if "x ∈ T" "T ∈ ℱ" "x ∈ S" for x T proof - have "T ∩ S ⊆ K ∨ S = T" using that by (metis (no_types) insert.prems(2) insertCI) then show ?thesis using UnionI feq geq ‹S ∉ ℱ› subsetD that by fastforce qed show ?case apply (rule_tac x="λx. if x ∈ S then f x else g x" in exI, simp) apply (intro conjI continuous_on_cases) apply (simp_all add: insert closed_Union contf contg) using fim gim feq geq apply (force simp: insert closed_Union contf contg inf_commute intro: fg)+ done qed lemma extending_maps_Union: assumes fin: "finite ℱ" and "⋀S. S ∈ ℱ ⟹ ∃g. continuous_on S g ∧ g ` S ⊆ T ∧ (∀x ∈ S ∩ K. g x = h x)" and "⋀S. S ∈ ℱ ⟹ closed S" and K: "⋀X Y. ⟦X ∈ ℱ; Y ∈ ℱ; ~ X ⊆ Y; ~ Y ⊆ X⟧ ⟹ X ∩ Y ⊆ K" shows "∃g. continuous_on (⋃ℱ) g ∧ g ` (⋃ℱ) ⊆ T ∧ (∀x ∈ ⋃ℱ ∩ K. g x = h x)" apply (simp add: Union_maximal_sets [OF fin, symmetric]) apply (rule extending_maps_Union_aux) apply (simp_all add: Union_maximal_sets [OF fin] assms) by (metis K psubsetI) lemma extend_map_lemma: assumes "finite ℱ" "𝒢 ⊆ ℱ" "convex T" "bounded T" and poly: "⋀X. X ∈ ℱ ⟹ polytope X" and aff: "⋀X. X ∈ ℱ - 𝒢 ⟹ aff_dim X < aff_dim T" and face: "⋀S T. ⟦S ∈ ℱ; T ∈ ℱ⟧ ⟹ (S ∩ T) face_of S ∧ (S ∩ T) face_of T" and contf: "continuous_on (⋃𝒢) f" and fim: "f ` (⋃𝒢) ⊆ rel_frontier T" obtains g where "continuous_on (⋃ℱ) g" "g ` (⋃ℱ) ⊆ rel_frontier T" "⋀x. x ∈ ⋃𝒢 ⟹ g x = f x" proof (cases "ℱ - 𝒢 = {}") case True then have "⋃ℱ ⊆ ⋃𝒢" by (simp add: Union_mono) then show ?thesis apply (rule_tac g=f in that) using contf continuous_on_subset apply blast using fim apply blast by simp next case False then have "0 ≤ aff_dim T" by (metis aff aff_dim_empty aff_dim_geq aff_dim_negative_iff all_not_in_conv not_less) then obtain i::nat where i: "int i = aff_dim T" by (metis nonneg_eq_int) have Union_empty_eq: "⋃{D. D = {} ∧ P D} = {}" for P :: "'a set ⇒ bool" by auto have extendf: "∃g. continuous_on (⋃(𝒢 ∪ {D. ∃C ∈ ℱ. D face_of C ∧ aff_dim D < i})) g ∧ g ` (⋃ (𝒢 ∪ {D. ∃C ∈ ℱ. D face_of C ∧ aff_dim D < i})) ⊆ rel_frontier T ∧ (∀x ∈ ⋃𝒢. g x = f x)" if "i ≤ aff_dim T" for i::nat using that proof (induction i) case 0 then show ?case apply (simp add: Union_empty_eq) apply (rule_tac x=f in exI) apply (intro conjI) using contf continuous_on_subset apply blast using fim apply blast by simp next case (Suc p) with ‹bounded T› have "rel_frontier T ≠ {}" by (auto simp: rel_frontier_eq_empty affine_bounded_eq_lowdim [of T]) then obtain t where t: "t ∈ rel_frontier T" by auto have ple: "int p ≤ aff_dim T" using Suc.prems by force obtain h where conth: "continuous_on (⋃(𝒢 ∪ {D. ∃C ∈ ℱ. D face_of C ∧ aff_dim D < p})) h" and him: "h ` (⋃ (𝒢 ∪ {D. ∃C ∈ ℱ. D face_of C ∧ aff_dim D < p})) ⊆ rel_frontier T" and heq: "⋀x. x ∈ ⋃𝒢 ⟹ h x = f x" using Suc.IH [OF ple] by auto let ?Faces = "{D. ∃C ∈ ℱ. D face_of C ∧ aff_dim D ≤ p}" have extendh: "∃g. continuous_on D g ∧ g ` D ⊆ rel_frontier T ∧ (∀x ∈ D ∩ ⋃(𝒢 ∪ {D. ∃C ∈ ℱ. D face_of C ∧ aff_dim D < p}). g x = h x)" if D: "D ∈ 𝒢 ∪ ?Faces" for D proof (cases "D ⊆ ⋃(𝒢 ∪ {D. ∃C ∈ ℱ. D face_of C ∧ aff_dim D < p})") case True then show ?thesis apply (rule_tac x=h in exI) apply (intro conjI) apply (blast intro: continuous_on_subset [OF conth]) using him apply blast by simp next case False note notDsub = False show ?thesis proof (cases "∃a. D = {a}") case True then obtain a where "D = {a}" by auto with notDsub t show ?thesis by (rule_tac x="λx. t" in exI) simp next case False have "D ≠ {}" using notDsub by auto have Dnotin: "D ∉ 𝒢 ∪ {D. ∃C ∈ ℱ. D face_of C ∧ aff_dim D < p}" using notDsub by auto then have "D ∉ 𝒢" by simp have "D ∈ ?Faces - {D. ∃C ∈ ℱ. D face_of C ∧ aff_dim D < p}" using Dnotin that by auto then obtain C where "C ∈ ℱ" "D face_of C" and affD: "aff_dim D = int p" by auto then have "bounded D" using face_of_polytope_polytope poly polytope_imp_bounded by blast then have [simp]: "¬ affine D" using affine_bounded_eq_trivial False ‹D ≠ {}› ‹bounded D› by blast have "{F. F facet_of D} ⊆ {E. E face_of C ∧ aff_dim E < int p}" apply clarify apply (metis ‹D face_of C› affD eq_iff face_of_trans facet_of_def zle_diff1_eq) done moreover have "polyhedron D" using ‹C ∈ ℱ› ‹D face_of C› face_of_polytope_polytope poly polytope_imp_polyhedron by auto ultimately have relf_sub: "rel_frontier D ⊆ ⋃ {E. E face_of C ∧ aff_dim E < p}" by (simp add: rel_frontier_of_polyhedron Union_mono) then have him_relf: "h ` rel_frontier D ⊆ rel_frontier T" using ‹C ∈ ℱ› him by blast have "convex D" by (simp add: ‹polyhedron D› polyhedron_imp_convex) have affD_lessT: "aff_dim D < aff_dim T" using Suc.prems affD by linarith have contDh: "continuous_on (rel_frontier D) h" using ‹C ∈ ℱ› relf_sub by (blast intro: continuous_on_subset [OF conth]) then have *: "(∃c. homotopic_with (λx. True) (rel_frontier D) (rel_frontier T) h (λx. c)) = (∃g. continuous_on UNIV g ∧ range g ⊆ rel_frontier T ∧ (∀x∈rel_frontier D. g x = h x))" apply (rule nullhomotopic_into_rel_frontier_extension [OF closed_rel_frontier]) apply (simp_all add: assms rel_frontier_eq_empty him_relf) done have "(∃c. homotopic_with (λx. True) (rel_frontier D) (rel_frontier T) h (λx. c))" by (metis inessential_spheremap_lowdim_gen [OF ‹convex D› ‹bounded D› ‹convex T› ‹bounded T› affD_lessT contDh him_relf]) then obtain g where contg: "continuous_on UNIV g" and gim: "range g ⊆ rel_frontier T" and gh: "⋀x. x ∈ rel_frontier D ⟹ g x = h x" by (metis *) have "D ∩ E ⊆ rel_frontier D" if "E ∈ 𝒢 ∪ {D. Bex ℱ ((face_of) D) ∧ aff_dim D < int p}" for E proof (rule face_of_subset_rel_frontier) show "D ∩ E face_of D" using that ‹C ∈ ℱ› ‹D face_of C› face apply auto apply (meson face_of_Int_subface ‹𝒢 ⊆ ℱ› face_of_refl_eq poly polytope_imp_convex subsetD) using face_of_Int_subface apply blast done show "D ∩ E ≠ D" using that notDsub by auto qed then show ?thesis apply (rule_tac x=g in exI) apply (intro conjI ballI) using continuous_on_subset contg apply blast using gim apply blast using gh by fastforce qed qed have intle: "i < 1 + int j ⟷ i ≤ int j" for i j by auto have "finite 𝒢" using ‹finite ℱ› ‹𝒢 ⊆ ℱ› rev_finite_subset by blast then have fin: "finite (𝒢 ∪ ?Faces)" apply simp apply (rule_tac B = "⋃{{D. D face_of C}| C. C ∈ ℱ}" in finite_subset) by (auto simp: ‹finite ℱ› finite_polytope_faces poly) have clo: "closed S" if "S ∈ 𝒢 ∪ ?Faces" for S using that ‹𝒢 ⊆ ℱ› face_of_polytope_polytope poly polytope_imp_closed by blast have K: "X ∩ Y ⊆ ⋃(𝒢 ∪ {D. ∃C∈ℱ. D face_of C ∧ aff_dim D < int p})" if "X ∈ 𝒢 ∪ ?Faces" "Y ∈ 𝒢 ∪ ?Faces" "~ Y ⊆ X" for X Y proof - have ff: "X ∩ Y face_of X ∧ X ∩ Y face_of Y" if XY: "X face_of D" "Y face_of E" and DE: "D ∈ ℱ" "E ∈ ℱ" for D E apply (rule face_of_Int_subface [OF _ _ XY]) apply (auto simp: face DE) done show ?thesis using that apply auto apply (drule_tac x="X ∩ Y" in spec, safe) using ff face_of_imp_convex [of X] face_of_imp_convex [of Y] apply (fastforce dest: face_of_aff_dim_lt) by (meson face_of_trans ff) qed obtain g where "continuous_on (⋃(𝒢 ∪ ?Faces)) g" "g ` ⋃(𝒢 ∪ ?Faces) ⊆ rel_frontier T" "(∀x ∈ ⋃(𝒢 ∪ ?Faces) ∩ ⋃(𝒢 ∪ {D. ∃C∈ℱ. D face_of C ∧ aff_dim D < p}). g x = h x)" apply (rule exE [OF extending_maps_Union [OF fin extendh clo K]], blast+) done then show ?case apply (simp add: intle local.heq [symmetric], blast) done qed have eq: "⋃(𝒢 ∪ {D. ∃C ∈ ℱ. D face_of C ∧ aff_dim D < i}) = ⋃ℱ" proof show "⋃(𝒢 ∪ {D. ∃C∈ℱ. D face_of C ∧ aff_dim D < int i}) ⊆ ⋃ℱ" apply (rule Union_subsetI) using ‹𝒢 ⊆ ℱ› face_of_imp_subset apply force done show "⋃ℱ ⊆ ⋃(𝒢 ∪ {D. ∃C∈ℱ. D face_of C ∧ aff_dim D < i})" apply (rule Union_mono) using face apply (fastforce simp: aff i) done qed have "int i ≤ aff_dim T" by (simp add: i) then show ?thesis using extendf [of i] unfolding eq by (metis that) qed lemma extend_map_lemma_cofinite0: assumes "finite ℱ" and "pairwise (λS T. S ∩ T ⊆ K) ℱ" and "⋀S. S ∈ ℱ ⟹ ∃a g. a ∉ U ∧ continuous_on (S - {a}) g ∧ g ` (S - {a}) ⊆ T ∧ (∀x ∈ S ∩ K. g x = h x)" and "⋀S. S ∈ ℱ ⟹ closed S" shows "∃C g. finite C ∧ disjnt C U ∧ card C ≤ card ℱ ∧ continuous_on (⋃ℱ - C) g ∧ g ` (⋃ℱ - C) ⊆ T ∧ (∀x ∈ (⋃ℱ - C) ∩ K. g x = h x)" using assms proof induction case empty then show ?case by force next case (insert X ℱ) then have "closed X" and clo: "⋀X. X ∈ ℱ ⟹ closed X" and ℱ: "⋀S. S ∈ ℱ ⟹ ∃a g. a ∉ U ∧ continuous_on (S - {a}) g ∧ g ` (S - {a}) ⊆ T ∧ (∀x ∈ S ∩ K. g x = h x)" and pwX: "⋀Y. Y ∈ ℱ ∧ Y ≠ X ⟶ X ∩ Y ⊆ K ∧ Y ∩ X ⊆ K" and pwF: "pairwise (λ S T. S ∩ T ⊆ K) ℱ" by (simp_all add: pairwise_insert) obtain C g where C: "finite C" "disjnt C U" "card C ≤ card ℱ" and contg: "continuous_on (⋃ℱ - C) g" and gim: "g ` (⋃ℱ - C) ⊆ T" and gh: "⋀x. x ∈ (⋃ℱ - C) ∩ K ⟹ g x = h x" using insert.IH [OF pwF ℱ clo] by auto obtain a f where "a ∉ U" and contf: "continuous_on (X - {a}) f" and fim: "f ` (X - {a}) ⊆ T" and fh: "(∀x ∈ X ∩ K. f x = h x)" using insert.prems by (meson insertI1) show ?case proof (intro exI conjI) show "finite (insert a C)" by (simp add: C) show "disjnt (insert a C) U" using C ‹a ∉ U› by simp show "card (insert a C) ≤ card (insert X ℱ)" by (simp add: C card_insert_if insert.hyps le_SucI) have "closed (⋃ℱ)" using clo insert.hyps by blast have "continuous_on (X - insert a C ∪ (⋃ℱ - insert a C)) (λx. if x ∈ X then f x else g x)" apply (rule continuous_on_cases_local) apply (simp_all add: closedin_closed) using ‹closed X› apply blast using ‹closed (⋃ℱ)› apply blast using contf apply (force simp: elim: continuous_on_subset) using contg apply (force simp: elim: continuous_on_subset) using fh gh insert.hyps pwX by fastforce then show "continuous_on (⋃insert X ℱ - insert a C) (λa. if a ∈ X then f a else g a)" by (blast intro: continuous_on_subset) show "∀x∈(⋃insert X ℱ - insert a C) ∩ K. (if x ∈ X then f x else g x) = h x" using gh by (auto simp: fh) show "(λa. if a ∈ X then f a else g a) ` (⋃insert X ℱ - insert a C) ⊆ T" using fim gim by auto force qed qed lemma extend_map_lemma_cofinite1: assumes "finite ℱ" and ℱ: "⋀X. X ∈ ℱ ⟹ ∃a g. a ∉ U ∧ continuous_on (X - {a}) g ∧ g ` (X - {a}) ⊆ T ∧ (∀x ∈ X ∩ K. g x = h x)" and clo: "⋀X. X ∈ ℱ ⟹ closed X" and K: "⋀X Y. ⟦X ∈ ℱ; Y ∈ ℱ; ~(X ⊆ Y); ~(Y ⊆ X)⟧ ⟹ X ∩ Y ⊆ K" obtains C g where "finite C" "disjnt C U" "card C ≤ card ℱ" "continuous_on (⋃ℱ - C) g" "g ` (⋃ℱ - C) ⊆ T" "⋀x. x ∈ (⋃ℱ - C) ∩ K ⟹ g x = h x" proof - let ?ℱ = "{X ∈ ℱ. ∀Y∈ℱ. ¬ X ⊂ Y}" have [simp]: "⋃?ℱ = ⋃ℱ" by (simp add: Union_maximal_sets assms) have fin: "finite ?ℱ" by (force intro: finite_subset [OF _ ‹finite ℱ›]) have pw: "pairwise (λ S T. S ∩ T ⊆ K) ?ℱ" by (simp add: pairwise_def) (metis K psubsetI) have "card {X ∈ ℱ. ∀Y∈ℱ. ¬ X ⊂ Y} ≤ card ℱ" by (simp add: ‹finite ℱ› card_mono) moreover obtain C g where "finite C ∧ disjnt C U ∧ card C ≤ card ?ℱ ∧ continuous_on (⋃?ℱ - C) g ∧ g ` (⋃?ℱ - C) ⊆ T ∧ (∀x ∈ (⋃?ℱ - C) ∩ K. g x = h x)" apply (rule exE [OF extend_map_lemma_cofinite0 [OF fin pw, of U T h]]) apply (fastforce intro!: clo ℱ)+ done ultimately show ?thesis by (rule_tac C=C and g=g in that) auto qed lemma extend_map_lemma_cofinite: assumes "finite ℱ" "𝒢 ⊆ ℱ" and T: "convex T" "bounded T" and poly: "⋀X. X ∈ ℱ ⟹ polytope X" and contf: "continuous_on (⋃𝒢) f" and fim: "f ` (⋃𝒢) ⊆ rel_frontier T" and face: "⋀X Y. ⟦X ∈ ℱ; Y ∈ ℱ⟧ ⟹ (X ∩ Y) face_of X ∧ (X ∩ Y) face_of Y" and aff: "⋀X. X ∈ ℱ - 𝒢 ⟹ aff_dim X ≤ aff_dim T" obtains C g where "finite C" "disjnt C (⋃𝒢)" "card C ≤ card ℱ" "continuous_on (⋃ℱ - C) g" "g ` (⋃ ℱ - C) ⊆ rel_frontier T" "⋀x. x ∈ ⋃𝒢 ⟹ g x = f x" proof - define ℋ where "ℋ ≡ 𝒢 ∪ {D. ∃C ∈ ℱ - 𝒢. D face_of C ∧ aff_dim D < aff_dim T}" have "finite 𝒢" using assms finite_subset by blast moreover have "finite (⋃{{D. D face_of C} |C. C ∈ ℱ})" apply (rule finite_Union) apply (simp add: ‹finite ℱ›) using finite_polytope_faces poly by auto ultimately have "finite ℋ" apply (simp add: ℋ_def) apply (rule finite_subset [of _ "⋃ {{D. D face_of C} | C. C ∈ ℱ}"], auto) done have *: "⋀X Y. ⟦X ∈ ℋ; Y ∈ ℋ⟧ ⟹ X ∩ Y face_of X ∧ X ∩ Y face_of Y" unfolding ℋ_def apply (elim UnE bexE CollectE DiffE) using subsetD [OF ‹𝒢 ⊆ ℱ›] apply (simp_all add: face) apply (meson subsetD [OF ‹𝒢 ⊆ ℱ›] face face_of_Int_subface face_of_imp_subset face_of_refl poly polytope_imp_convex)+ done obtain h where conth: "continuous_on (⋃ℋ) h" and him: "h ` (⋃ℋ) ⊆ rel_frontier T" and hf: "⋀x. x ∈ ⋃𝒢 ⟹ h x = f x" using ‹finite ℋ› unfolding ℋ_def apply (rule extend_map_lemma [OF _ Un_upper1 T _ _ _ contf fim]) using ‹𝒢 ⊆ ℱ› face_of_polytope_polytope poly apply fastforce using * apply (auto simp: ℋ_def) done have "bounded (⋃𝒢)" using ‹finite 𝒢› ‹𝒢 ⊆ ℱ› poly polytope_imp_bounded by blast then have "⋃𝒢 ≠ UNIV" by auto then obtain a where a: "a ∉ ⋃𝒢" by blast have ℱ: "∃a g. a ∉ ⋃𝒢 ∧ continuous_on (D - {a}) g ∧ g ` (D - {a}) ⊆ rel_frontier T ∧ (∀x ∈ D ∩ ⋃ℋ. g x = h x)" if "D ∈ ℱ" for D proof (cases "D ⊆ ⋃ℋ") case True then show ?thesis apply (rule_tac x=a in exI) apply (rule_tac x=h in exI) using him apply (blast intro!: ‹a ∉ ⋃𝒢› continuous_on_subset [OF conth]) + done next case False note D_not_subset = False show ?thesis proof (cases "D ∈ 𝒢") case True with D_not_subset show ?thesis by (auto simp: ℋ_def) next case False then have affD: "aff_dim D ≤ aff_dim T" by (simp add: ‹D ∈ ℱ› aff) show ?thesis proof (cases "rel_interior D = {}") case True with ‹D ∈ ℱ› poly a show ?thesis by (force simp: rel_interior_eq_empty polytope_imp_convex) next case False then obtain b where brelD: "b ∈ rel_interior D" by blast have "polyhedron D" by (simp add: poly polytope_imp_polyhedron that) have "rel_frontier D retract_of affine hull D - {b}" by (simp add: rel_frontier_retract_of_punctured_affine_hull poly polytope_imp_bounded polytope_imp_convex that brelD) then obtain r where relfD: "rel_frontier D ⊆ affine hull D - {b}" and contr: "continuous_on (affine hull D - {b}) r" and rim: "r ` (affine hull D - {b}) ⊆ rel_frontier D" and rid: "⋀x. x ∈ rel_frontier D ⟹ r x = x" by (auto simp: retract_of_def retraction_def) show ?thesis proof (intro exI conjI ballI) show "b ∉ ⋃𝒢" proof clarify fix E assume "b ∈ E" "E ∈ 𝒢" then have "E ∩ D face_of E ∧ E ∩ D face_of D" using ‹𝒢 ⊆ ℱ› face that by auto with face_of_subset_rel_frontier ‹E ∈ 𝒢› ‹b ∈ E› brelD rel_interior_subset [of D] D_not_subset rel_frontier_def ℋ_def show False by blast qed have "r ` (D - {b}) ⊆ r ` (affine hull D - {b})" by (simp add: Diff_mono hull_subset image_mono) also have "... ⊆ rel_frontier D" by (rule rim) also have "... ⊆ ⋃{E. E face_of D ∧ aff_dim E < aff_dim T}" using affD by (force simp: rel_frontier_of_polyhedron [OF ‹polyhedron D›] facet_of_def) also have "... ⊆ ⋃(ℋ)" using D_not_subset ℋ_def that by fastforce finally have rsub: "r ` (D - {b}) ⊆ ⋃(ℋ)" . show "continuous_on (D - {b}) (h ∘ r)" apply (intro conjI ‹b ∉ ⋃𝒢› continuous_on_compose) apply (rule continuous_on_subset [OF contr]) apply (simp add: Diff_mono hull_subset) apply (rule continuous_on_subset [OF conth rsub]) done show "(h ∘ r) ` (D - {b}) ⊆ rel_frontier T" using brelD him rsub by fastforce show "(h ∘ r) x = h x" if x: "x ∈ D ∩ ⋃ℋ" for x proof - consider A where "x ∈ D" "A ∈ 𝒢" "x ∈ A" | A B where "x ∈ D" "A face_of B" "B ∈ ℱ" "B ∉ 𝒢" "aff_dim A < aff_dim T" "x ∈ A" using x by (auto simp: ℋ_def) then have xrel: "x ∈ rel_frontier D" proof cases case 1 show ?thesis proof (rule face_of_subset_rel_frontier [THEN subsetD]) show "D ∩ A face_of D" using ‹A ∈ 𝒢› ‹𝒢 ⊆ ℱ› face ‹D ∈ ℱ› by blast show "D ∩ A ≠ D" using ‹A ∈ 𝒢› D_not_subset ℋ_def by blast qed (auto simp: 1) next case 2 show ?thesis proof (rule face_of_subset_rel_frontier [THEN subsetD]) show "D ∩ A face_of D" apply (rule face_of_Int_subface [of D B _ A, THEN conjunct1]) apply (simp_all add: 2 ‹D ∈ ℱ› face) apply (simp add: ‹polyhedron D› polyhedron_imp_convex face_of_refl) done show "D ∩ A ≠ D" using "2" D_not_subset ℋ_def by blast qed (auto simp: 2) qed show ?thesis by (simp add: rid xrel) qed qed qed qed qed have clo: "⋀S. S ∈ ℱ ⟹ closed S" by (simp add: poly polytope_imp_closed) obtain C g where "finite C" "disjnt C (⋃𝒢)" "card C ≤ card ℱ" "continuous_on (⋃ℱ - C) g" "g ` (⋃ℱ - C) ⊆ rel_frontier T" and gh: "⋀x. x ∈ (⋃ℱ - C) ∩ ⋃ℋ ⟹ g x = h x" proof (rule extend_map_lemma_cofinite1 [OF ‹finite ℱ› ℱ clo]) show "X ∩ Y ⊆ ⋃ℋ" if XY: "X ∈ ℱ" "Y ∈ ℱ" and "¬ X ⊆ Y" "¬ Y ⊆ X" for X Y proof (cases "X ∈ 𝒢") case True then show ?thesis by (auto simp: ℋ_def) next case False have "X ∩ Y ≠ X" using ‹¬ X ⊆ Y› by blast with XY show ?thesis by (clarsimp simp: ℋ_def) (metis Diff_iff Int_iff aff antisym_conv face face_of_aff_dim_lt face_of_refl not_le poly polytope_imp_convex) qed qed (blast)+ with ‹𝒢 ⊆ ℱ› show ?thesis apply (rule_tac C=C and g=g in that) apply (auto simp: disjnt_def hf [symmetric] ℋ_def intro!: gh) done qed text‹The next two proofs are similar› theorem extend_map_cell_complex_to_sphere: assumes "finite ℱ" and S: "S ⊆ ⋃ℱ" "closed S" and T: "convex T" "bounded T" and poly: "⋀X. X ∈ ℱ ⟹ polytope X" and aff: "⋀X. X ∈ ℱ ⟹ aff_dim X < aff_dim T" and face: "⋀X Y. ⟦X ∈ ℱ; Y ∈ ℱ⟧ ⟹ (X ∩ Y) face_of X ∧ (X ∩ Y) face_of Y" and contf: "continuous_on S f" and fim: "f ` S ⊆ rel_frontier T" obtains g where "continuous_on (⋃ℱ) g" "g ` (⋃ℱ) ⊆ rel_frontier T" "⋀x. x ∈ S ⟹ g x = f x" proof - 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" using neighbourhood_extension_into_ANR [OF contf fim _ ‹closed S›] ANR_rel_frontier_convex T by blast have "compact S" by (meson assms compact_Union poly polytope_imp_compact seq_compact_closed_subset seq_compact_eq_compact) then obtain d where "d > 0" and d: "⋀x y. ⟦x ∈ S; y ∈ - V⟧ ⟹ d ≤ dist x y" using separate_compact_closed [of S "-V"] ‹open V› ‹S ⊆ V› by force obtain 𝒢 where "finite 𝒢" "⋃𝒢 = ⋃ℱ" and diaG: "⋀X. X ∈ 𝒢 ⟹ diameter X < d" and polyG: "⋀X. X ∈ 𝒢 ⟹ polytope X" and affG: "⋀X. X ∈ 𝒢 ⟹ aff_dim X ≤ aff_dim T - 1" and faceG: "⋀X Y. ⟦X ∈ 𝒢; Y ∈ 𝒢⟧ ⟹ X ∩ Y face_of X ∧ X ∩ Y face_of Y" proof (rule cell_complex_subdivision_exists [OF ‹d>0› ‹finite ℱ› poly _ face]) show "⋀X. X ∈ ℱ ⟹ aff_dim X ≤ aff_dim T - 1" by (simp add: aff) qed auto obtain h where conth: "continuous_on (⋃𝒢) h" and him: "h ` ⋃𝒢 ⊆ rel_frontier T" and hg: "⋀x. x ∈ ⋃(𝒢 ∩ Pow V) ⟹ h x = g x" proof (rule extend_map_lemma [of 𝒢 "𝒢 ∩ Pow V" T g]) show "continuous_on (⋃(𝒢 ∩ Pow V)) g" by (metis Union_Int_subset Union_Pow_eq ‹continuous_on V g› continuous_on_subset le_inf_iff) qed (use ‹finite 𝒢› T polyG affG faceG gim in fastforce)+ show ?thesis proof show "continuous_on (⋃ℱ) h" using ‹⋃𝒢 = ⋃ℱ› conth by auto show "h ` ⋃ℱ ⊆ rel_frontier T" using ‹⋃𝒢 = ⋃ℱ› him by auto show "h x = f x" if "x ∈ S" for x proof - have "x ∈ ⋃𝒢" using ‹⋃𝒢 = ⋃ℱ› ‹S ⊆ ⋃ℱ› that by auto then obtain X where "x ∈ X" "X ∈ 𝒢" by blast then have "diameter X < d" "bounded X" by (auto simp: diaG ‹X ∈ 𝒢› polyG polytope_imp_bounded) then have "X ⊆ V" using d [OF ‹x ∈ S›] diameter_bounded_bound [OF ‹bounded X› ‹x ∈ X›] by fastforce have "h x = g x" apply (rule hg) using ‹X ∈ 𝒢› ‹X ⊆ V› ‹x ∈ X› by blast also have "... = f x" by (simp add: gf that) finally show "h x = f x" . qed qed qed theorem extend_map_cell_complex_to_sphere_cofinite: assumes "finite ℱ" and S: "S ⊆ ⋃ℱ" "closed S" and T: "convex T" "bounded T" and poly: "⋀X. X ∈ ℱ ⟹ polytope X" and aff: "⋀X. X ∈ ℱ ⟹ aff_dim X ≤ aff_dim T" and face: "⋀X Y. ⟦X ∈ ℱ; Y ∈ ℱ⟧ ⟹ (X ∩ Y) face_of X ∧ (X ∩ Y) face_of Y" and contf: "continuous_on S f" and fim: "f ` S ⊆ rel_frontier T" obtains C g where "finite C" "disjnt C S" "continuous_on (⋃ℱ - C) g" "g ` (⋃ℱ - C) ⊆ rel_frontier T" "⋀x. x ∈ S ⟹ g x = f x" proof - 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" using neighbourhood_extension_into_ANR [OF contf fim _ ‹closed S›] ANR_rel_frontier_convex T by blast have "compact S" by (meson assms compact_Union poly polytope_imp_compact seq_compact_closed_subset seq_compact_eq_compact) then obtain d where "d > 0" and d: "⋀x y. ⟦x ∈ S; y ∈ - V⟧ ⟹ d ≤ dist x y" using separate_compact_closed [of S "-V"] ‹open V› ‹S ⊆ V› by force obtain 𝒢 where "finite 𝒢" "⋃𝒢 = ⋃ℱ" and diaG: "⋀X. X ∈ 𝒢 ⟹ diameter X < d" and polyG: "⋀X. X ∈ 𝒢 ⟹ polytope X" and affG: "⋀X. X ∈ 𝒢 ⟹ aff_dim X ≤ aff_dim T" and faceG: "⋀X Y. ⟦X ∈ 𝒢; Y ∈ 𝒢⟧ ⟹ X ∩ Y face_of X ∧ X ∩ Y face_of Y" by (rule cell_complex_subdivision_exists [OF ‹d>0› ‹finite ℱ› poly aff face]) auto obtain C h where "finite C" and dis: "disjnt C (⋃(𝒢 ∩ Pow V))" and card: "card C ≤ card 𝒢" and conth: "continuous_on (⋃𝒢 - C) h" and him: "h ` (⋃𝒢 - C) ⊆ rel_frontier T" and hg: "⋀x. x ∈ ⋃(𝒢 ∩ Pow V) ⟹ h x = g x" proof (rule extend_map_lemma_cofinite [of 𝒢 "𝒢 ∩ Pow V" T g]) show "continuous_on (⋃(𝒢 ∩ Pow V)) g" by (metis Union_Int_subset Union_Pow_eq ‹continuous_on V g› continuous_on_subset le_inf_iff) show "g ` ⋃(𝒢 ∩ Pow V) ⊆ rel_frontier T" using gim by force qed (auto intro: ‹finite 𝒢› T polyG affG dest: faceG) have Ssub: "S ⊆ ⋃(𝒢 ∩ Pow V)" proof fix x assume "x ∈ S" then have "x ∈ ⋃𝒢" using ‹⋃𝒢 = ⋃ℱ› ‹S ⊆ ⋃ℱ› by auto then obtain X where "x ∈ X" "X ∈ 𝒢" by blast then have "diameter X < d" "bounded X" by (auto simp: diaG ‹X ∈ 𝒢› polyG polytope_imp_bounded) then have "X ⊆ V" using d [OF ‹x ∈ S›] diameter_bounded_bound [OF ‹bounded X› ‹x ∈ X›] by fastforce then show "x ∈ ⋃(𝒢 ∩ Pow V)" using ‹X ∈ 𝒢› ‹x ∈ X› by blast qed show ?thesis proof show "continuous_on (⋃ℱ-C) h" using ‹⋃𝒢 = ⋃ℱ› conth by auto show "h ` (⋃ℱ - C) ⊆ rel_frontier T" using ‹⋃𝒢 = ⋃ℱ› him by auto show "h x = f x" if "x ∈ S" for x proof - have "h x = g x" apply (rule hg) using Ssub that by blast also have "... = f x" by (simp add: gf that) finally show "h x = f x" . qed show "disjnt C S" using dis Ssub by (meson disjnt_iff subset_eq) qed (intro ‹finite C›) qed subsection‹ Special cases and corollaries involving spheres› lemma disjnt_Diff1: "X ⊆ Y' ⟹ disjnt (X - Y) (X' - Y')" by (auto simp: disjnt_def) proposition extend_map_affine_to_sphere_cofinite_simple: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "compact S" "convex U" "bounded U" and aff: "aff_dim T ≤ aff_dim U" and "S ⊆ T" and contf: "continuous_on S f" and fim: "f ` S ⊆ rel_frontier U" obtains K g where "finite K" "K ⊆ T" "disjnt K S" "continuous_on (T - K) g" "g ` (T - K) ⊆ rel_frontier U" "⋀x. x ∈ S ⟹ g x = f x" proof - have "∃K g. finite K ∧ disjnt K S ∧ continuous_on (T - K) g ∧ g ` (T - K) ⊆ rel_frontier U ∧ (∀x ∈ S. g x = f x)" if "affine T" "S ⊆ T" and aff: "aff_dim T ≤ aff_dim U" for T proof (cases "S = {}") case True show ?thesis proof (cases "rel_frontier U = {}") case True with ‹bounded U› have "aff_dim U ≤ 0" using affine_bounded_eq_lowdim rel_frontier_eq_empty by auto with aff have "aff_dim T ≤ 0" by auto then obtain a where "T ⊆ {a}" using ‹affine T› affine_bounded_eq_lowdim affine_bounded_eq_trivial by auto then show ?thesis using ‹S = {}› fim by (metis Diff_cancel contf disjnt_empty2 finite.emptyI finite_insert finite_subset) next case False then obtain a where "a ∈ rel_frontier U" by auto then show ?thesis using continuous_on_const [of _ a] ‹S = {}› by force qed next case False have "bounded S" by (simp add: ‹compact S› compact_imp_bounded) then obtain b where b: "S ⊆ cbox (-b) b" using bounded_subset_cbox_symmetric by blast define bbox where "bbox ≡ cbox (-(b+One)) (b+One)" have "cbox (-b) b ⊆ bbox" by (auto simp: bbox_def algebra_simps intro!: subset_box_imp) with b ‹S ⊆ T› have "S ⊆ bbox ∩ T" by auto then have Ssub: "S ⊆ ⋃{bbox ∩ T}" by auto then have "aff_dim (bbox ∩ T) ≤ aff_dim U" by (metis aff aff_dim_subset inf_commute inf_le1 order_trans) obtain K g where K: "finite K" "disjnt K S" and contg: "continuous_on (⋃{bbox ∩ T} - K) g" and gim: "g ` (⋃{bbox ∩ T} - K) ⊆ rel_frontier U" and gf: "⋀x. x ∈ S ⟹ g x = f x" proof (rule extend_map_cell_complex_to_sphere_cofinite [OF _ Ssub _ ‹convex U› ‹bounded U› _ _ _ contf fim]) show "closed S" using ‹compact S› compact_eq_bounded_closed by auto show poly: "⋀X. X ∈ {bbox ∩ T} ⟹ polytope X" by (simp add: polytope_Int_polyhedron bbox_def polytope_interval affine_imp_polyhedron ‹affine T›) show "⋀X Y. ⟦X ∈ {bbox ∩ T}; Y ∈ {bbox ∩ T}⟧ ⟹ X ∩ Y face_of X ∧ X ∩ Y face_of Y" by (simp add:poly face_of_refl polytope_imp_convex) show "⋀X. X ∈ {bbox ∩ T} ⟹ aff_dim X ≤ aff_dim U" by (simp add: ‹aff_dim (bbox ∩ T) ≤ aff_dim U›) qed auto define fro where "fro ≡ λd. frontier(cbox (-(b + d *⇩_{R}One)) (b + d *⇩_{R}One))" obtain d where d12: "1/2 ≤ d" "d ≤ 1" and dd: "disjnt K (fro d)" proof (rule disjoint_family_elem_disjnt [OF _ ‹finite K›]) show "infinite {1/2..1::real}" by (simp add: infinite_Icc) have dis1: "disjnt (fro x) (fro y)" if "x<y" for x y by (auto simp: algebra_simps that subset_box_imp disjnt_Diff1 frontier_def fro_def) then show "disjoint_family_on fro {1/2..1}" by (auto simp: disjoint_family_on_def disjnt_def neq_iff) qed auto define c where "c ≡ b + d *⇩_{R}One" have cbsub: "cbox (-b) b ⊆ box (-c) c" "cbox (-b) b ⊆ cbox (-c) c" "cbox (-c) c ⊆ bbox" using d12 by (auto simp: algebra_simps subset_box_imp c_def bbox_def) have clo_cbT: "closed (cbox (- c) c ∩ T)" by (simp add: affine_closed closed_Int closed_cbox ‹affine T›) have cpT_ne: "cbox (- c) c ∩ T ≠ {}" using ‹S ≠ {}› b cbsub(2) ‹S ⊆ T› by fastforce have "closest_point (cbox (- c) c ∩ T) x ∉ K" if "x ∈ T" "x ∉ K" for x proof (cases "x ∈ cbox (-c) c") case True with that show ?thesis by (simp add: closest_point_self) next case False have int_ne: "interior (cbox (-c) c) ∩ T ≠ {}" using ‹S ≠ {}› ‹S ⊆ T› b ‹cbox (- b) b ⊆ box (- c) c› by force have "convex T" by (meson ‹affine T› affine_imp_convex) then have "x ∈ affine hull (cbox (- c) c ∩ T)" 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) then have "x ∈ affine hull (cbox (- c) c ∩ T) - rel_interior (cbox (- c) c ∩ T)" by (meson DiffI False Int_iff rel_interior_subset subsetCE) then have "closest_point (cbox (- c) c ∩ T) x ∈ rel_frontier (cbox (- c) c ∩ T)" by (rule closest_point_in_rel_frontier [OF clo_cbT cpT_ne]) moreover have "(rel_frontier (cbox (- c) c ∩ T)) ⊆ fro d" apply (subst convex_affine_rel_frontier_Int [OF _ ‹affine T› int_ne]) apply (auto simp: fro_def c_def) done ultimately show ?thesis using dd by (force simp: disjnt_def) qed then have cpt_subset: "closest_point (cbox (- c) c ∩ T) ` (T - K) ⊆ ⋃{bbox ∩ T} - K" using closest_point_in_set [OF clo_cbT cpT_ne] cbsub(3) by force show ?thesis proof (intro conjI ballI exI) have "continuous_on (T - K) (closest_point (cbox (- c) c ∩ T))" apply (rule continuous_on_closest_point) using ‹S ≠ {}› cbsub(2) b that by (auto simp: affine_imp_convex convex_Int affine_closed closed_Int closed_cbox ‹affine T›) then show "continuous_on (T - K) (g ∘ closest_point (cbox (- c) c ∩ T))" by (metis continuous_on_compose continuous_on_subset [OF contg cpt_subset]) have "(g ∘ closest_point (cbox (- c) c ∩ T)) ` (T - K) ⊆ g ` (⋃{bbox ∩ T} - K)" by (metis image_comp image_mono cpt_subset) also have "... ⊆ rel_frontier U" by (rule gim) finally show "(g ∘ closest_point (cbox (- c) c ∩ T)) ` (T - K) ⊆ rel_frontier U" . show "(g ∘ closest_point (cbox (- c) c ∩ T)) x = f x" if "x ∈ S" for x proof - have "(g ∘ closest_point (cbox (- c) c ∩ T)) x = g x" unfolding o_def by (metis IntI ‹S ⊆ T› b cbsub(2) closest_point_self subset_eq that) also have "... = f x" by (simp add: that gf) finally show ?thesis . qed qed (auto simp: K) qed then obtain K g where "finite K" "disjnt K S" and contg: "continuous_on (affine hull T - K) g" and gim: "g ` (affine hull T - K) ⊆ rel_frontier U" and gf: "⋀x. x ∈ S ⟹ g x = f x" by (metis aff affine_affine_hull aff_dim_affine_hull order_trans [OF ‹S ⊆ T› hull_subset [of T affine]]) then obtain K g where "finite K" "disjnt K S" and contg: "continuous_on (T - K) g" and gim: "g ` (T - K) ⊆ rel_frontier U" and gf: "⋀x. x ∈ S ⟹ g x = f x" by (rule_tac K=K and g=g in that) (auto simp: hull_inc elim: continuous_on_subset) then show ?thesis by (rule_tac K="K ∩ T" and g=g in that) (auto simp: disjnt_iff Diff_Int contg) qed subsection‹Extending maps to spheres› (*Up to extend_map_affine_to_sphere_cofinite_gen*) lemma extend_map_affine_to_sphere1: fixes f :: "'a::euclidean_space ⇒ 'b::topological_space" assumes "finite K" "affine U" and contf: "continuous_on (U - K) f" and fim: "f ` (U - K) ⊆ T" and comps: "⋀C. ⟦C ∈ components(U - S); C ∩ K ≠ {}⟧ ⟹ C ∩ L ≠ {}" and clo: "closedin (subtopology euclidean U) S" and K: "disjnt K S" "K ⊆ U" obtains g where "continuous_on (U - L) g" "g ` (U - L) ⊆ T" "⋀x. x ∈ S ⟹ g x = f x" proof (cases "K = {}") case True then show ?thesis by (metis Diff_empty Diff_subset contf fim continuous_on_subset image_subsetI rev_image_eqI subset_iff that) next case False have "S ⊆ U" using clo closedin_limpt by blast then have "(U - S) ∩ K ≠ {}" by (metis Diff_triv False Int_Diff K disjnt_def inf.absorb_iff2 inf_commute) then have "⋃(components (U - S)) ∩ K ≠ {}" using Union_components by simp then obtain C0 where C0: "C0 ∈ components (U - S)" "C0 ∩ K ≠ {}" by blast have "convex U" by (simp add: affine_imp_convex ‹affine U›) then have "locally connected U" by (rule convex_imp_locally_connected) have "∃a g. a ∈ C ∧ a ∈ L ∧ continuous_on (S ∪ (C - {a})) g ∧ g ` (S ∪ (C - {a})) ⊆ T ∧ (∀x ∈ S. g x = f x)" if C: "C ∈ components (U - S)" and CK: "C ∩ K ≠ {}" for C proof - have "C ⊆ U-S" "C ∩ L ≠ {}" by (simp_all add: in_components_subset comps that) then obtain a where a: "a ∈ C" "a ∈ L" by auto have opeUC: "openin (subtopology euclidean U) C" proof (rule openin_trans) show "openin (subtopology euclidean (U-S)) C" by (simp add: ‹locally connected U› clo locally_diff_closed openin_components_locally_connected [OF _ C]) show "openin (subtopology euclidean U) (U - S)" by (simp add: clo openin_diff) qed then obtain d where "C ⊆ U" "0 < d" and d: "cball a d ∩ U ⊆ C" using openin_contains_cball by (metis ‹a ∈ C›) then have "ball a d ∩ U ⊆ C" by auto obtain h k where homhk: "homeomorphism (S ∪ C) (S ∪ C) h k" and subC: "{x. (~ (h x = x ∧ k x = x))} ⊆ C" and bou: "bounded {x. (~ (h x = x ∧ k x = x))}" and hin: "⋀x. x ∈ C ∩ K ⟹ h x ∈ ball a d ∩ U" proof (rule homeomorphism_grouping_points_exists_gen [of C "ball a d ∩ U" "C ∩ K" "S ∪ C"]) show "openin (subtopology euclidean C) (ball a d ∩ U)" by (metis open_ball ‹C ⊆ U› ‹ball a d ∩ U ⊆ C› inf.absorb_iff2 inf.orderE inf_assoc open_openin openin_subtopology) show "openin (subtopology euclidean (affine hull C)) C" by (metis ‹a ∈ C› ‹openin (subtopology euclidean U) C› affine_hull_eq affine_hull_openin all_not_in_conv ‹affine U›) show "ball a d ∩ U ≠ {}" using ‹0 < d› ‹C ⊆ U› ‹a ∈ C› by force show "finite (C ∩ K)" by (simp add: ‹finite K›) show "S ∪ C ⊆ affine hull C" by (metis ‹C ⊆ U› ‹S ⊆ U› ‹a ∈ C› opeUC affine_hull_eq affine_hull_openin all_not_in_conv assms(2) sup.bounded_iff) show "connected C" by (metis C in_components_connected) qed auto have a_BU: "a ∈ ball a d ∩ U" using ‹0 < d› ‹C ⊆ U› ‹a ∈ C› by auto have "rel_frontier (cball a d ∩ U) retract_of (affine hull (cball a d ∩ U) - {a})" apply (rule rel_frontier_retract_of_punctured_affine_hull) apply (auto simp: ‹convex U› convex_Int) by (metis ‹affine U› convex_cball empty_iff interior_cball a_BU rel_interior_convex_Int_affine) moreover have "rel_frontier (cball a d ∩ U) = frontier (cball a d) ∩ U" apply (rule convex_affine_rel_frontier_Int) using a_BU by (force simp: ‹affine U›)+ moreover have "affine hull (cball a d ∩ U) = U" by (metis ‹convex U› a_BU affine_hull_convex_Int_nonempty_interior affine_hull_eq ‹affine U› equals0D inf.commute interior_cball) ultimately have "frontier (cball a d) ∩ U retract_of (U - {a})" by metis then obtain r where contr: "continuous_on (U - {a}) r" and rim: "r ` (U - {a}) ⊆ sphere a d" "r ` (U - {a}) ⊆ U" and req: "⋀x. x ∈ sphere a d ∩ U ⟹ r x = x" using ‹affine U› by (auto simp: retract_of_def retraction_def hull_same) define j where "j ≡ λx. if x ∈ ball a d then r x else x" have kj: "⋀x. x ∈ S ⟹ k (j x) = x" using ‹C ⊆ U - S› ‹S ⊆ U› ‹ball a d ∩ U ⊆ C› j_def subC by auto have Uaeq: "U - {a} = (cball a d - {a}) ∩ U ∪ (U - ball a d)" using ‹0 < d› by auto have jim: "j ` (S ∪ (C - {a})) ⊆ (S ∪ C) - ball a d" proof clarify fix y assume "y ∈ S ∪ (C - {a})" then have "y ∈ U - {a}" using ‹C ⊆ U - S› ‹S ⊆ U› ‹a ∈ C› by auto then have "r y ∈ sphere a d" using rim by auto then show "j y ∈ S ∪ C - ball a d" apply (simp add: j_def) using ‹r y ∈ sphere a d› ‹y ∈ U - {a}› ‹y ∈ S ∪ (C - {a})› d rim by fastforce qed have contj: "continuous_on (U - {a}) j" unfolding j_def Uaeq proof (intro continuous_on_cases_local continuous_on_id, simp_all add: req closedin_closed Uaeq [symmetric]) show "∃T. closed T ∧ (cball a d - {a}) ∩ U = (U - {a}) ∩ T" apply (rule_tac x="(cball a d) ∩ U" in exI) using affine_closed ‹affine U› by blast show "∃T. closed T ∧ U - ball a d = (U - {a}) ∩ T" apply (rule_tac x="U - ball a d" in exI) using ‹0 < d› by (force simp: affine_closed ‹affine U› closed_Diff) show "continuous_on ((cball a d - {a}) ∩ U) r" by (force intro: continuous_on_subset [OF contr]) qed have fT: "x ∈ U - K ⟹ f x ∈ T" for x using fim by blast show ?thesis proof (intro conjI exI) show "continuous_on (S ∪ (C - {a})) (f ∘ k ∘ j)" proof (intro continuous_on_compose) show "continuous_on (S ∪ (C - {a})) j" apply (rule continuous_on_subset [OF contj]) using ‹C ⊆ U - S› ‹S ⊆ U› ‹a ∈ C› by force show "continuous_on (j ` (S ∪ (C - {a}))) k" apply (rule continuous_on_subset [OF homeomorphism_cont2 [OF homhk]]) using jim ‹C ⊆ U - S› ‹S ⊆ U› ‹ball a d ∩ U ⊆ C› j_def by fastforce show "continuous_on (k ` j ` (S ∪ (C - {a}))) f" proof (clarify intro!: continuous_on_subset [OF contf]) fix y assume "y ∈ S ∪ (C - {a})" have ky: "k y ∈ S ∪ C" using homeomorphism_image2 [OF homhk] ‹y ∈ S ∪ (C - {a})› by blast have jy: "j y ∈ S ∪ C - ball a d" using Un_iff ‹y ∈ S ∪ (C - {a})› jim by auto show "k (j y) ∈ U - K" apply safe using ‹C ⊆ U› ‹S ⊆ U› homeomorphism_image2 [OF homhk] jy apply blast by (metis DiffD1 DiffD2 Int_iff Un_iff ‹disjnt K S› disjnt_def empty_iff hin homeomorphism_apply2 homeomorphism_image2 homhk imageI jy) qed qed have ST: "⋀x. x ∈ S ⟹ (f ∘ k ∘ j) x ∈ T" apply (simp add: kj) apply (metis DiffI ‹S ⊆ U› ‹disjnt K S› subsetD disjnt_iff fim image_subset_iff) done moreover have "(f ∘ k ∘ j) x ∈ T" if "x ∈ C" "x ≠ a" "x ∉ S" for x proof - have rx: "r x ∈ sphere a d" using ‹C ⊆ U› rim that by fastforce have jj: "j x ∈ S ∪ C - ball a d" using jim that by blast have "k (j x) = j x ⟶ k (j x) ∈ C ∨ j x ∈ C" by (metis Diff_iff Int_iff Un_iff ‹S ⊆ U› subsetD d j_def jj rx sphere_cball that(1)) then have "k (j x) ∈ C" using homeomorphism_apply2 [OF homhk, of "j x"] ‹C ⊆ U› ‹S ⊆ U› a rx by (metis (mono_tags, lifting) Diff_iff subsetD jj mem_Collect_eq subC) with jj ‹C ⊆ U› show ?thesis apply safe using ST j_def apply fastforce apply (auto simp: not_less intro!: fT) by (metis DiffD1 DiffD2 Int_iff hin homeomorphism_apply2 [OF homhk] jj) qed ultimately show "(f ∘ k ∘ j) ` (S ∪ (C - {a})) ⊆ T" by force show "∀x∈S. (f ∘ k ∘ j) x = f x" using kj by simp qed (auto simp: a) qed then obtain a h where ah: "⋀C. ⟦C ∈ components (U - S); C ∩ K ≠ {}⟧ ⟹ a C ∈ C ∧ a C ∈ L ∧ continuous_on (S ∪ (C - {a C})) (h C) ∧ h C ` (S ∪ (C - {a C})) ⊆ T ∧ (∀x ∈ S. h C x = f x)" using that by metis define F where "F ≡ {C ∈ components (U - S). C ∩ K ≠ {}}" define G where "G ≡ {C ∈ components (U - S). C ∩ K = {}}" define UF where "UF ≡ (⋃C∈F. C - {a C})" have "C0 ∈ F" by (auto simp: F_def C0) have "finite F" proof (subst finite_image_iff [of "λC. C ∩ K" F, symmetric]) show "inj_on (λC. C ∩ K) F" unfolding F_def inj_on_def using components_nonoverlap by blast show "finite ((λC. C ∩ K) ` F)" unfolding F_def by (rule finite_subset [of _ "Pow K"]) (auto simp: ‹finite K›) qed obtain g where contg: "continuous_on (S ∪ UF) g" and gh: "⋀x i. ⟦i ∈ F; x ∈ (S ∪ UF) ∩ (S ∪ (i - {a i}))⟧ ⟹ g x = h i x" proof (rule pasting_lemma_exists_closed [OF ‹finite F›, of "S ∪ UF" "λC. S ∪ (C - {a C})" h]) show "S ∪ UF ⊆ (⋃C∈F. S ∪ (C - {a C}))" using ‹C0 ∈ F› by (force simp: UF_def) show "closedin (subtopology euclidean (S ∪ UF)) (S ∪ (C - {a C}))" if "C ∈ F" for C proof (rule closedin_closed_subset [of U "S ∪ C"]) show "closedin (subtopology euclidean U) (S ∪ C)" apply (rule closedin_Un_complement_component [OF ‹locally connected U› clo]) using F_def that by blast next have "x = a C'" if "C' ∈ F" "x ∈ C'" "x ∉ U" for x C' proof - have "∀A. x ∈ ⋃A ∨ C' ∉ A" using ‹x ∈ C'› by blast with that show "x = a C'" by (metis (lifting) DiffD1 F_def Union_components mem_Collect_eq) qed then show "S ∪ UF ⊆ U" using ‹S ⊆ U› by (force simp: UF_def) next show "S ∪ (C - {a C}) = (S ∪ C) ∩ (S ∪ UF)" using F_def UF_def components_nonoverlap that by auto qed next show "continuous_on (S ∪ (C' - {a C'})) (h C')" if "C' ∈ F" for C' using ah F_def that by blast show "⋀i j x. ⟦i ∈ F; j ∈ F; x ∈ (S ∪ UF) ∩ (S ∪ (i - {a i})) ∩ (S ∪ (j - {a j}))⟧ ⟹ h i x = h j x" using components_eq by (fastforce simp: components_eq F_def ah) qed blast have SU': "S ∪ ⋃G ∪ (S ∪ UF) ⊆ U" using ‹S ⊆ U› in_components_subset by (auto simp: F_def G_def UF_def) have clo1: "closedin (subtopology euclidean (S ∪ ⋃G ∪ (S ∪ UF))) (S ∪ ⋃G)" proof (rule closedin_closed_subset [OF _ SU']) have *: "⋀C. C ∈ F ⟹ openin (subtopology euclidean U) C" unfolding F_def by clarify (metis (no_types, lifting) ‹locally connected U› clo closedin_def locally_diff_closed openin_components_locally_connected openin_trans topspace_euclidean_subtopology) show "closedin (subtopology euclidean U) (U - UF)" unfolding UF_def by (force intro: openin_delete *) show "S ∪ ⋃G = (U - UF) ∩ (S ∪ ⋃G ∪ (S ∪ UF))" using ‹S ⊆ U› apply (auto simp: F_def G_def UF_def) apply (metis Diff_iff UnionI Union_components) apply (metis DiffD1 UnionI Union_components) by (metis (no_types, lifting) IntI components_nonoverlap empty_iff) qed have clo2: "closedin (subtopology euclidean (S ∪ ⋃G ∪ (S ∪ UF))) (S ∪ UF)" proof (rule closedin_closed_subset [OF _ SU']) show "closedin (subtopology euclidean U) (⋃C∈F. S ∪ C)" apply (rule closedin_Union) apply (simp add: ‹finite F›) using F_def ‹locally connected U› clo closedin_Un_complement_component by blast show "S ∪ UF = (⋃C∈F. S ∪ C) ∩ (S ∪ ⋃G ∪ (S ∪ UF))" using ‹S ⊆ U› apply (auto simp: F_def G_def UF_def) using C0 apply blast by (metis components_nonoverlap disjnt_def disjnt_iff) qed have SUG: "S ∪ ⋃G ⊆ U - K" using ‹S ⊆ U› K apply (auto simp: G_def disjnt_iff) by (meson Diff_iff subsetD in_components_subset) then have contf': "continuous_on (S ∪ ⋃G) f" by (rule continuous_on_subset [OF contf]) have contg': "continuous_on (S ∪ UF) g" apply (rule continuous_on_subset [OF contg]) using ‹S ⊆ U› by (auto simp: F_def G_def) have "⋀x. ⟦S ⊆ U; x ∈ S⟧ ⟹ f x = g x" by (subst gh) (auto simp: ah C0 intro: ‹C0 ∈ F›) then have f_eq_g: "⋀x. x ∈ S ∪ UF ∧ x ∈ S ∪ ⋃G ⟹ f x = g x" using ‹S ⊆ U› apply (auto simp: F_def G_def UF_def dest: in_components_subset) using components_eq by blast have cont: "continuous_on (S ∪ ⋃G ∪ (S ∪ UF)) (λx. if x ∈ S ∪ ⋃G then f x else g x)" by (blast intro: continuous_on_cases_local [OF clo1 clo2 contf' contg' f_eq_g, of "λx. x ∈ S ∪ ⋃G"]) show ?thesis proof have UF: "⋃F - L ⊆ UF" unfolding F_def UF_def using ah by blast have "U - S - L = ⋃(components (U - S)) - L" by simp also have "... = ⋃F ∪ ⋃G - L" unfolding F_def G_def by blast also have "... ⊆ UF ∪ ⋃G" using UF by blast finally have "U - L ⊆ S ∪ ⋃G ∪ (S ∪ UF)" by blast then show "continuous_on (U - L) (λx. if x ∈ S ∪ ⋃G then f x else g x)" by (rule continuous_on_subset [OF cont]) have "((U - L) ∩ {x. x ∉ S ∧ (∀xa∈G. x ∉ xa)}) ⊆ ((U - L) ∩ (-S ∩ UF))" using ‹U - L ⊆ S ∪ ⋃G ∪ (S ∪ UF)› by auto moreover have "g ` ((U - L) ∩ (-S ∩ UF)) ⊆ T" proof - have "g x ∈ T" if "x ∈ U" "x ∉ L" "x ∉ S" "C ∈ F" "x ∈ C" "x ≠ a C" for x C proof (subst gh) show "x ∈ (S ∪ UF) ∩ (S ∪ (C - {a C}))" using that by (auto simp: UF_def) show "h C x ∈ T" using ah that by (fastforce simp add: F_def) qed (rule that) then show ?thesis by (force simp: UF_def) qed ultimately have "g ` ((U - L) ∩ {x. x ∉ S ∧ (∀xa∈G. x ∉ xa)}) ⊆ T" using image_mono order_trans by blast moreover have "f ` ((U - L) ∩ (S ∪ ⋃G)) ⊆ T" using fim SUG by blast ultimately show "(λx. if x ∈ S ∪ ⋃G then f x else g x) ` (U - L) ⊆ T" by force show "⋀x. x ∈ S ⟹ (if x ∈ S ∪ ⋃G then f x else g x) = f x" by (simp add: F_def G_def) qed qed lemma extend_map_affine_to_sphere2: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "compact S" "convex U" "bounded U" "affine T" "S ⊆ T" and affTU: "aff_dim T ≤ aff_dim U" and contf: "continuous_on S f" and fim: "f ` S ⊆ rel_frontier U" and ovlap: "⋀C. C ∈ components(T - S) ⟹ C ∩ L ≠ {}" obtains K g where "finite K" "K ⊆ L" "K ⊆ T" "disjnt K S" "continuous_on (T - K) g" "g ` (T - K) ⊆ rel_frontier U" "⋀x. x ∈ S ⟹ g x = f x" proof - obtain K g where K: "finite K" "K ⊆ T" "disjnt K S" and contg: "continuous_on (T - K) g" and gim: "g ` (T - K) ⊆ rel_frontier U" and gf: "⋀x. x ∈ S ⟹ g x = f x" using assms extend_map_affine_to_sphere_cofinite_simple by metis have "(∃y C. C ∈ components (T - S) ∧ x ∈ C ∧ y ∈ C ∧ y ∈ L)" if "x ∈ K" for x proof - have "x ∈ T-S" using ‹K ⊆ T› ‹disjnt K S› disjnt_def that by fastforce then obtain C where "C ∈ components(T - S)" "x ∈ C" by (metis UnionE Union_components) with ovlap [of C] show ?thesis by blast qed then obtain ξ where ξ: "⋀x. x ∈ K ⟹ ∃C. C ∈ components (T - S) ∧ x ∈ C ∧ ξ x ∈ C ∧ ξ x ∈ L" by metis obtain h where conth: "continuous_on (T - ξ ` K) h" and him: "h ` (T - ξ ` K) ⊆ rel_frontier U" and hg: "⋀x. x ∈ S ⟹ h x = g x" proof (rule extend_map_affine_to_sphere1 [OF ‹finite K› ‹affine T› contg gim, of S "ξ ` K"]) show cloTS: "closedin (subtopology euclidean T) S" by (simp add: ‹compact S› ‹S ⊆ T› closed_subset compact_imp_closed) show "⋀C. ⟦C ∈ components (T - S); C ∩ K ≠ {}⟧ ⟹ C ∩ ξ ` K ≠ {}" using ξ components_eq by blast qed (use K in auto) show ?thesis proof show *: "ξ ` K ⊆ L" using ξ by blast show "finite (ξ ` K)" by (simp add: K) show "ξ ` K ⊆ T" by clarify (meson ξ Diff_iff contra_subsetD in_components_subset) show "continuous_on (T - ξ ` K) h" by (rule conth) show "disjnt (ξ ` K) S" using K apply (auto simp: disjnt_def) by (metis ξ DiffD2 UnionI Union_components) qed (simp_all add: him hg gf) qed proposition extend_map_affine_to_sphere_cofinite_gen: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes SUT: "compact S" "convex U" "bounded U" "affine T" "S ⊆ T" and aff: "aff_dim T ≤ aff_dim U" and contf: "continuous_on S f" and fim: "f ` S ⊆ rel_frontier U" and dis: "⋀C. ⟦C ∈ components(T - S); bounded C⟧ ⟹ C ∩ L ≠ {}" obtains K g where "finite K" "K ⊆ L" "K ⊆ T" "disjnt K S" "continuous_on (T - K) g" "g ` (T - K) ⊆ rel_frontier U" "⋀x. x ∈ S ⟹ g x = f x" proof (cases "S = {}") case True show ?thesis proof (cases "rel_frontier U = {}") case True with aff have "aff_dim T ≤ 0" apply (simp add: rel_frontier_eq_empty) using affine_bounded_eq_lowdim ‹bounded U› order_trans by auto with aff_dim_geq [of T] consider "aff_dim T = -1" | "aff_dim T = 0" by linarith then show ?thesis proof cases assume "aff_dim T = -1" then have "T = {}" by (simp add: aff_dim_empty) then show ?thesis by (rule_tac K="{}" in that) auto next assume "aff_dim T = 0" then obtain a where "T = {a}" using aff_dim_eq_0 by blast then have "a ∈ L" using dis [of "{a}"] ‹S = {}› by (auto simp: in_components_self) with ‹S = {}› ‹T = {a}› show ?thesis by (rule_tac K="{a}" and g=f in that) auto qed next case False then obtain y where "y ∈ rel_frontier U" by auto with ‹S = {}› show ?thesis by (rule_tac K="{}" and g="λx. y" in that) (auto simp: continuous_on_const) qed next case False have "bounded S" by (simp add: assms compact_imp_bounded) then obtain b where b: "S ⊆ cbox (-b) b" using bounded_subset_cbox_symmetric by blast define LU where "LU ≡ L ∪ (⋃ {C ∈ components (T - S). ~bounded C} - cbox (-(b+One)) (b+One))" obtain K g where "finite K" "K ⊆ LU" "K ⊆ T" "disjnt K S" and contg: "continuous_on (T - K) g" and gim: "g ` (T - K) ⊆ rel_frontier U" and gf: "⋀x. x ∈ S ⟹ g x = f x" proof (rule extend_map_affine_to_sphere2 [OF SUT aff contf fim]) show "C ∩ LU ≠ {}" if "C ∈ components (T - S)" for C proof (cases "bounded C") case True with dis that show ?thesis unfolding LU_def by fastforce next case False then have "¬ bounded (⋃{C ∈ components (T - S). ¬ bounded C})" by (metis (no_types, lifting) Sup_upper bounded_subset mem_Collect_eq that) then show ?thesis apply (clarsimp simp: LU_def Int_Un_distrib Diff_Int_distrib Int_UN_distrib) by (metis (no_types, lifting) False Sup_upper bounded_cbox bounded_subset inf.orderE mem_Collect_eq that) qed qed blast have *: False if "x ∈ cbox (- b - m *⇩_{R}One) (b + m *⇩_{R}One)" "x ∉ box (- b - n *⇩_{R}One) (b + n *⇩_{R}One)" "0 ≤ m" "m < n" "n ≤ 1" for m n x using that by (auto simp: mem_box algebra_simps) have "disjoint_family_on (λd. frontier (cbox (- b - d *⇩_{R}One) (b + d *⇩_{R}One))) {1 / 2..1}" by (auto simp: disjoint_family_on_def neq_iff frontier_def dest: *) then obtain d where d12: "1/2 ≤ d" "d ≤ 1" and ddis: "disjnt K (frontier (cbox (-(b + d *⇩_{R}One)) (b + d *⇩_{R}One)))" using disjoint_family_elem_disjnt [of "{1/2..1::real}" K "λd. frontier (cbox (-(b + d *⇩_{R}One)) (b + d *⇩_{R}One))"] by (auto simp: ‹finite K›) define c where "c ≡ b + d *⇩_{R}One" have cbsub: "cbox (-b) b ⊆ box (-c) c" "cbox (-b) b ⊆ cbox (-c) c" "cbox (-c) c ⊆ cbox (-(b+One)) (b+One)" using d12 by (simp_all add: subset_box c_def inner_diff_left inner_left_distrib) have clo_cT: "closed (cbox (- c) c ∩ T)" using affine_closed ‹affine T› by blast have cT_ne: "cbox (- c) c ∩ T ≠ {}" using ‹S ≠ {}› ‹S ⊆ T› b cbsub by fastforce have S_sub_cc: "S ⊆ cbox (- c) c" using ‹cbox (- b) b ⊆ cbox (- c) c› b by auto show ?thesis proof show "finite (K ∩ cbox (-(b+One)) (b+One))" using ‹finite K› by blast show "K ∩ cbox (- (b + One)) (b + One) ⊆ L" using ‹K ⊆ LU› by (auto simp: LU_def) show "K ∩ cbox (- (b + One)) (b + One) ⊆ T" using ‹K ⊆ T› by auto show "disjnt (K ∩ cbox (- (b + One)) (b + One)) S" using ‹disjnt K S› by (simp add: disjnt_def disjoint_eq_subset_Compl inf.coboundedI1) have cloTK: "closest_point (cbox (- c) c ∩ T) x ∈ T - K" if "x ∈ T" and Knot: "x ∈ K ⟶ x ∉ cbox (- b - One) (b + One)" for x proof (cases "x ∈ cbox (- c) c") case True with ‹x ∈ T› show ?thesis using cbsub(3) Knot by (force simp: closest_point_self) next case False have clo_in_rf: "closest_point (cbox (- c) c ∩ T) x ∈ rel_frontier (cbox (- c) c ∩ T)" proof (intro closest_point_in_rel_frontier [OF clo_cT cT_ne] DiffI notI) have "T ∩ interior (cbox (- c) c) ≠ {}" using ‹S ≠ {}› ‹S ⊆ T› b cbsub(1) by fastforce then show "x ∈ affine hull (cbox (- c) c ∩ T)" by (simp add: Int_commute affine_hull_affine_Int_nonempty_interior ‹affine T› hull_inc that(1)) next show "False" if "x ∈ rel_interior (cbox (- c) c ∩ T)" proof - have "interior (cbox (- c) c) ∩ T ≠ {}" using ‹S ≠ {}› ‹S ⊆ T› b cbsub(1) by fastforce then have "affine hull (T ∩ cbox (- c) c) = T" using affine_hull_convex_Int_nonempty_interior [of T "cbox (- c) c"] by (simp add: affine_imp_convex ‹affine T› inf_commute) then show ?thesis by (meson subsetD le_inf_iff rel_interior_subset that False) qed qed have "closest_point (cbox (- c) c ∩ T) x ∉ K" proof assume inK: "closest_point (cbox (- c) c ∩ T) x ∈ K" have "⋀x. x ∈ K ⟹ x ∉ frontier (cbox (- (b + d *⇩_{R}One)) (b + d *⇩_{R}One))" by (metis ddis disjnt_iff) then show False by (metis DiffI Int_iff ‹affine T› cT_ne c_def clo_cT clo_in_rf closest_point_in_set convex_affine_rel_frontier_Int convex_box(1) empty_iff frontier_cbox inK interior_cbox) qed then show ?thesis using cT_ne clo_cT closest_point_in_set by blast qed show "continuous_on (T - K ∩ cbox (- (b + One)) (b + One)) (g ∘ closest_point (cbox (-c) c ∩ T))" apply (intro continuous_on_compose continuous_on_closest_point continuous_on_subset [OF contg]) apply (simp_all add: clo_cT affine_imp_convex ‹affine T› convex_Int cT_ne) using cloTK by blast have "g (closest_point (cbox (- c) c ∩ T) x) ∈ rel_frontier U" if "x ∈ T" "x ∈ K ⟶ x ∉ cbox (- b - One) (b + One)" for x apply (rule gim [THEN subsetD]) using that cloTK by blast then show "(g ∘ closest_point (cbox (- c) c ∩ T)) ` (T - K ∩ cbox (- (b + One)) (b + One)) ⊆ rel_frontier U" by force show "⋀x. x ∈ S ⟹ (g ∘ closest_point (cbox (- c) c ∩ T)) x = f x" by simp (metis (mono_tags, lifting) IntI ‹S ⊆ T› cT_ne clo_cT closest_point_refl gf subsetD S_sub_cc) qed qed corollary extend_map_affine_to_sphere_cofinite: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes SUT: "compact S" "affine T" "S ⊆ T" and aff: "aff_dim T ≤ DIM('b)" and "0 ≤ r" and contf: "continuous_on S f" and fim: "f ` S ⊆ sphere a r" and dis: "⋀C. ⟦C ∈ components(T - S); bounded C⟧ ⟹ C ∩ L ≠ {}" obtains K g where "finite K" "K ⊆ L" "K ⊆ T" "disjnt K S" "continuous_on (T - K) g" "g ` (T - K) ⊆ sphere a r" "⋀x. x ∈ S ⟹ g x = f x" proof (cases "r = 0") case True with fim show ?thesis by (rule_tac K="{}" and g = "λx. a" in that) (auto simp: continuous_on_const) next case False with assms have "0 < r" by auto then have "aff_dim T ≤ aff_dim (cball a r)" by (simp add: aff aff_dim_cball) then show ?thesis apply (rule extend_map_affine_to_sphere_cofinite_gen [OF ‹compact S› convex_cball bounded_cball ‹affine T› ‹S ⊆ T› _ contf]) using fim apply (auto simp: assms False that dest: dis) done qed corollary extend_map_UNIV_to_sphere_cofinite: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes aff: "DIM('a) ≤ DIM('b)" and "0 ≤ r" and SUT: "compact S" and contf: "continuous_on S f" and fim: "f ` S ⊆ sphere a r" and dis: "⋀C. ⟦C ∈ components(- S); bounded C⟧ ⟹ C ∩ L ≠ {}" obtains K g where "finite K" "K ⊆ L" "disjnt K S" "continuous_on (- K) g" "g ` (- K) ⊆ sphere a r" "⋀x. x ∈ S ⟹ g x = f x" apply (rule extend_map_affine_to_sphere_cofinite [OF ‹compact S› affine_UNIV subset_UNIV _ ‹0 ≤ r› contf fim dis]) apply (auto simp: assms that Compl_eq_Diff_UNIV [symmetric]) done corollary extend_map_UNIV_to_sphere_no_bounded_component: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes aff: "DIM('a) ≤ DIM('b)" and "0 ≤ r" and SUT: "compact S" and contf: "continuous_on S f" and fim: "f ` S ⊆ sphere a r" and dis: "⋀C. C ∈ components(- S) ⟹ ¬ bounded C" obtains g where "continuous_on UNIV g" "g ` UNIV ⊆ sphere a r" "⋀x. x ∈ S ⟹ g x = f x" apply (rule extend_map_UNIV_to_sphere_cofinite [OF aff ‹0 ≤ r› ‹compact S› contf fim, of "{}"]) apply (auto simp: that dest: dis) done theorem Borsuk_separation_theorem_gen: fixes S :: "'a::euclidean_space set" assumes "compact S" shows "(∀c ∈ components(- S). ~bounded c) ⟷ (∀f. continuous_on S f ∧ f ` S ⊆ sphere (0::'a) 1 ⟶ (∃c. homotopic_with (λx. True) S (sphere 0 1) f (λx. c)))" (is "?lhs = ?rhs") proof assume L [rule_format]: ?lhs show ?rhs proof clarify fix f :: "'a ⇒ 'a" assume contf: "continuous_on S f" and fim: "f ` S ⊆ sphere 0 1" obtain g where contg: "continuous_on UNIV g" and gim: "range g ⊆ sphere 0 1" and gf: "⋀x. x ∈ S ⟹ g x = f x" by (rule extend_map_UNIV_to_sphere_no_bounded_component [OF _ _ ‹compact S› contf fim L]) auto then show "∃c. homotopic_with (λx. True) S (sphere 0 1) f (λx. c)" using nullhomotopic_from_contractible [OF contg gim] by (metis assms compact_imp_closed contf empty_iff fim homotopic_with_equal nullhomotopic_into_sphere_extension) qed next assume R [rule_format]: ?rhs show ?lhs unfolding components_def proof clarify fix a assume "a ∉ S" and a: "bounded (connected_component_set (- S) a)" have cont: "continuous_on S (λx. inverse(norm(x - a)) *⇩_{R}(x - a))" apply (intro continuous_intros) using ‹a ∉ S› by auto have im: "(λx. inverse(norm(x - a)) *⇩_{R}(x - a)) ` S ⊆ sphere 0 1" by clarsimp (metis ‹a ∉ S› eq_iff_diff_eq_0 left_inverse norm_eq_zero) show False using R cont im Borsuk_map_essential_bounded_component [OF ‹compact S› ‹a ∉ S›] a by blast qed qed corollary Borsuk_separation_theorem: fixes S :: "'a::euclidean_space set" assumes "compact S" and 2: "2 ≤ DIM('a)" shows "connected(- S) ⟷ (∀f. continuous_on S f ∧ f ` S ⊆ sphere (0::'a) 1 ⟶ (∃c. homotopic_with (λx. True) S (sphere 0 1) f (λx. c)))" (is "?lhs = ?rhs") proof assume L: ?lhs show ?rhs proof (cases "S = {}") case True then show ?thesis by auto next case False then have "(∀c∈components (- S). ¬ bounded c)" by (metis L assms(1) bounded_empty cobounded_imp_unbounded compact_imp_bounded in_components_maximal order_refl) then show ?thesis by (simp add: Borsuk_separation_theorem_gen [OF ‹compact S›]) qed next assume R: ?rhs then show ?lhs apply (simp add: Borsuk_separation_theorem_gen [OF ‹compact S›, symmetric]) apply (auto simp: components_def connected_iff_eq_connected_component_set) using connected_component_in apply fastforce using cobounded_unique_unbounded_component [OF _ 2, of "-S"] ‹compact S› compact_eq_bounded_closed by fastforce qed lemma homotopy_eqv_separation: fixes S :: "'a::euclidean_space set" and T :: "'a set" assumes "S homotopy_eqv T" and "compact S" and "compact T" shows "connected(- S) ⟷ connected(- T)" proof - consider "DIM('a) = 1" | "2 ≤ DIM('a)" by (metis DIM_ge_Suc0 One_nat_def Suc_1 dual_order.antisym not_less_eq_eq) then show ?thesis proof cases case 1 then show ?thesis using bounded_connected_Compl_1 compact_imp_bounded homotopy_eqv_empty1 homotopy_eqv_empty2 assms by metis next case 2 with assms show ?thesis by (simp add: Borsuk_separation_theorem homotopy_eqv_cohomotopic_triviality_null) qed qed lemma Jordan_Brouwer_separation: fixes S :: "'a::euclidean_space set" and a::'a assumes hom: "S homeomorphic sphere a r" and "0 < r" shows "¬ connected(- S)" proof - have "- sphere a r ∩ ball a r ≠ {}" using ‹0 < r› by (simp add: Int_absorb1 subset_eq) moreover have eq: "- sphere a r - ball a r = - cball a r" by auto have "- cball a r ≠ {}" proof - have "frontier (cball a r) ≠ {}" using ‹0 < r› by auto then show ?thesis by (metis frontier_complement frontier_empty) qed with eq have "- sphere a r - ball a r ≠ {}" by auto moreover have "connected (- S) = connected (- sphere a r)" proof (rule homotopy_eqv_separation) show "S homotopy_eqv sphere a r" using hom homeomorphic_imp_homotopy_eqv by blast show "compact (sphere a r)" by simp then show " compact S" using hom homeomorphic_compactness by blast qed ultimately show ?thesis using connected_Int_frontier [of "- sphere a r" "ball a r"] by (auto simp: ‹0 < r›) qed lemma Jordan_Brouwer_frontier: fixes S :: "'a::euclidean_space set" and a::'a assumes S: "S homeomorphic sphere a r" and T: "T ∈ components(- S)" and 2: "2 ≤ DIM('a)" shows "frontier T = S" proof (cases r rule: linorder_cases) assume "r < 0" with S T show ?thesis by auto next assume "r = 0" with S T card_eq_SucD obtain b where "S = {b}" by (auto simp: homeomorphic_finite [of "{a}" S]) have "components (- {b}) = { -{b}}" using T ‹S = {b}› by (auto simp: components_eq_sing_iff connected_punctured_universe 2) with T show ?thesis by (metis ‹S = {b}› cball_trivial frontier_cball frontier_complement singletonD sphere_trivial) next assume "r > 0" have "compact S" using homeomorphic_compactness compact_sphere S by blast show ?thesis proof (rule frontier_minimal_separating_closed) show "closed S" using ‹compact S› compact_eq_bounded_closed by blast show "¬ connected (- S)" using Jordan_Brouwer_separation S ‹0 < r› by blast obtain f g where hom: "homeomorphism S (sphere a r) f g" using S by (auto simp: homeomorphic_def) show "connected (- T)" if "closed T" "T ⊂ S" for T proof - have "f ` T ⊆ sphere a r" using ‹T ⊂ S› hom homeomorphism_image1 by blast moreover have "f ` T ≠ sphere a r" using ‹T ⊂ S› hom by (metis homeomorphism_image2 homeomorphism_of_subsets order_refl psubsetE) ultimately have "f ` T ⊂ sphere a r" by blast then have "connected (- f ` T)" by (rule psubset_sphere_Compl_connected [OF _ ‹0 < r› 2]) moreover have "compact T" using ‹compact S› bounded_subset compact_eq_bounded_closed that by blast moreover then have "compact (f ` T)" by (meson compact_continuous_image continuous_on_subset hom homeomorphism_def psubsetE ‹T ⊂ S›) moreover have "T homotopy_eqv f ` T" by (meson ‹f ` T ⊆ sphere a r› dual_order.strict_implies_order hom homeomorphic_def homeomorphic_imp_homotopy_eqv homeomorphism_of_subsets ‹T ⊂ S›) ultimately show ?thesis using homotopy_eqv_separation [of T "f`T"] by blast qed qed (rule T) qed lemma Jordan_Brouwer_nonseparation: fixes S :: "'a::euclidean_space set" and a::'a assumes S: "S homeomorphic sphere a r" and "T ⊂ S" and 2: "2 ≤ DIM('a)" shows "connected(- T)" proof - have *: "connected(C ∪ (S - T))" if "C ∈ components(- S)" for C proof (rule connected_intermediate_closure) show "connected C" using in_components_connected that by auto have "S = frontier C" using "2" Jordan_Brouwer_frontier S that by blast with closure_subset show "C ∪ (S - T) ⊆ closure C" by (auto simp: frontier_def) qed auto have "components(- S) ≠ {}" by (metis S bounded_empty cobounded_imp_unbounded compact_eq_bounded_closed compact_sphere components_eq_empty homeomorphic_compactness) then have "- T = (⋃C ∈ components(- S). C ∪ (S - T))" using Union_components [of "-S"] ‹T ⊂ S› by auto then show ?thesis apply (rule ssubst) apply (rule connected_Union) using ‹T ⊂ S› apply (auto simp: *) done qed subsection‹ Invariance of domain and corollaries› lemma invariance_of_domain_ball: fixes f :: "'a ⇒ 'a::euclidean_space" assumes contf: "continuous_on (cball a r) f" and "0 < r" and inj: "inj_on f (cball a r)" shows "open(f ` ball a r)" proof (cases "DIM('a) = 1") case True obtain h::"'a⇒real" and k where "linear h" "linear k" "h ` UNIV = UNIV" "k ` UNIV = UNIV" "⋀x. norm(h x) = norm x" "⋀x. norm(k x) = norm x" "⋀x. k(h x) = x" "⋀x. h(k x) = x" apply (rule isomorphisms_UNIV_UNIV [where 'M='a and 'N=real]) using True apply force by (metis UNIV_I UNIV_eq_I imageI) have cont: "continuous_on S h" "continuous_on T k" for S T by (simp_all add: ‹linear h› ‹linear k› linear_continuous_on linear_linear) have "continuous_on (h ` cball a r) (h ∘ f ∘ k)" apply (intro continuous_on_compose cont continuous_on_subset [OF contf]) apply (auto simp: ‹⋀x. k (h x) = x›) done moreover have "is_interval (h ` cball a r)" by (simp add: is_interval_connected_1 ‹linear h› linear_continuous_on linear_linear connected_continuous_image) moreover have "inj_on (h ∘ f ∘ k) (h ` cball a r)" using inj by (simp add: inj_on_def) (metis ‹⋀x. k (h x) = x›) ultimately have *: "⋀T. ⟦open T; T ⊆ h ` cball a r⟧ ⟹ open ((h ∘ f ∘ k) ` T)" using injective_eq_1d_open_map_UNIV by blast have "open ((h ∘ f ∘ k) ` (h ` ball a r))" by (rule *) (auto simp: ‹linear h› ‹range h = UNIV› open_surjective_linear_image) then have "open ((h ∘ f) ` ball a r)" by (simp add: image_comp ‹⋀x. k (h x) = x› cong: image_cong) then show ?thesis apply (simp add: image_comp [symmetric]) apply (metis open_bijective_linear_image_eq ‹linear h› ‹⋀x. k (h x) = x› ‹range h = UNIV› bijI inj_on_def) done next case False then have 2: "DIM('a) ≥ 2" by (metis DIM_ge_Suc0 One_nat_def Suc_1 antisym not_less_eq_eq) have fimsub: "f ` ball a r ⊆ - f ` sphere a r" using inj by clarsimp (metis inj_onD less_eq_real_def mem_cball order_less_irrefl) have hom: "f ` sphere a r homeomorphic sphere a r" by (meson compact_sphere contf continuous_on_subset homeomorphic_compact homeomorphic_sym inj inj_on_subset sphere_cball) then have nconn: "¬ connected (- f ` sphere a r)" by (rule Jordan_Brouwer_separation) (auto simp: ‹0 < r›) obtain C where C: "C ∈ components (- f ` sphere a r)" and "bounded C" apply (rule cobounded_has_bounded_component [OF _ nconn]) apply (simp_all add: 2) by (meson compact_imp_bounded compact_continuous_image_eq compact_sphere contf inj sphere_cball) moreover have "f ` (ball a r) = C" proof have "C ≠ {}" by (rule in_components_nonempty [OF C]) show "C ⊆ f ` ball a r" proof (rule ccontr) assume nonsub: "¬ C ⊆ f ` ball a r" have "- f ` cball a r ⊆ C" proof (rule components_maximal [OF C]) have "f ` cball a r homeomorphic cball a r" using compact_cball contf homeomorphic_compact homeomorphic_sym inj by blast then show "connected (- f ` cball a r)" by (auto intro: connected_complement_homeomorphic_convex_compact 2) show "- f ` cball a r ⊆ - f ` sphere a r" by auto then show "C ∩ - f ` cball a r ≠ {}" using ‹C ≠ {}› in_components_subset [OF C] nonsub using image_iff by fastforce qed then have "bounded (- f ` cball a r)" using bounded_subset ‹bounded C› by auto then have "¬ bounded (f ` cball a r)" using cobounded_imp_unbounded by blast then show "False" using compact_continuous_image [OF contf] compact_cball compact_imp_bounded by blast qed with ‹C ≠ {}› have "C ∩ f ` ball a r ≠ {}" by (simp add: inf.absorb_iff1) then show "f ` ball a r ⊆ C" by (metis components_maximal [OF C _ fimsub] connected_continuous_image ball_subset_cball connected_ball contf continuous_on_subset) qed moreover have "open (- f ` sphere a r)" using hom compact_eq_bounded_closed compact_sphere homeomorphic_compactness by blast ultimately show ?thesis using open_components by blast qed text‹Proved by L. E. J. Brouwer (1912)› theorem invariance_of_domain: fixes f :: "'a ⇒ 'a::euclidean_space" assumes "continuous_on S f" "open S" "inj_on f S" shows "open(f ` S)" unfolding open_subopen [of "f`S"] proof clarify fix a assume "a ∈ S" obtain δ where "δ > 0" and δ: "cball a δ ⊆ S" using ‹open S› ‹a ∈ S› open_contains_cball_eq by blast show "∃T. open T ∧ f a ∈ T ∧ T ⊆ f ` S" proof (intro exI conjI) show "open (f ` (ball a δ))" by (meson δ ‹0 < δ› assms continuous_on_subset inj_on_subset invariance_of_domain_ball) show "f a ∈ f ` ball a δ" by (simp add: ‹0 < δ›) show "f ` ball a δ ⊆ f ` S" using δ ball_subset_cball by blast qed qed lemma inv_of_domain_ss0: fixes f :: "'a ⇒ 'a::euclidean_space" assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U ⊆ S" and "subspace S" and dimS: "dim S = DIM('b::euclidean_space)" and ope: "openin (subtopology euclidean S) U" shows "openin (subtopology euclidean S) (f ` U)" proof - have "U ⊆ S" using ope openin_imp_subset by blast have "(UNIV::'b set) homeomorphic S" by (simp add: ‹subspace S› dimS homeomorphic_subspaces) then obtain h k where homhk: "homeomorphism (UNIV::'b set) S h k" using homeomorphic_def by blast have homkh: "homeomorphism S (k ` S) k h" using homhk homeomorphism_image2 homeomorphism_sym by fastforce have "open ((k ∘ f ∘ h) ` k ` U)" proof (rule invariance_of_domain) show "continuous_on (k ` U) (k ∘ f ∘ h)" proof (intro continuous_intros) show "continuous_on (k ` U) h" by (meson continuous_on_subset [OF homeomorphism_cont1 [OF homhk]] top_greatest) show "continuous_on (h ` k ` U) f" apply (rule continuous_on_subset [OF contf], clarify) apply (metis homhk homeomorphism_def ope openin_imp_subset rev_subsetD) done show "continuous_on (f ` h ` k ` U) k" apply (rule continuous_on_subset [OF homeomorphism_cont2 [OF homhk]]) using fim homhk homeomorphism_apply2 ope openin_subset by fastforce qed have ope_iff: "⋀T. open T ⟷ openin (subtopology euclidean (k ` S)) T" using homhk homeomorphism_image2 open_openin by fastforce show "open (k ` U)" by (simp add: ope_iff homeomorphism_imp_open_map [OF homkh ope]) show "inj_on (k ∘ f ∘ h) (k ` U)" apply (clarsimp simp: inj_on_def) by (metis subsetD fim homeomorphism_apply2 [OF homhk] image_subset_iff inj_on_eq_iff injf ‹U ⊆ S›) qed moreover have eq: "f ` U = h ` (k ∘ f ∘ h ∘ k) ` U" apply (auto simp: image_comp [symmetric]) apply (metis homkh ‹U ⊆ S› fim homeomorphism_image2 homeomorphism_of_subsets homhk imageI subset_UNIV) by (metis ‹U ⊆ S› subsetD fim homeomorphism_def homhk image_eqI) ultimately show ?thesis by (metis (no_types, hide_lams) homeomorphism_imp_open_map homhk image_comp open_openin subtopology_UNIV) qed lemma inv_of_domain_ss1: fixes f :: "'a ⇒ 'a::euclidean_space" assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U ⊆ S" and "subspace S" and ope: "openin (subtopology euclidean S) U" shows "openin (subtopology euclidean S) (f ` U)" proof - define S' where "S' ≡ {y. ∀x ∈ S. orthogonal x y}" have "subspace S'" by (simp add: S'_def subspace_orthogonal_to_vectors) define g where "g ≡ λz::'a*'a. ((f ∘ fst)z, snd z)" have "openin (subtopology euclidean (S × S')) (g ` (U × S'))" proof (rule inv_of_domain_ss0) show "continuous_on (U × S') g" apply (simp add: g_def) apply (intro continuous_intros continuous_on_compose2 [OF contf continuous_on_fst], auto) done show "g ` (U × S') ⊆ S × S'" using fim by (auto simp: g_def) show "inj_on g (U × S')" using injf by (auto simp: g_def inj_on_def) show "subspace (S × S')" by (simp add: ‹subspace S'› ‹subspace S› subspace_Times) show "openin (subtopology euclidean (S × S')) (U × S')" by (simp add: openin_Times [OF ope]) have "dim (S × S') = dim S + dim S'" by (simp add: ‹subspace S'› ‹subspace S› dim_Times) also have "... = DIM('a)" using dim_subspace_orthogonal_to_vectors [OF ‹subspace S› subspace_UNIV] by (simp add: add.commute S'_def) finally show "dim (S × S') = DIM('a)" . qed moreover have "g ` (U × S') = f ` U × S'" by (auto simp: g_def image_iff) moreover have "0 ∈ S'" using ‹subspace S'› subspace_affine by blast ultimately show ?thesis by (auto simp: openin_Times_eq) qed corollary invariance_of_domain_subspaces: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes ope: "openin (subtopology euclidean U) S" and "subspace U" "subspace V" and VU: "dim V ≤ dim U" and contf: "continuous_on S f" and fim: "f ` S ⊆ V" and injf: "inj_on f S" shows "openin (subtopology euclidean V) (f ` S)" proof - obtain V' where "subspace V'" "V' ⊆ U" "dim V' = dim V" using choose_subspace_of_subspace [OF VU] by (metis span_eq_iff ‹subspace U›) then have "V homeomorphic V'" by (simp add: ‹subspace V› homeomorphic_subspaces) then obtain h k where homhk: "homeomorphism V V' h k" using homeomorphic_def by blast have eq: "f ` S = k ` (h ∘ f) ` S" proof - have "k ` h ` f ` S = f ` S" by (meson fim homeomorphism_def homeomorphism_of_subsets homhk subset_refl) then show ?thesis by (simp add: image_comp) qed show ?thesis unfolding eq proof (rule homeomorphism_imp_open_map) show homkh: "homeomorphism V' V k h" by (simp add: homeomorphism_symD homhk) have hfV': "(h ∘ f) ` S ⊆ V'" using fim homeomorphism_image1 homhk by fastforce moreover have "openin (subtopology euclidean U) ((h ∘ f) ` S)" proof (rule inv_of_domain_ss1) show "continuous_on S (h ∘ f)" by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_cont1 homhk) show "inj_on (h ∘ f) S" apply (clarsimp simp: inj_on_def) by (metis fim homeomorphism_apply2 [OF homkh] image_subset_iff inj_onD injf) show "(h ∘ f) ` S ⊆ U" using ‹V' ⊆ U› hfV' by auto qed (auto simp: assms) ultimately show "openin (subtopology euclidean V') ((h ∘ f) ` S)" using openin_subset_trans ‹V' ⊆ U› by force qed qed corollary invariance_of_dimension_subspaces: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes ope: "openin (subtopology euclidean U) S" and "subspace U" "subspace V" and contf: "continuous_on S f" and fim: "f ` S ⊆ V" and injf: "inj_on f S" and "S ≠ {}" shows "dim U ≤ dim V" proof - have "False" if "dim V < dim U" proof - obtain T where "subspace T" "T ⊆ U" "dim T = dim V" using choose_subspace_of_subspace [of "dim V" U] by (metis ‹dim V < dim U› assms(2) order.strict_implies_order span_eq_iff) then have "V homeomorphic T" by (simp add: ‹subspace V› homeomorphic_subspaces) then obtain h k where homhk: "homeomorphism V T h k" using homeomorphic_def by blast have "continuous_on S (h ∘ f)" by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_cont1 homhk) moreover have "(h ∘ f) ` S ⊆ U" using ‹T ⊆ U› fim homeomorphism_image1 homhk by fastforce moreover have "inj_on (h ∘ f) S" apply (clarsimp simp: inj_on_def) by (metis fim homeomorphism_apply1 homhk image_subset_iff inj_onD injf) ultimately have ope_hf: "openin (subtopology euclidean U) ((h ∘ f) ` S)" using invariance_of_domain_subspaces [OF ope ‹subspace U› ‹subspace U›] by auto have "(h ∘ f) ` S ⊆ T" using fim homeomorphism_image1 homhk by fastforce then show ?thesis by (metis dim_openin ‹dim T = dim V› ope_hf ‹subspace U› ‹S ≠ {}› dim_subset image_is_empty not_le that) qed then show ?thesis using not_less by blast qed corollary invariance_of_domain_affine_sets: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes ope: "openin (subtopology euclidean U) S" and aff: "affine U" "affine V" "aff_dim V ≤ aff_dim U" and contf: "continuous_on S f" and fim: "f ` S ⊆ V" and injf: "inj_on f S" shows "openin (subtopology euclidean V) (f ` S)" proof (cases "S = {}") case True then show ?thesis by auto next case False obtain a b where "a ∈ S" "a ∈ U" "b ∈ V" using False fim ope openin_contains_cball by fastforce have "openin (subtopology euclidean ((+) (- b) ` V)) (((+) (- b) ∘ f ∘ (+) a) ` (+) (- a) ` S)" proof (rule invariance_of_domain_subspaces) show "openin (subtopology euclidean ((+) (- a) ` U)) ((+) (- a) ` S)" by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois) show "subspace ((+) (- a) ` U)" by (simp add: ‹a ∈ U› affine_diffs_subspace ‹affine U›) show "subspace ((+) (- b) ` V)" by (simp add: ‹b ∈ V› affine_diffs_subspace ‹affine V›) show "dim ((+) (- b) ` V) ≤ dim ((+) (- a) ` U)" by (metis ‹a ∈ U› ‹b ∈ V› aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff) show "continuous_on ((+) (- a) ` S) ((+) (- b) ∘ f ∘ (+) a)" by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois) show "((+) (- b) ∘ f ∘ (+) a) ` (+) (- a) ` S ⊆ (+) (- b) ` V" using fim by auto show "inj_on ((+) (- b) ∘ f ∘ (+) a) ((+) (- a) ` S)" by (auto simp: inj_on_def) (meson inj_onD injf) qed then show ?thesis by (metis (no_types, lifting) homeomorphism_imp_open_map homeomorphism_translation image_comp translation_galois) qed corollary invariance_of_dimension_affine_sets: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes ope: "openin (subtopology euclidean U) S" and aff: "affine U" "affine V" and contf: "continuous_on S f" and fim: "f ` S ⊆ V" and injf: "inj_on f S" and "S ≠ {}" shows "aff_dim U ≤ aff_dim V" proof - obtain a b where "a ∈ S" "a ∈ U" "b ∈ V" using ‹S ≠ {}› fim ope openin_contains_cball by fastforce have "dim ((+) (- a) ` U) ≤ dim ((+) (- b) ` V)" proof (rule invariance_of_dimension_subspaces) show "openin (subtopology euclidean ((+) (- a) ` U)) ((+) (- a) ` S)" by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois) show "subspace ((+) (- a) ` U)" by (simp add: ‹a ∈ U› affine_diffs_subspace ‹affine U›) show "subspace ((+) (- b) ` V)" by (simp add: ‹b ∈ V› affine_diffs_subspace ‹affine V›) show "continuous_on ((+) (- a) ` S) ((+) (- b) ∘ f ∘ (+) a)" by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois) show "((+) (- b) ∘ f ∘ (+) a) ` (+) (- a) ` S ⊆ (+) (- b) ` V" using fim by auto show "inj_on ((+) (- b) ∘ f ∘ (+) a) ((+) (- a) ` S)" by (auto simp: inj_on_def) (meson inj_onD injf) qed (use ‹S ≠ {}› in auto) then show ?thesis by (metis ‹a ∈ U› ‹b ∈ V› aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff) qed corollary invariance_of_dimension: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes contf: "continuous_on S f" and "open S" and injf: "inj_on f S" and "S ≠ {}" shows "DIM('a) ≤ DIM('b)" using invariance_of_dimension_subspaces [of UNIV S UNIV f] assms by auto corollary continuous_injective_image_subspace_dim_le: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "subspace S" "subspace T" and contf: "continuous_on S f" and fim: "f ` S ⊆ T" and injf: "inj_on f S" shows "dim S ≤ dim T" apply (rule invariance_of_dimension_subspaces [of S S _ f]) using assms by (auto simp: subspace_affine) lemma invariance_of_dimension_convex_domain: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "convex S" and contf: "continuous_on S f" and fim: "f ` S ⊆ affine hull T" and injf: "inj_on f S" shows "aff_dim S ≤ aff_dim T" proof (cases "S = {}") case True then show ?thesis by (simp add: aff_dim_geq) next case False have "aff_dim (affine hull S) ≤ aff_dim (affine hull T)" proof (rule invariance_of_dimension_affine_sets) show "openin (subtopology euclidean (affine hull S)) (rel_interior S)" by (simp add: openin_rel_interior) show "continuous_on (rel_interior S) f" using contf continuous_on_subset rel_interior_subset by blast show "f ` rel_interior S ⊆ affine hull T" using fim rel_interior_subset by blast show "inj_on f (rel_interior S)" using inj_on_subset injf rel_interior_subset by blast show "rel_interior S ≠ {}" by (simp add: False ‹convex S› rel_interior_eq_empty) qed auto then show ?thesis by simp qed lemma homeomorphic_convex_sets_le: assumes "convex S" "S homeomorphic T" shows "aff_dim S ≤ aff_dim T" proof - obtain h k where homhk: "homeomorphism S T h k" using homeomorphic_def assms by blast show ?thesis proof (rule invariance_of_dimension_convex_domain [OF ‹convex S›]) show "continuous_on S h" using homeomorphism_def homhk by blast show "h ` S ⊆ affine hull T" by (metis homeomorphism_def homhk hull_subset) show "inj_on h S" by (meson homeomorphism_apply1 homhk inj_on_inverseI) qed qed lemma homeomorphic_convex_sets: assumes "convex S" "convex T" "S homeomorphic T" shows "aff_dim S = aff_dim T" by (meson assms dual_order.antisym homeomorphic_convex_sets_le homeomorphic_sym) lemma homeomorphic_convex_compact_sets_eq: assumes "convex S" "compact S" "convex T" "compact T" shows "S homeomorphic T ⟷ aff_dim S = aff_dim T" by (meson assms homeomorphic_convex_compact_sets homeomorphic_convex_sets) lemma invariance_of_domain_gen: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "open S" "continuous_on S f" "inj_on f S" "DIM('b) ≤ DIM('a)" shows "open(f ` S)" using invariance_of_domain_subspaces [of UNIV S UNIV f] assms by auto lemma injective_into_1d_imp_open_map_UNIV: fixes f :: "'a::euclidean_space ⇒ real" assumes "open T" "continuous_on S f" "inj_on f S" "T ⊆ S" shows "open (f ` T)" apply (rule invariance_of_domain_gen [OF ‹open T›]) using assms apply (auto simp: elim: continuous_on_subset subset_inj_on) done lemma continuous_on_inverse_open: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "open S" "continuous_on S f" "DIM('b) ≤ DIM('a)" and gf: "⋀x. x ∈ S ⟹ g(f x) = x" shows "continuous_on (f ` S) g" proof (clarsimp simp add: continuous_openin_preimage_eq) fix T :: "'a set" assume "open T" have eq: "f ` S ∩ g -` T = f ` (S ∩ T)" by (auto simp: gf) show "openin (subtopology euclidean (f ` S)) (f ` S ∩ g -` T)" apply (subst eq) apply (rule open_openin_trans) apply (rule invariance_of_domain_gen) using assms apply auto using inj_on_inverseI apply auto[1] by (metis ‹open T› continuous_on_subset inj_onI inj_on_subset invariance_of_domain_gen openin_open openin_open_eq) qed lemma invariance_of_domain_homeomorphism: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "open S" "continuous_on S f" "DIM('b) ≤ DIM('a)" "inj_on f S" obtains g where "homeomorphism S (f ` S) f g" proof show "homeomorphism S (f ` S) f (inv_into S f)" by (simp add: assms continuous_on_inverse_open homeomorphism_def) qed corollary invariance_of_domain_homeomorphic: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "open S" "continuous_on S f" "DIM('b) ≤ DIM('a)" "inj_on f S" shows "S homeomorphic (f ` S)" using invariance_of_domain_homeomorphism [OF assms] by (meson homeomorphic_def) lemma continuous_image_subset_interior: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "continuous_on S f" "inj_on f S" "DIM('b) ≤ DIM('a)" shows "f ` (interior S) ⊆ interior(f ` S)" apply (rule interior_maximal) apply (simp add: image_mono interior_subset) apply (rule invariance_of_domain_gen) using assms apply (auto simp: subset_inj_on interior_subset continuous_on_subset) done lemma homeomorphic_interiors_same_dimension: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" and dimeq: "DIM('a) = DIM('b)" shows "(interior S) homeomorphic (interior T)" using assms [unfolded homeomorphic_minimal] unfolding homeomorphic_def proof (clarify elim!: ex_forward) fix f g assume S: "∀x∈S. f x ∈ T ∧ g (f x) = x" and T: "∀y∈T. g y ∈ S ∧ f (g y) = y" and contf: "continuous_on S f" and contg: "continuous_on T g" then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T" by (auto simp: inj_on_def intro: rev_image_eqI) metis+ have fim: "f ` interior S ⊆ interior T" using continuous_image_subset_interior [OF contf ‹inj_on f S›] dimeq fST by simp have gim: "g ` interior T ⊆ interior S" using continuous_image_subset_interior [OF contg ‹inj_on g T›] dimeq gTS by simp show "homeomorphism (interior S) (interior T) f g" unfolding homeomorphism_def proof (intro conjI ballI) show "⋀x. x ∈ interior S ⟹ g (f x) = x" by (meson ‹∀x∈S. f x ∈ T ∧ g (f x) = x› subsetD interior_subset) have "interior T ⊆ f ` interior S" proof fix x assume "x ∈ interior T" then have "g x ∈ interior S" using gim by blast then show "x ∈ f ` interior S" by (metis T ‹x ∈ interior T› image_iff interior_subset subsetCE) qed then show "f ` interior S = interior T" using fim by blast show "continuous_on (interior S) f" by (metis interior_subset continuous_on_subset contf) show "⋀y. y ∈ interior T ⟹ f (g y) = y" by (meson T subsetD interior_subset) have "interior S ⊆ g ` interior T" proof fix x assume "x ∈ interior S" then have "f x ∈ interior T" using fim by blast then show "x ∈ g ` interior T" by (metis S ‹x ∈ interior S› image_iff interior_subset subsetCE) qed then show "g ` interior T = interior S" using gim by blast show "continuous_on (interior T) g" by (metis interior_subset continuous_on_subset contg) qed qed lemma homeomorphic_open_imp_same_dimension: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" "open S" "S ≠ {}" "open T" "T ≠ {}" shows "DIM('a) = DIM('b)" using assms apply (simp add: homeomorphic_minimal) apply (rule order_antisym; metis inj_onI invariance_of_dimension) done lemma homeomorphic_interiors: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" "interior S = {} ⟷ interior T = {}" shows "(interior S) homeomorphic (interior T)" proof (cases "interior T = {}") case True with assms show ?thesis by auto next case False then have "DIM('a) = DIM('b)" using assms apply (simp add: homeomorphic_minimal) apply (rule order_antisym; metis continuous_on_subset inj_onI inj_on_subset interior_subset invariance_of_dimension open_interior) done then show ?thesis by (rule homeomorphic_interiors_same_dimension [OF ‹S homeomorphic T›]) qed lemma homeomorphic_frontiers_same_dimension: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" "closed S" "closed T" and dimeq: "DIM('a) = DIM('b)" shows "(frontier S) homeomorphic (frontier T)" using assms [unfolded homeomorphic_minimal] unfolding homeomorphic_def proof (clarify elim!: ex_forward) fix f g assume S: "∀x∈S. f x ∈ T ∧ g (f x) = x" and T: "∀y∈T. g y ∈ S ∧ f (g y) = y" and contf: "continuous_on S f" and contg: "continuous_on T g" then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T" by (auto simp: inj_on_def intro: rev_image_eqI) metis+ have "g ` interior T ⊆ interior S" using continuous_image_subset_interior [OF contg ‹inj_on g T›] dimeq gTS by simp then have fim: "f ` frontier S ⊆ frontier T" apply (simp add: frontier_def) using continuous_image_subset_interior assms(2) assms(3) S by auto have "f ` interior S ⊆ interior T" using continuous_image_subset_interior [OF contf ‹inj_on f S›] dimeq fST by simp then have gim: "g ` frontier T ⊆ frontier S" apply (simp add: frontier_def) using continuous_image_subset_interior T assms(2) assms(3) by auto show "homeomorphism (frontier S) (frontier T) f g" unfolding homeomorphism_def proof (intro conjI ballI) show gf: "⋀x. x ∈ frontier S ⟹ g (f x) = x" by (simp add: S assms(2) frontier_def) show fg: "⋀y. y ∈ frontier T ⟹ f (g y) = y" by (simp add: T assms(3) frontier_def) have "frontier T ⊆ f ` frontier S" proof fix x assume "x ∈ frontier T" then have "g x ∈ frontier S" using gim by blast then show "x ∈ f ` frontier S" by (metis fg ‹x ∈ frontier T› imageI) qed then show "f ` frontier S = frontier T" using fim by blast show "continuous_on (frontier S) f" by (metis Diff_subset assms(2) closure_eq contf continuous_on_subset frontier_def) have "frontier S ⊆ g ` frontier T" proof fix x assume "x ∈ frontier S" then have "f x ∈ frontier T" using fim by blast then show "x ∈ g ` frontier T" by (metis gf ‹x ∈ frontier S› imageI) qed then show "g ` frontier T = frontier S" using gim by blast show "continuous_on (frontier T) g" by (metis Diff_subset assms(3) closure_closed contg continuous_on_subset frontier_def) qed qed lemma homeomorphic_frontiers: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" "closed S" "closed T" "interior S = {} ⟷ interior T = {}" shows "(frontier S) homeomorphic (frontier T)" proof (cases "interior T = {}") case True then show ?thesis by (metis Diff_empty assms closure_eq frontier_def) next case False show ?thesis apply (rule homeomorphic_frontiers_same_dimension) apply (simp_all add: assms) using False assms homeomorphic_interiors homeomorphic_open_imp_same_dimension by blast qed lemma continuous_image_subset_rel_interior: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S ⊆ T" and TS: "aff_dim T ≤ aff_dim S" shows "f ` (rel_interior S) ⊆ rel_interior(f ` S)" proof (rule rel_interior_maximal) show "f ` rel_interior S ⊆ f ` S" by(simp add: image_mono rel_interior_subset) show "openin (subtopology euclidean (affine hull f ` S)) (f ` rel_interior S)" proof (rule invariance_of_domain_affine_sets) show "openin (subtopology euclidean (affine hull S)) (rel_interior S)" by (simp add: openin_rel_interior) show "aff_dim (affine hull f ` S) ≤ aff_dim (affine hull S)" by (metis aff_dim_affine_hull aff_dim_subset fim TS order_trans) show "f ` rel_interior S ⊆ affine hull f ` S" by (meson ‹f ` rel_interior S ⊆ f ` S› hull_subset order_trans) show "continuous_on (rel_interior S) f" using contf continuous_on_subset rel_interior_subset by blast show "inj_on f (rel_interior S)" using inj_on_subset injf rel_interior_subset by blast qed auto qed lemma homeomorphic_rel_interiors_same_dimension: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T" shows "(rel_interior S) homeomorphic (rel_interior T)" using assms [unfolded homeomorphic_minimal] unfolding homeomorphic_def proof (clarify elim!: ex_forward) fix f g assume S: "∀x∈S. f x ∈ T ∧ g (f x) = x" and T: "∀y∈T. g y ∈ S ∧ f (g y) = y" and contf: "continuous_on S f" and contg: "continuous_on T g" then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T" by (auto simp: inj_on_def intro: rev_image_eqI) metis+ have fim: "f ` rel_interior S ⊆ rel_interior T" by (metis ‹inj_on f S› aff contf continuous_image_subset_rel_interior fST order_refl) have gim: "g ` rel_interior T ⊆ rel_interior S" by (metis ‹inj_on g T› aff contg continuous_image_subset_rel_interior gTS order_refl) show "homeomorphism (rel_interior S) (rel_interior T) f g" unfolding homeomorphism_def proof (intro conjI ballI) show gf: "⋀x. x ∈ rel_interior S ⟹ g (f x) = x" using S rel_interior_subset by blast show fg: "⋀y. y ∈ rel_interior T ⟹ f (g y) = y" using T mem_rel_interior_ball by blast have "rel_interior T ⊆ f ` rel_interior S" proof fix x assume "x ∈ rel_interior T" then have "g x ∈ rel_interior S" using gim by blast then show "x ∈ f ` rel_interior S" by (metis fg ‹x ∈ rel_interior T› imageI) qed moreover have "f ` rel_interior S ⊆ rel_interior T" by (metis ‹inj_on f S› aff contf continuous_image_subset_rel_interior fST order_refl) ultimately show "f ` rel_interior S = rel_interior T" by blast show "continuous_on (rel_interior S) f" using contf continuous_on_subset rel_interior_subset by blast have "rel_interior S ⊆ g ` rel_interior T" proof fix x assume "x ∈ rel_interior S" then have "f x ∈ rel_interior T" using fim by blast then show "x ∈ g ` rel_interior T" by (metis gf ‹x ∈ rel_interior S› imageI) qed then show "g ` rel_interior T = rel_interior S" using gim by blast show "continuous_on (rel_interior T) g" using contg continuous_on_subset rel_interior_subset by blast qed qed lemma homeomorphic_rel_interiors: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" "rel_interior S = {} ⟷ rel_interior T = {}" shows "(rel_interior S) homeomorphic (rel_interior T)" proof (cases "rel_interior T = {}") case True with assms show ?thesis by auto next case False obtain f g where S: "∀x∈S. f x ∈ T ∧ g (f x) = x" and T: "∀y∈T. g y ∈ S ∧ f (g y) = y" and contf: "continuous_on S f" and contg: "continuous_on T g" using assms [unfolded homeomorphic_minimal] by auto have "aff_dim (affine hull S) ≤ aff_dim (affine hull T)" apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior S" _ f]) apply (simp_all add: openin_rel_interior False assms) using contf continuous_on_subset rel_interior_subset apply blast apply (meson S hull_subset image_subsetI rel_interior_subset rev_subsetD) apply (metis S inj_on_inverseI inj_on_subset rel_interior_subset) done moreover have "aff_dim (affine hull T) ≤ aff_dim (affine hull S)" apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior T" _ g]) apply (simp_all add: openin_rel_interior False assms) using contg continuous_on_subset rel_interior_subset apply blast apply (meson T hull_subset image_subsetI rel_interior_subset rev_subsetD) apply (metis T inj_on_inverseI inj_on_subset rel_interior_subset) done ultimately have "aff_dim S = aff_dim T" by force then show ?thesis by (rule homeomorphic_rel_interiors_same_dimension [OF ‹S homeomorphic T›]) qed lemma homeomorphic_rel_boundaries_same_dimension: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T" shows "(S - rel_interior S) homeomorphic (T - rel_interior T)" using assms [unfolded homeomorphic_minimal] unfolding homeomorphic_def proof (clarify elim!: ex_forward) fix f g assume S: "∀x∈S. f x ∈ T ∧ g (f x) = x" and T: "∀y∈T. g y ∈ S ∧ f (g y) = y" and contf: "continuous_on S f" and contg: "continuous_on T g" then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T" by (auto simp: inj_on_def intro: rev_image_eqI) metis+ have fim: "f ` rel_interior S ⊆ rel_interior T" by (metis ‹inj_on f S› aff contf continuous_image_subset_rel_interior fST order_refl) have gim: "g ` rel_interior T ⊆ rel_interior S" by (metis ‹inj_on g T› aff contg continuous_image_subset_rel_interior gTS order_refl) show "homeomorphism (S - rel_interior S) (T - rel_interior T) f g" unfolding homeomorphism_def proof (intro conjI ballI) show gf: "⋀x. x ∈ S - rel_interior S ⟹ g (f x) = x" using S rel_interior_subset by blast show fg: "⋀y. y ∈ T - rel_interior T ⟹ f (g y) = y" using T mem_rel_interior_ball by blast show "f ` (S - rel_interior S) = T - rel_interior T" using S fST fim gim by auto show "continuous_on (S - rel_interior S) f" using contf continuous_on_subset rel_interior_subset by blast show "g ` (T - rel_interior T) = S - rel_interior S" using T gTS gim fim by auto show "continuous_on (T - rel_interior T) g" using contg continuous_on_subset rel_interior_subset by blast qed qed lemma homeomorphic_rel_boundaries: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" "rel_interior S = {} ⟷ rel_interior T = {}" shows "(S - rel_interior S) homeomorphic (T - rel_interior T)" proof (cases "rel_interior T = {}") case True with assms show ?thesis by auto next case False obtain f g where S: "∀x∈S. f x ∈ T ∧ g (f x) = x" and T: "∀y∈T. g y ∈ S ∧ f (g y) = y" and contf: "continuous_on S f" and contg: "continuous_on T g" using assms [unfolded homeomorphic_minimal] by auto have "aff_dim (affine hull S) ≤ aff_dim (affine hull T)" apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior S" _ f]) apply (simp_all add: openin_rel_interior False assms) using contf continuous_on_subset rel_interior_subset apply blast apply (meson S hull_subset image_subsetI rel_interior_subset rev_subsetD) apply (metis S inj_on_inverseI inj_on_subset rel_interior_subset) done moreover have "aff_dim (affine hull T) ≤ aff_dim (affine hull S)" apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior T" _ g]) apply (simp_all add: openin_rel_interior False assms) using contg continuous_on_subset rel_interior_subset apply blast apply (meson T hull_subset image_subsetI rel_interior_subset rev_subsetD) apply (metis T inj_on_inverseI inj_on_subset rel_interior_subset) done ultimately have "aff_dim S = aff_dim T" by force then show ?thesis by (rule homeomorphic_rel_boundaries_same_dimension [OF ‹S homeomorphic T›]) qed proposition uniformly_continuous_homeomorphism_UNIV_trivial: fixes f :: "'a::euclidean_space ⇒ 'a" assumes contf: "uniformly_continuous_on S f" and hom: "homeomorphism S UNIV f g" shows "S = UNIV" proof (cases "S = {}") case True then show ?thesis by (metis UNIV_I hom empty_iff homeomorphism_def image_eqI) next case False have "inj g" by (metis UNIV_I hom homeomorphism_apply2 injI) then have "open (g ` UNIV)" by (blast intro: invariance_of_domain hom homeomorphism_cont2) then have "open S" using hom homeomorphism_image2 by blast moreover have "complete S" unfolding complete_def proof clarify fix σ assume σ: "∀n. σ n ∈ S" and "Cauchy σ" have "Cauchy (f o σ)" using uniformly_continuous_imp_Cauchy_continuous ‹Cauchy σ› σ contf by blast then obtain l where "(f ∘ σ) ⇢ l" by (auto simp: convergent_eq_Cauchy [symmetric]) show "∃l∈S. σ ⇢ l" proof show "g l ∈ S" using hom homeomorphism_image2 by blast have "(g ∘ (f ∘ σ)) ⇢ g l" by (meson UNIV_I ‹(f ∘ σ) ⇢ l› continuous_on_sequentially hom homeomorphism_cont2) then show "σ ⇢ g l" proof - have "∀n. σ n = (g ∘ (f ∘ σ)) n" by (metis (no_types) σ comp_eq_dest_lhs hom homeomorphism_apply1) then show ?thesis by (metis (no_types) LIMSEQ_iff ‹(g ∘ (f ∘ σ)) ⇢ g l›) qed qed qed then have "closed S" by (simp add: complete_eq_closed) ultimately show ?thesis using clopen [of S] False by simp qed subsection‹Dimension-based conditions for various homeomorphisms› lemma homeomorphic_subspaces_eq: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "subspace S" "subspace T" shows "S homeomorphic T ⟷ dim S = dim T" proof assume "S homeomorphic T" then obtain f g where hom: "homeomorphism S T f g" using homeomorphic_def by blast show "dim S = dim T" proof (rule order_antisym) show "dim S ≤ dim T" by (metis assms dual_order.refl inj_onI homeomorphism_cont1 [OF hom] homeomorphism_apply1 [OF hom] homeomorphism_image1 [OF hom] continuous_injective_image_subspace_dim_le) show "dim T ≤ dim S" by (metis assms dual_order.refl inj_onI homeomorphism_cont2 [OF hom] homeomorphism_apply2 [OF hom] homeomorphism_image2 [OF hom] continuous_injective_image_subspace_dim_le) qed next assume "dim S = dim T" then show "S homeomorphic T" by (simp add: assms homeomorphic_subspaces) qed lemma homeomorphic_affine_sets_eq: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "affine S" "affine T" shows "S homeomorphic T ⟷ aff_dim S = aff_dim T" proof (cases "S = {} ∨ T = {}") case True then show ?thesis using assms homeomorphic_affine_sets by force next case False then obtain a b where "a ∈ S" "b ∈ T" by blast then have "subspace ((+) (- a) ` S)" "subspace ((+) (- b) ` T)" using affine_diffs_subspace assms by blast+ then show ?thesis by (metis affine_imp_convex assms homeomorphic_affine_sets homeomorphic_convex_sets) qed lemma homeomorphic_hyperplanes_eq: fixes a :: "'a::euclidean_space" and c :: "'b::euclidean_space" assumes "a ≠ 0" "c ≠ 0" shows "({x. a ∙ x = b} homeomorphic {x. c ∙ x = d} ⟷ DIM('a) = DIM('b))" apply (auto simp: homeomorphic_affine_sets_eq affine_hyperplane assms) by (metis DIM_positive Suc_pred) lemma homeomorphic_UNIV_UNIV: shows "(UNIV::'a set) homeomorphic (UNIV::'b set) ⟷ DIM('a::euclidean_space) = DIM('b::euclidean_space)" by (simp add: homeomorphic_subspaces_eq) lemma simply_connected_sphere_gen: assumes "convex S" "bounded S" and 3: "3 ≤ aff_dim S" shows "simply_connected(rel_frontier S)" proof - have pa: "path_connected (rel_frontier S)" using assms by (simp add: path_connected_sphere_gen) show ?thesis proof (clarsimp simp add: simply_connected_eq_contractible_circlemap pa) fix f assume f: "continuous_on (sphere (0::complex) 1) f" "f ` sphere 0 1 ⊆ rel_frontier S" have eq: "sphere (0::complex) 1 = rel_frontier(cball 0 1)" by simp have "convex (cball (0::complex) 1)" by (rule convex_cball) then obtain c where "homotopic_with (λz. True) (sphere (0::complex) 1) (rel_frontier S) f (λx. c)" apply (rule inessential_spheremap_lowdim_gen [OF _ bounded_cball ‹convex S› ‹bounded S›, where f=f]) using f 3 apply (auto simp: aff_dim_cball) done then show "∃a. homotopic_with (λh. True) (sphere 0 1) (rel_frontier S) f (λx. a)" by blast qed qed subsection‹more invariance of domain› proposition invariance_of_domain_sphere_affine_set_gen: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S ⊆ T" and U: "bounded U" "convex U" and "affine T" and affTU: "aff_dim T < aff_dim U" and ope: "openin (subtopology euclidean (rel_frontier U)) S" shows "openin (subtopology euclidean T) (f ` S)" proof (cases "rel_frontier U = {}") case True then show ?thesis using ope openin_subset by force next case False obtain b c where b: "b ∈ rel_frontier U" and c: "c ∈ rel_frontier U" and "b ≠ c" using ‹bounded U› rel_frontier_not_sing [of U] subset_singletonD False by fastforce obtain V :: "'a set" where "affine V" and affV: "aff_dim V = aff_dim U - 1" proof (rule choose_affine_subset [OF affine_UNIV]) show "- 1 ≤ aff_dim U - 1" by (metis aff_dim_empty aff_dim_geq aff_dim_negative_iff affTU diff_0 diff_right_mono not_le) show "aff_dim U - 1 ≤ aff_dim (UNIV::'a set)" by (metis aff_dim_UNIV aff_dim_le_DIM le_cases not_le zle_diff1_eq) qed auto have SU: "S ⊆ rel_frontier U" using ope openin_imp_subset by auto have homb: "rel_frontier U - {b} homeomorphic V" and homc: "rel_frontier U - {c} homeomorphic V" using homeomorphic_punctured_sphere_affine_gen [of U _ V] by (simp_all add: ‹affine V› affV U b c) then obtain g h j k where gh: "homeomorphism (rel_frontier U - {b}) V g h" and jk: "homeomorphism (rel_frontier U - {c}) V j k" by (auto simp: homeomorphic_def) with SU have hgsub: "(h ` g ` (S - {b})) ⊆ S" and kjsub: "(k ` j ` (S - {c})) ⊆ S" by (simp_all add: homeomorphism_def subset_eq) have [simp]: "aff_dim T ≤ aff_dim V" by (simp add: affTU affV) have "openin (subtopology euclidean T) ((f ∘ h) ` g ` (S - {b}))" proof (rule invariance_of_domain_affine_sets [OF _ ‹affine V›]) show "openin (subtopology euclidean V) (g ` (S - {b}))" apply (rule homeomorphism_imp_open_map [OF gh]) by (meson Diff_mono Diff_subset SU ope openin_delete openin_subset_trans order_refl) show "continuous_on (g ` (S - {b})) (f ∘ h)" apply (rule continuous_on_compose) apply (meson Diff_mono SU homeomorphism_def homeomorphism_of_subsets gh set_eq_subset) using contf continuous_on_subset hgsub by blast show "inj_on (f ∘ h) (g ` (S - {b}))" using kjsub apply (clarsimp simp add: inj_on_def) by (metis SU b homeomorphism_def inj_onD injf insert_Diff insert_iff gh rev_subsetD) show "(f ∘ h) ` g ` (S - {b}) ⊆ T" by (metis fim image_comp image_mono hgsub subset_trans) qed (auto simp: assms) moreover have "openin (subtopology euclidean T) ((f ∘ k) ` j ` (S - {c}))" proof (rule invariance_of_domain_affine_sets [OF _ ‹affine V›]) show "openin (subtopology euclidean V) (j ` (S - {c}))" apply (rule homeomorphism_imp_open_map [OF jk]) by (meson Diff_mono Diff_subset SU ope openin_delete openin_subset_trans order_refl) show "continuous_on (j ` (S - {c})) (f ∘ k)" apply (rule continuous_on_compose) apply (meson Diff_mono SU homeomorphism_def homeomorphism_of_subsets jk set_eq_subset) using contf continuous_on_subset kjsub by blast show "inj_on (f ∘ k) (j ` (S - {c}))" using kjsub apply (clarsimp simp add: inj_on_def) by (metis SU c homeomorphism_def inj_onD injf insert_Diff insert_iff jk rev_subsetD) show "(f ∘ k) ` j ` (S - {c}) ⊆ T" by (metis fim image_comp image_mono kjsub subset_trans) qed (auto simp: assms) ultimately have "openin (subtopology euclidean T) ((f ∘ h) ` g ` (S - {b}) ∪ ((f ∘ k) ` j ` (S - {c})))" by (rule openin_Un) moreover have "(f ∘ h) ` g ` (S - {b}) = f ` (S - {b})" proof - have "h ` g ` (S - {b}) = (S - {b})" proof show "h ` g ` (S - {b}) ⊆ S - {b}" using homeomorphism_apply1 [OF gh] SU by (fastforce simp add: image_iff image_subset_iff) show "S - {b} ⊆ h ` g ` (S - {b})" apply clarify by (metis SU subsetD homeomorphism_apply1 [OF gh] image_iff member_remove remove_def) qed then show ?thesis by (metis image_comp) qed moreover have "(f ∘ k) ` j ` (S - {c}) = f ` (S - {c})" proof - have "k ` j ` (S - {c}) = (S - {c})" proof show "k ` j ` (S - {c}) ⊆ S - {c}" using homeomorphism_apply1 [OF jk] SU by (fastforce simp add: image_iff image_subset_iff) show "S - {c} ⊆ k ` j ` (S - {c})" apply clarify by (metis SU subsetD homeomorphism_apply1 [OF jk] image_iff member_remove remove_def) qed then show ?thesis by (metis image_comp) qed moreover have "f ` (S - {b}) ∪ f ` (S - {c}) = f ` (S)" using ‹b ≠ c› by blast ultimately show ?thesis by simp qed lemma invariance_of_domain_sphere_affine_set: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S ⊆ T" and "r ≠ 0" "affine T" and affTU: "aff_dim T < DIM('a)" and ope: "openin (subtopology euclidean (sphere a r)) S" shows "openin (subtopology euclidean T) (f ` S)" proof (cases "sphere a r = {}") case True then show ?thesis using ope openin_subset by force next case False show ?thesis proof (rule invariance_of_domain_sphere_affine_set_gen [OF contf injf fim bounded_cball convex_cball ‹affine T›]) show "aff_dim T < aff_dim (cball a r)" by (metis False affTU aff_dim_cball assms(4) linorder_cases sphere_empty) show "openin (subtopology euclidean (rel_frontier (cball a r))) S" by (simp add: ‹r ≠ 0› ope) qed qed lemma no_embedding_sphere_lowdim: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes contf: "continuous_on (sphere a r) f" and injf: "inj_on f (sphere a r)" and "r > 0" shows "DIM('a) ≤ DIM('b)" proof - have "False" if "DIM('a) > DIM('b)" proof - have "compact (f ` sphere a r)" using compact_continuous_image by (simp add: compact_continuous_image contf) then have "¬ open (f ` sphere a r)" using compact_open by (metis assms(3) image_is_empty not_less_iff_gr_or_eq sphere_eq_empty) then show False using invariance_of_domain_sphere_affine_set [OF contf injf subset_UNIV] ‹r > 0› by (metis aff_dim_UNIV affine_UNIV less_irrefl of_nat_less_iff open_openin openin_subtopology_self subtopology_UNIV that) qed then show ?thesis using not_less by blast qed lemma simply_connected_sphere: fixes a :: "'a::euclidean_space" assumes "3 ≤ DIM('a)" shows "simply_connected(sphere a r)" proof (cases rule: linorder_cases [of r 0]) case less then show ?thesis by simp next case equal then show ?thesis by (auto simp: convex_imp_simply_connected) next case greater then show ?thesis using simply_connected_sphere_gen [of "cball a r"] assms by (simp add: aff_dim_cball) qed lemma simply_connected_sphere_eq: fixes a :: "'a::euclidean_space" shows "simply_connected(sphere a r) ⟷ 3 ≤ DIM('a) ∨ r ≤ 0" (is "?lhs = ?rhs") proof (cases "r ≤ 0") case True have "simply_connected (sphere a r)" apply (rule convex_imp_simply_connected) using True less_eq_real_def by auto with True show ?thesis by auto next case False show ?thesis proof assume L: ?lhs have "False" if "DIM('a) = 1 ∨ DIM('a) = 2" using that proof assume "DIM('a) = 1" with L show False using connected_sphere_eq simply_connected_imp_connected by (metis False Suc_1 not_less_eq_eq order_refl) next assume "DIM('a) = 2" then have "sphere a r homeomorphic sphere (0::complex) 1" by (metis DIM_complex False homeomorphic_spheres_gen not_less zero_less_one) then have "simply_connected(sphere (0::complex) 1)" using L homeomorphic_simply_connected_eq by blast then obtain a::complex where "homotopic_with (λh. True) (sphere 0 1) (sphere 0 1) id (λx. a)" apply (simp add: simply_connected_eq_contractible_circlemap) by (metis continuous_on_id' id_apply image_id subset_refl) then show False using contractible_sphere contractible_def not_one_le_zero by blast qed with False show ?rhs apply simp by (metis DIM_ge_Suc0 le_antisym not_less_eq_eq numeral_2_eq_2 numeral_3_eq_3) next assume ?rhs with False show ?lhs by (simp add: simply_connected_sphere) qed qed lemma simply_connected_punctured_universe_eq: fixes a :: "'a::euclidean_space" shows "simply_connected(- {a}) ⟷ 3 ≤ DIM('a)" proof - have [simp]: "a ∈ rel_interior (cball a 1)" by (simp add: rel_interior_nonempty_interior) have [simp]: "affine hull cball a 1 - {a} = -{a}" by (metis Compl_eq_Diff_UNIV aff_dim_cball aff_dim_lt_full not_less_iff_gr_or_eq zero_less_one) have "simply_connected(- {a}) ⟷ simply_connected(sphere a 1)" apply (rule sym) apply (rule homotopy_eqv_simple_connectedness) using homotopy_eqv_rel_frontier_punctured_affine_hull [of "cball a 1" a] apply auto done also have "... ⟷ 3 ≤ DIM('a)" by (simp add: simply_connected_sphere_eq) finally show ?thesis . qed lemma not_simply_connected_circle: fixes a :: complex shows "0 < r ⟹ ¬ simply_connected(sphere a r)" by (simp add: simply_connected_sphere_eq) proposition simply_connected_punctured_convex: fixes a :: "'a::euclidean_space" assumes "convex S" and 3: "3 ≤ aff_dim S" shows "simply_connected(S - {a})" proof (cases "a ∈ rel_interior S") case True then obtain e where "a ∈ S" "0 < e" and e: "cball a e ∩ affine hull S ⊆ S" by (auto simp: rel_interior_cball) have con: "convex (cball a e ∩ affine hull S)" by (simp add: convex_Int) have bo: "bounded (cball a e ∩ affine hull S)" by (simp add: bounded_Int) have "affine hull S ∩ interior (cball a e) ≠ {}" using ‹0 < e› ‹a ∈ S› hull_subset by fastforce then have "3 ≤ aff_dim (affine hull S ∩ cball a e)" by (simp add: 3 aff_dim_convex_Int_nonempty_interior [OF convex_affine_hull]) also have "... = aff_dim (cball a e ∩ affine hull S)" by (simp add: Int_commute) finally have "3 ≤ aff_dim (cball a e ∩ affine hull S)" . moreover have "rel_frontier (cball a e ∩ affine hull S) homotopy_eqv S - {a}" proof (rule homotopy_eqv_rel_frontier_punctured_convex) show "a ∈ rel_interior (cball a e ∩ affine hull S)" by (meson IntI Int_mono ‹a ∈ S› ‹0 < e› e ‹cball a e ∩ affine hull S ⊆ S› ball_subset_cball centre_in_cball dual_order.strict_implies_order hull_inc hull_mono mem_rel_interior_ball) have "closed (cball a e ∩ affine hull S)" by blast then show "rel_frontier (cball a e ∩ affine hull S) ⊆ S" apply (simp add: rel_frontier_def) using e by blast show "S ⊆ affine hull (cball a e ∩ affine hull S)" by (metis (no_types, lifting) IntI ‹a ∈ S› ‹0 < e› affine_hull_convex_Int_nonempty_interior centre_in_ball convex_affine_hull empty_iff hull_subset inf_commute interior_cball subsetCE subsetI) qed (auto simp: assms con bo) ultimately show ?thesis using homotopy_eqv_simple_connectedness simply_connected_sphere_gen [OF con bo] by blast next case False show ?thesis apply (rule contractible_imp_simply_connected) apply (rule contractible_convex_tweak_boundary_points [OF ‹convex S›]) apply (simp add: False rel_interior_subset subset_Diff_insert) by (meson Diff_subset closure_subset subset_trans) qed corollary simply_connected_punctured_universe: fixes a :: "'a::euclidean_space" assumes "3 ≤ DIM('a)" shows "simply_connected(- {a})" proof - have [simp]: "affine hull cball a 1 = UNIV" apply auto by (metis UNIV_I aff_dim_cball aff_dim_lt_full zero_less_one not_less_iff_gr_or_eq) have "simply_connected (rel_frontier (cball a 1)) = simply_connected (affine hull cball a 1 - {a})" apply (rule homotopy_eqv_simple_connectedness) apply (rule homotopy_eqv_rel_frontier_punctured_affine_hull) apply (force simp: rel_interior_cball intro: homotopy_eqv_simple_connectedness homotopy_eqv_rel_frontier_punctured_affine_hull)+ done then show ?thesis using simply_connected_sphere [of a 1, OF assms] by (auto simp: Compl_eq_Diff_UNIV) qed subsection‹The power, squaring and exponential functions as covering maps› proposition covering_space_power_punctured_plane: assumes "0 < n" shows "covering_space (- {0}) (λz::complex. z^n) (- {0})" proof - consider "n = 1" | "2 ≤ n" using assms by linarith then obtain e where "0 < e" and e: "⋀w z. cmod(w - z) < e * cmod z ⟹ (w^n = z^n ⟷ w = z)" proof cases assume "n = 1" then show ?thesis by (rule_tac e=1 in that) auto next assume "2 ≤ n" have eq_if_pow_eq: "w = z" if lt: "cmod (w - z) < 2 * sin (pi / real n) * cmod z" and eq: "w^n = z^n" for w z proof (cases "z = 0") case True with eq assms show ?thesis by (auto simp: power_0_left) next case False then have "z ≠ 0" by auto have "(w/z)^n = 1" by (metis False divide_self_if eq power_divide power_one) then obtain j where j: "w / z = exp (2 * of_real pi * 𝗂 * j / n)" and "j < n" using Suc_leI assms ‹2 ≤ n› complex_roots_unity [THEN eqset_imp_iff, of n "w/z"] by force have "cmod (w/z - 1) < 2 * sin (pi / real n)" using lt assms ‹z ≠ 0› by (simp add: divide_simps norm_divide) then have "cmod (exp (𝗂 * of_real (2 * pi * j / n)) - 1) < 2 * sin (pi / real n)" by (simp add: j field_simps) then have "2 * ¦sin((2 * pi * j / n) / 2)¦ < 2 * sin (pi / real n)" by (simp only: dist_exp_i_1) then have sin_less: "sin((pi * j / n)) < sin (pi / real n)" by (simp add: field_simps) then have "w / z = 1" proof (cases "j = 0") case True then show ?thesis by (auto simp: j) next case False then have "sin (pi / real n) ≤ sin((pi * j / n))" proof (cases "j / n ≤ 1/2") case True show ?thesis apply (rule sin_monotone_2pi_le) using ‹j ≠ 0 › ‹j < n› True apply (auto simp: field_simps intro: order_trans [of _ 0]) done next case False then have seq: "sin(pi * j / n) = sin(pi * (n - j) / n)" using ‹j < n› by (simp add: algebra_simps diff_divide_distrib of_nat_diff) show ?thesis apply (simp only: seq) apply (rule sin_monotone_2pi_le) using ‹j < n› False apply (auto simp: field_simps intro: order_trans [of _ 0]) done qed with sin_less show ?thesis by force qed then show ?thesis by simp qed show ?thesis apply (rule_tac e = "2 * sin(pi / n)" in that) apply (force simp: ‹2 ≤ n› sin_pi_divide_n_gt_0) apply (meson eq_if_pow_eq) done qed have zn1: "continuous_on (- {0}) (λz::complex. z^n)" by (rule continuous_intros)+ have zn2: "(λz::complex. z^n) ` (- {0}) = - {0}" using assms by (auto simp: image_def elim: exists_complex_root_nonzero [where n = n]) have zn3: "∃T. z^n ∈ T ∧ open T ∧ 0 ∉ T ∧ (∃v. ⋃v = -{0} ∩ (λz. z ^ n) -` T ∧ (∀u∈v. open u ∧ 0 ∉ u) ∧ pairwise disjnt v ∧ (∀u∈v. Ex (homeomorphism u T (λz. z^n))))" if "z ≠ 0" for z::complex proof - define d where "d ≡ min (1/2) (e/4) * norm z" have "0 < d" by (simp add: d_def ‹0 < e› ‹z ≠ 0›) have iff_x_eq_y: "x^n = y^n ⟷ x = y" if eq: "w^n = z^n" and x: "x ∈ ball w d" and y: "y ∈ ball w d" for w x y proof - have [simp]: "norm z = norm w" using that by (simp add: assms power_eq_imp_eq_norm) show ?thesis proof (cases "w = 0") case True with ‹z ≠ 0› assms eq show ?thesis by (auto simp: power_0_left) next case False have "cmod (x - y) < 2*d" using x y by (simp add: dist_norm [symmetric]) (metis dist_commute mult_2 dist_triangle_less_add) also have "... ≤ 2 * e / 4 * norm w" using ‹e > 0› by (simp add: d_def min_mult_distrib_right) also have "... = e * (cmod w / 2)" by simp also have "... ≤ e * cmod y" apply (rule mult_left_mono) using ‹e > 0› y apply (simp_all add: dist_norm d_def min_mult_distrib_right del: divide_const_simps) apply (metis dist_0_norm dist_complex_def dist_triangle_half_l linorder_not_less order_less_irrefl) done finally have "cmod (x - y) < e * cmod y" . then show ?thesis by (rule e) qed qed then have inj: "inj_on (λw. w^n) (ball z d)" by (simp add: inj_on_def) have cont: "continuous_on (ball z d) (λw. w ^ n)" by (intro continuous_intros) have noncon: "¬ (λw::complex. w^n) constant_on UNIV" by (metis UNIV_I assms constant_on_def power_one zero_neq_one zero_power) have im_eq: "(λw. w^n) ` ball z' d = (λw. w^n) ` ball z d" if z': "z'^n = z^n" for z' proof - have nz': "norm z' = norm z" using that assms power_eq_imp_eq_norm by blast have "(w ∈ (λw. w^n) ` ball z' d) = (w ∈ (λw. w^n) ` ball z d)" for w proof (cases "w=0") case True with assms show ?thesis by (simp add: image_def ball_def nz') next case False have "z' ≠ 0" using ‹z ≠ 0› nz' by force have [simp]: "(z*x / z')^n = x^n" if "x ≠ 0" for x using z' that by (simp add: field_simps ‹z ≠ 0›) have [simp]: "cmod (z - z * x / z') = cmod (z' - x)" if "x ≠ 0" for x proof - have "cmod (z - z * x / z') = cmod z * cmod (1 - x / z')" by (metis (no_types) ab_semigroup_mult_class.mult_ac(1) divide_complex_def mult.right_neutral norm_mult right_diff_distrib') also have "... = cmod z' * cmod (1 - x / z')" by (simp add: nz') also have "... = cmod (z' - x)" by (simp add: ‹z' ≠ 0› diff_divide_eq_iff norm_divide) finally show ?thesis . qed have [simp]: "(z'*x / z)^n = x^n" if "x ≠ 0" for x using z' that by (simp add: field_simps ‹z ≠ 0›) have [simp]: "cmod (z' - z' * x / z) = cmod (z - x)" if "x ≠ 0" for x proof - have "cmod (z * (1 - x * inverse z)) = cmod (z - x)" by (metis ‹z ≠ 0› diff_divide_distrib divide_complex_def divide_self_if nonzero_eq_divide_eq semiring_normalization_rules(7)) then show ?thesis by (metis (no_types) mult.assoc divide_complex_def mult.right_neutral norm_mult nz' right_diff_distrib') qed show ?thesis unfolding image_def ball_def apply safe apply simp_all apply (rule_tac x="z/z' * x" in exI) using assms False apply (simp add: dist_norm) apply (rule_tac x="z'/z * x" in exI) using assms False apply (simp add: dist_norm) done qed then show ?thesis by blast qed have ex_ball: "∃B. (∃z'. B = ball z' d ∧ z'^n = z^n) ∧ x ∈ B" if "x ≠ 0" and eq: "x^n = w^n" and dzw: "dist z w < d" for x w proof - have "w ≠ 0" by (metis assms power_eq_0_iff that(1) that(2)) have [simp]: "cmod x = cmod w" using assms power_eq_imp_eq_norm eq by blast have [simp]: "cmod (x * z / w - x) = cmod (z - w)" proof - have "cmod (x * z / w - x) = cmod x * cmod (z / w - 1)" by (metis (no_types) mult.right_neutral norm_mult right_diff_distrib' times_divide_eq_right) also have "... = cmod w * cmod (z / w - 1)" by simp also have "... = cmod (z - w)" by (simp add: ‹w ≠ 0› divide_diff_eq_iff nonzero_norm_divide) finally show ?thesis . qed show ?thesis apply (rule_tac x="ball (z / w * x) d" in exI) using ‹d > 0› that apply (simp add: ball_eq_ball_iff) apply (simp add: ‹z ≠ 0› ‹w ≠ 0› field_simps) apply (simp add: dist_norm) done qed show ?thesis proof (rule exI, intro conjI) show "z ^ n ∈ (λw. w ^ n) ` ball z d" using ‹d > 0› by simp show "open ((λw. w ^ n) ` ball z d)" by (rule invariance_of_domain [OF cont open_ball inj]) show "0 ∉ (λw. w ^ n) ` ball z d" using ‹z ≠ 0› assms by (force simp: d_def) show "∃v. ⋃v = - {0} ∩ (λz. z ^ n) -` (λw. w ^ n) ` ball z d ∧ (∀u∈v. open u ∧ 0 ∉ u) ∧ disjoint v ∧ (∀u∈v. Ex (homeomorphism u ((λw. w ^ n) ` ball z d) (λz. z ^ n)))" proof (rule exI, intro ballI conjI) show "⋃{ball z' d |z'. z'^n = z^n} = - {0} ∩ (λz. z ^ n) -` (λw. w ^ n) ` ball z d" (is "?l = ?r") proof show "?l ⊆ ?r" apply auto apply (simp add: assms d_def power_eq_imp_eq_norm that) by (metis im_eq image_eqI mem_ball) show "?r ⊆ ?l" by auto (meson ex_ball) qed show "⋀u. u ∈ {ball z' d |z'. z' ^ n = z ^ n} ⟹ 0 ∉ u" by (force simp add: assms d_def power_eq_imp_eq_norm that) show "disjoint {ball z' d |z'. z' ^ n = z ^ n}" proof (clarsimp simp add: pairwise_def disjnt_iff) fix ξ ζ x assume "ξ^n = z^n" "ζ^n = z^n" "ball ξ d ≠ ball ζ d" and "dist ξ x < d" "dist ζ x < d" then have "dist ξ ζ < d+d" using dist_triangle_less_add by blast then have "cmod (ξ - ζ) < 2*d" by (simp add: dist_norm) also have "... ≤ e * cmod z" using mult_right_mono ‹0 < e› that by (auto simp: d_def) finally have "cmod (ξ - ζ) < e * cmod z" . with e have "ξ = ζ" by (metis ‹ξ^n = z^n› ‹ζ^n = z^n› assms power_eq_imp_eq_norm) then show "False" using ‹ball ξ d ≠ ball ζ d› by blast qed show "Ex (homeomorphism u ((λw. w ^ n) ` ball z d) (λz. z ^ n))" if "u ∈ {ball z' d |z'. z' ^ n = z ^ n}" for u proof (rule invariance_of_domain_homeomorphism [of "u" "λz. z^n"]) show "open u" using that by auto show "continuous_on u (λz. z ^ n)" by (intro continuous_intros) show "inj_on (λz. z ^ n) u" using that by (auto simp: iff_x_eq_y inj_on_def) show "⋀g. homeomorphism u ((λz. z ^ n) ` u) (λz. z ^ n) g ⟹ Ex (homeomorphism u ((λw. w ^ n) ` ball z d) (λz. z ^ n))" using im_eq that by clarify metis qed auto qed auto qed qed show ?thesis using assms apply (simp add: covering_space_def zn1 zn2) apply (subst zn2 [symmetric]) apply (simp add: openin_open_eq open_Compl) apply (blast intro: zn3) done qed corollary covering_space_square_punctured_plane: "covering_space (- {0}) (λz::complex. z^2) (- {0})" by (simp add: covering_space_power_punctured_plane) proposition covering_space_exp_punctured_plane: "covering_space UNIV (λz::complex. exp z) (- {0})" proof (simp add: covering_space_def, intro conjI ballI) show "continuous_on UNIV (λz::complex. exp z)" by (rule continuous_on_exp [OF continuous_on_id]) show "range exp = - {0::complex}" by auto (metis exp_Ln range_eqI) show "∃T. z ∈ T ∧ openin (subtopology euclidean (- {0})) T ∧ (∃v. ⋃v = exp -` T ∧ (∀u∈v. open u) ∧ disjoint v ∧ (∀u∈v. ∃q. homeomorphism u T exp q))" if "z ∈ - {0::complex}" for z proof - have "z ≠ 0" using that by auto have inj_exp: "inj_on exp (ball (Ln z) 1)" apply (rule inj_on_subset [OF inj_on_exp_pi [of "Ln z"]]) using pi_ge_two by (simp add: ball_subset_ball_iff) define 𝒱 where "𝒱 ≡ range (λn. (λx. x + of_real (2 * of_int n * pi) * 𝗂) ` (ball(Ln z) 1))" show ?thesis proof (intro exI conjI) show "z ∈ exp ` (ball(Ln z) 1)" by (metis ‹z ≠ 0› centre_in_ball exp_Ln rev_image_eqI zero_less_one) have "open (- {0::complex})" by blast moreover have "inj_on exp (ball (Ln z) 1)" apply (rule inj_on_subset [OF inj_on_exp_pi [of "Ln z"]]) using pi_ge_two by (simp add: ball_subset_ball_iff) <