section ‹Extending Continous Maps, Invariance of Domain, etc› (*FIX rename? *) text‹Ported from HOL Light (moretop.ml) by L C Paulson› theory Further_Topology imports Weierstrass_Theorems Polytope Complex_Transcendental Equivalence_Lebesgue_Henstock_Integration Retracts 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 "⋀u. ⟦u ∈ S; norm u *⇩_{R}f (u /⇩_{R}norm u) ∉ T⟧ ⟹ u = 0" by (metis (mono_tags, lifting) DiffI subS01 subspace_mul [OF ‹subspace T›] fim image_subset_iff inf_le2 singletonD) then have "g ` (S - {0}) ⊆ T" using g_def by blast 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 obtain u where u: "f u ∈ T" "x /⇩_{R}norm x = f u" "norm u = 1" "u ∈ S" using * [THEN subsetD, of "x /⇩_{R}norm x"] ‹x ≠ 0› by auto with that have [simp]: "norm x *⇩_{R}f u = x" by (metis divideR_right norm_eq_zero) moreover have "norm x *⇩_{R}u ∈ S - {0}" using ‹subspace S› subspace_scale that(2) u by auto with u show ?thesis by (simp add: image_eqI [where x="norm x *⇩_{R}u"]) 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 "g differentiable_on p1 ` {x + y |x y. x ∈ S - {0} ∧ y ∈ T'}" using p12_eq ‹S ⊆ T› by (force intro: differentiable_on_subset [OF gdiff]) then have "(λz. g (p1 z)) differentiable_on {x + y |x y. x ∈ S - {0} ∧ y ∈ T'}" by (rule differentiable_on_compose [OF linear_imp_differentiable_on [OF ‹linear p1›]]) 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 using ‹S ⊆ T› p12_eq by (rule_tac x="s + t'" in image_eqI) 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'" by (metis Diff_iff ‹z ∉ T'› add.left_neutral eq geq p1 p2 singletonD) 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_canon (λ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" using Stone_Weierstrass_polynomial_function_subspace [OF _ contf _ ‹subspace T›, of "1/2"] fim by auto 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 using gnz by (fastforce intro: derivative_intros diffg differentiable_on_compose [OF diffg]) have homfg: "homotopic_with_canon (λ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" using g12 that by auto ultimately show ?thesis by (auto simp: norm_minus_commute dest: segment_bound) qed show "closed_segment (f x) (g x) ⊆ T - {0}" if "x ∈ sphere 0 1 ∩ S" for x proof - have "convex T" by (simp add: ‹subspace T› subspace_imp_convex) then have "convex hull {f x, g x} ⊆ T" by (metis IntD2 closed_segment_subset fim gim image_subset_iff segment_convex_hull that) then show ?thesis using that non0fg segment_convex_hull by fastforce qed 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_canon (λz. True) (sphere 0 1 ∩ S) (T - {0}) h (λx. -d)" proof (rule homotopic_with_linear [OF conth continuous_on_const]) fix x assume x: "x ∈ sphere 0 1 ∩ S" have "convex hull {h x, - d} ⊆ T" proof (rule hull_minimal) show "{h x, - d} ⊆ T" using h d x by (force simp: subspace_neg [OF ‹subspace T›]) qed (simp add: subspace_imp_convex [OF ‹subspace T›]) with x segment_convex_hull show "closed_segment (h x) (- d) ⊆ T - {0}" by (auto simp add: subset_Diff_insert non0hd) qed 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_canon (λz. True) (sphere 0 1 ∩ S) (sphere 0 1 ∩ T) h (λx. c)" proof show "homotopic_with_canon (λz. True) (sphere 0 1 ∩ S) (sphere 0 1 ∩ T) h (λx. - d)" using d by (force simp: h_def intro: homotopic_with_eq homotopic_with_compose_continuous_left [OF hom_hd conT0 sub0T]) qed have "homotopic_with_canon (λx. True) (sphere 0 1 ∩ S) (sphere 0 1 ∩ T) f h" by (force simp: h_def intro: homotopic_with_eq homotopic_with_compose_continuous_left [OF homfg conT0 sub0T]) then show ?thesis by (metis homotopic_with_trans [OF _ homhc]) 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)" proof (rule homeomorphic_rel_frontiers_convex_bounded_sets [OF ‹convex S› ‹bounded S›]) show "convex (ball 0 1 ∩ T)" by (simp add: ‹subspace T› convex_Int subspace_imp_convex) show "bounded (ball 0 1 ∩ T)" by (simp add: bounded_Int) show "aff_dim S = aff_dim (ball 0 1 ∩ T)" by (rule affS_eq) qed also have "... = frontier (ball 0 1) ∩ T" proof (rule convex_affine_rel_frontier_Int [OF convex_ball]) show "affine T" by (simp add: ‹subspace T› subspace_imp_affine) show "interior (ball 0 1) ∩ T ≠ {}" using ‹subspace T› subspace_0 by force qed 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_canon (λz. True) (rel_frontier S) (rel_frontier T) f (λx. c)" proof (cases "S = {}") case True then show ?thesis using homotopic_with_canon_on_empty that by auto next case False then show ?thesis proof (cases "T = {}") case True then have "rel_frontier S = {}" "rel_frontier T = {}" using fim by fastforce+ then show ?thesis using that by (simp add: homotopic_on_emptyI) 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'" using ‹T ≠ {}› spheremap_lemma3 [OF ‹bounded T› ‹convex T› subspace_UNIV, where 'b='a] by (force simp add: aff_dim_le_DIM) with homeomorphic_imp_homotopy_eqv have relT: "sphere 0 1 ∩ T' homotopy_eqv rel_frontier T" using homotopy_equivalent_space_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_equivalent_space_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_canon (λz. True) (rel_frontier S) (rel_frontier T) f (λx. c)" using spheremap_lemma2 homotopy_eqv_cohomotopic_triviality_null[OF relS] using homotopy_eqv_homotopic_triviality_null_imp [OF relT contf fim] by (metis ‹S' ⊆ T'› ‹subspace S'› ‹subspace T'› dimST' image_subset_iff_funcset) 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_canon (λ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 using inessential_spheremap_lowdim_gen [of "cball a r" "cball b s" f] using ‹0 < r› ‹0 < s› assms(1) that by (auto simp add: f aff_dim_cball) 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 moreover have "continuous_on (S ∪ ⋃ ℱ) (λx. if x ∈ S then f x else g x)" by (auto simp: insert closed_Union contf contg intro: fg continuous_on_cases) ultimately show ?case by (smt (verit, del_insts) Int_iff UnE complete_lattice_class.Sup_insert feq fim geq gim image_subset_iff) 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 flip: Union_maximal_sets [OF fin]) 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" 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 show ?thesis proof show "continuous_on (⋃ ℱ) f" using True ‹𝒢 ⊆ ℱ› contf by auto show "f ` ⋃ ℱ ⊆ rel_frontier T" using True fim by auto qed auto 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 face': "⋀S T. ⟦S ∈ ℱ; T ∈ ℱ⟧ ⟹ (S ∩ T) face_of S ∧ (S ∩ T) face_of T" by (metis face inf_commute) 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 show ?case using 0 contf fim by (auto simp add: Union_empty_eq) 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 have "continuous_on D h" using True conth continuous_on_subset by blast moreover have "h ` D ⊆ rel_frontier T" using True him by blast ultimately show ?thesis by blast 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}" by clarify (metis ‹D face_of C› affD eq_iff face_of_trans facet_of_def zle_diff1_eq) 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_canon (λ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))" by (simp add: assms image_subset_iff_funcset rel_frontier_eq_empty him_relf nullhomotopic_into_rel_frontier_extension [OF closed_rel_frontier]) have "∃c. homotopic_with_canon (λ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 proof safe assume "E ∈ 𝒢" then show "D ∩ E face_of D" by (meson ‹C ∈ ℱ› ‹D face_of C› assms(2) face' face_of_Int_subface face_of_refl_eq poly polytope_imp_convex subsetD) next fix x assume "aff_dim E < int p" "x ∈ ℱ" "E face_of x" then show "D ∩ E face_of D" by (meson ‹C ∈ ℱ› ‹D face_of C› face' face_of_Int_subface that) qed show "D ∩ E ≠ D" using that notDsub by auto qed moreover have "continuous_on D g" using contg continuous_on_subset by blast ultimately show ?thesis by (rule_tac x=g in exI) (use gh gim in 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 moreover have "finite (?Faces)" proof - have §: "finite (⋃ {{D. D face_of C} |C. C ∈ ℱ})" by (auto simp: ‹finite ℱ› finite_polytope_faces poly) show ?thesis by (auto intro: finite_subset [OF _ §]) qed ultimately have fin: "finite (𝒢 ∪ ?Faces)" by simp 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 by (rule face_of_Int_subface [OF _ _ XY]) (auto simp: face' DE) show ?thesis using that apply clarsimp by (smt (verit, ccfv_SIG) IntI face_of_aff_dim_lt face_of_imp_convex [of X] face_of_imp_convex [of Y] 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)" by (rule exE [OF extending_maps_Union [OF fin extendh clo K]], blast+) then show ?case by (simp add: intle local.heq [symmetric], blast) 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}) ⊆ ⋃ℱ" using ‹𝒢 ⊆ ℱ› face_of_imp_subset by fastforce show "⋃ℱ ⊆ ⋃(𝒢 ∪ {D. ∃C∈ℱ. D face_of C ∧ aff_dim D < i})" proof (rule Union_mono) show "ℱ ⊆ 𝒢 ∪ {D. ∃C∈ℱ. D face_of C ∧ aff_dim D < int i}" using face by (fastforce simp: aff i) qed 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) f" using contf by (force simp: elim: continuous_on_subset) moreover have "continuous_on (⋃ ℱ - insert a C) g" using contg by (force simp: elim: continuous_on_subset) ultimately have "continuous_on (X - insert a C ∪ (⋃ℱ - insert a C)) (λx. if x ∈ X then f x else g x)" apply (intro continuous_on_cases_local; simp add: closedin_closed) using ‹closed X› apply blast using ‹closed (⋃ℱ)› apply blast 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)" using extend_map_lemma_cofinite0 [OF fin pw, of U T h] by (fastforce intro!: clo ℱ) 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" 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 have *: "finite (⋃{{D. D face_of C} |C. C ∈ ℱ})" using finite_polytope_faces poly ‹finite ℱ› by force then have "finite ℋ" by (auto simp: ℋ_def ‹finite 𝒢› intro: finite_subset [OF _ *]) have face': "⋀S T. ⟦S ∈ ℱ; T ∈ ℱ⟧ ⟹ (S ∩ T) face_of S ∧ (S ∩ T) face_of T" by (metis face inf_commute) have *: "⋀X Y. ⟦X ∈ ℋ; Y ∈ ℋ⟧ ⟹ X ∩ Y face_of X" by (simp add: ℋ_def) (smt (verit) ‹𝒢 ⊆ ℱ› DiffE face' face_of_Int_subface in_mono inf.idem) obtain h where conth: "continuous_on (⋃ℋ) h" and him: "h ` (⋃ℋ) ⊆ rel_frontier T" and hf: "⋀x. x ∈ ⋃𝒢 ⟹ h x = f x" proof (rule extend_map_lemma [OF ‹finite ℋ› [unfolded ℋ_def] Un_upper1 T]) show "⋀X. ⟦X ∈ 𝒢 ∪ {D. ∃C∈ℱ - 𝒢. D face_of C ∧ aff_dim D < aff_dim T}⟧ ⟹ polytope X" using ‹𝒢 ⊆ ℱ› face_of_polytope_polytope poly by fastforce qed (use * ℋ_def contf fim in auto) 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 have "h ` (D - {a}) ⊆ rel_frontier T" "continuous_on (D - {a}) h" using him by (blast intro!: ‹a ∉ ⋃𝒢› continuous_on_subset [OF conth])+ then show ?thesis using a by blast 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)" proof (rule continuous_on_compose) show "continuous_on (D - {b}) r" by (meson Diff_mono continuous_on_subset contr hull_subset order_refl) show "continuous_on (r ` (D - {b})) h" by (simp add: Diff_mono hull_subset continuous_on_subset [OF conth rsub]) qed 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]) have "D face_of D" by (simp add: ‹polyhedron D› polyhedron_imp_convex face_of_refl) then show "D ∩ A face_of D" by (meson "2"(2) "2"(3) ‹D ∈ ℱ› face' face_of_Int_Int face_of_face) 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 by (rule_tac C=C and g=g in that) (auto simp: disjnt_def hf [symmetric] ℋ_def intro!: gh) 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" 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" 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" using ‹X ∈ 𝒢› ‹X ⊆ V› ‹x ∈ X› hg by auto 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" 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" 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" using Ssub hg 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› 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" 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" by (subst convex_affine_rel_frontier_Int [OF _ ‹affine T› int_ne]) (auto simp: fro_def c_def) 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))" proof (rule continuous_on_closest_point) show "convex (cbox (- c) c ∩ T)" by (simp add: affine_imp_convex convex_Int ‹affine T›) show "closed (cbox (- c) c ∩ T)" using clo_cbT by blast show "cbox (- c) c ∩ T ≠ {}" using ‹S ≠ {}› cbsub(2) b that by auto qed 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" by blast 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 (top_of_set 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 DiffD1 Diff_empty Diff_subset PiE Pi_I contf continuous_on_subset fim 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 (top_of_set U) C" by (m