Quelle Further_Topology.thy Sprache: Isabelle

section \<open>Extending Continous Maps, Invariance of Domain, etc\<close> (*FIX rename? *)

text\<open>Ported from HOL Light (moretop.ml) by L C Paulson\<close>

theory Further_Topology
  imports Weierstrass_Theorems Polytope Complex_Transcendental Equivalence_Lebesgue_Henstock_Integration Retracts
begin

subsection\<open>A map from a sphere to a higher dimensional sphere is nullhomotopic\<close>

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 /\<^sub>R norm x) \ S"
    using subspace_mul \<open>subspace S\<close> by blast
  have subS01: "(\x. x /\<^sub>R norm x) ` (S - {0}) \ sphere 0 1 \ S"
    using \<open>subspace S\<close> subspace_mul by fastforce
  then have diff_f': "f differentiable_on (\x. x /\<^sub>R norm x) ` (S - {0})"
    by (rule differentiable_on_subset [OF diff_f])
  define g where "g \ \x. norm x *\<^sub>R f(inverse(norm x) *\<^sub>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 *\<^sub>R f (u /\<^sub>R norm u) \ T\ \ u = 0"
      by (metis (mono_tags, lifting) DiffI subS01 subspace_mul [OF \<open>subspace T\<close>] 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 /\<^sub>R norm y) = 0"
      then have "y \ 0 \ y /\<^sub>R norm y \ sphere 0 1 \ S"
        by (auto simp: subspace_mul [OF \<open>subspace S\<close>])
      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 *\<^sub>R f (x /\<^sub>R norm x)) ` (S - {0})"
          if "x \ T" "x \ 0" for x
    proof -
      have "x /\<^sub>R norm x \ T"
        using \<open>subspace T\<close> subspace_mul that by blast
      then obtain u where u: "f u \ T" "x /\<^sub>R norm x = f u" "norm u = 1" "u \ S"
        using * [THEN subsetD, of "x /\<^sub>R norm x"] \x \ 0\ by auto
      with that have [simp]: "norm x *\<^sub>R f u = x"
        by (metis divideR_right norm_eq_zero)
      moreover have "norm x *\<^sub>R u \ S - {0}"
        using \<open>subspace S\<close> subspace_scale that(2) u by auto
      with u show ?thesis
        by (simp add: image_eqI [where x="norm x *\<^sub>R u"])
    qed
    then have "T - {0} \ (\x. norm x *\<^sub>R f (x /\<^sub>R norm x)) ` (S - {0})"
      by force
    then show "T - {0} \ g ` (S - {0})"
      by (simp add: g_def)
  qed
  define T' where "T' \<equiv> {y. \<forall>x \<in> 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] \<open>subspace T\<close>
    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 \<open>subspace T\<close> 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 \<open>subspace T'\<close> 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 *\<^sub>R x) = c *\<^sub>R p1 x \ p2 (c *\<^sub>R x) = c *\<^sub>R p2 x"
  proof -
    fix c :: real and x :: 'a
    have f1: "c *\<^sub>R x = c *\<^sub>R p1 x + c *\<^sub>R p2 x"
      by (metis eq pth_6)
    have f2: "c *\<^sub>R p2 x \ T'"
      by (simp add: \<open>subspace T'\<close> p2 subspace_scale)
    have "c *\<^sub>R p1 x \ T"
      by (metis (full_types) assms(2) p1span span_eq_iff subspace_scale)
    then show "p1 (c *\<^sub>R x) = c *\<^sub>R p1 x \ p2 (c *\<^sub>R x) = c *\<^sub>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 \<open>S \<subseteq> T\<close>  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 \<open>linear p1\<close>]])
  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 \<open>linear p2\<close>])
  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 \<open>subspace S\<close> \<open>subspace T'\<close>]
    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\
          \<Longrightarrow> g s + t' \<in> (\<lambda>x. g (p1 x) + p2 x) `
                         {x + t' |x t'. x \<in> S \<and> x \<noteq> 0 \<and> t' \<in> T'}" for t' s
      using \<open>S \<subseteq> T\<close> p12_eq  by (rule_tac x="s + t'" in image_eqI) auto
    then show "{x + y |x y. x \ g ` (S - {0}) \ y \ T'}
          \<subseteq> (\<lambda>x. g (p1 x) + p2 x) ` {x + y |x y. x \<in> S - {0} \<and> y \<in> 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 \<open>z \<notin> T'\<close> 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 auto
  have "compact (sphere 0 1 \ S)"
    by (simp add: \<open>subspace S\<close> 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 _ \<open>subspace T\<close>, of "1/2"] fim
    by (auto simp: image_subset_iff_funcset)
  have gnz: "g x \ 0" if "x \ sphere 0 1 \ S" for x
    using g12 that by fastforce
  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)) *\<^sub>R g x"
  have h: "x \ sphere 0 1 \ S \ h x \ sphere 0 1 \ T" for x
    unfolding h_def using \<open>subspace T\<close> gim gnz subspace_mul by fastforce
  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: \<open>subspace T\<close> subspace_imp_convex)
      then have "convex hull {f x, g x} \ T"
        by (metis IntD2 PiE closed_segment_subset fim gim 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 \<open>S \<subseteq> T\<close> 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 \<open>subspace T\<close>])
    qed (simp add: subspace_imp_convex [OF \<open>subspace T\<close>])
    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) *\<^sub>R y)"
    by (intro continuous_intros) auto
  have sub0T: "(\y. y /\<^sub>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 \<open>subspace U\<close> 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 \<open>subspace T\<close>])
    show "T \ U"
      using span_eq_iff \<open>subspace U\<close> \<open>T \<subseteq> span U\<close> by blast
    show "aff_dim T = aff_dim S"
      using dimT \<open>subspace T\<close> 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 \<open>subspace T\<close> 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 \<open>aff_dim T = aff_dim S\<close> by simp
      have "rel_frontier S homeomorphic rel_frontier(ball 0 1 \ T)"
        using homeomorphic_rel_frontiers_convex_bounded_sets [OF \<open>convex S\<close> \<open>bounded S\<close>]
        by (simp add: \<open>subspace T\<close> affS_eq assms bounded_Int convex_Int
            homeomorphic_rel_frontiers_convex_bounded_sets subspace_imp_convex)
      also have "... = frontier (ball 0 1) \ T"
      proof (rule convex_affine_rel_frontier_Int [OF convex_ball])
        show "affine T"
          by (simp add: \<open>subspace T\<close> subspace_imp_affine)
        show "interior (ball 0 1) \ T \ {}"
          using \<open>subspace T\<close> 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 show ?thesis
      by (smt (verit, best) False affST aff_dim_negative_iff)
  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 \<open>T \<noteq> {}\<close>  spheremap_lemma3 [OF \<open>bounded T\<close> \<open>convex T\<close> 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 \<open>bounded S\<close> \<open>convex S\<close> \<open>subspace T'\<close>] \<open>S \<noteq> {}\<close>
    obtain S':: "'a set" where "subspace S'" "S' \<subseteq> 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 \<open>S' \<subseteq> T'\<close> \<open>subspace S'\<close> \<open>subspace T'\<close> 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 \<open>S' \<subseteq> T'\<close> \<open>subspace S'\<close> \<open>subspace T'\<close> 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 \<open>\<not> s \<le> 0\<close> have "r > 0" "s > 0" by auto
    show thesis
      using inessential_spheremap_lowdim_gen [of "cball a r" "cball b s" f]
      using \<open>0 < r\<close> \<open>0 < s\<close> assms(1) that by (auto simp add: f aff_dim_cball)
  qed
qed

subsection\<open> Some technical lemmas about extending maps from cell complexes\<close>

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 \<F>)
  case empty show ?case by simp
next
  case (insert S \<F>)
  then obtain f where contf: "continuous_on S f" and fim: "f \ S \ T" and feq: "\x \ S \ K. f x = h x"
    by (metis funcset_image insert_iff)
  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 \<open>S \<notin> \<F>\<close> 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)
  moreover have "S \ \ \ = \ (insert S \)"
    by auto
  ultimately show ?case
    by (smt (verit) Int_iff Pi_iff UnE feq fim geq gim)
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)"
proof -
  have "\S T. \S \ \; \U\\. \ S \ U; T \ \; \U\\. \ T \ U; S \ T\ \ S \ T \ K"
    by (metis K psubsetI)
  then show ?thesis
    apply (simp flip: Union_maximal_sets [OF fin])
    apply (rule extending_maps_Union_aux, simp_all add: Union_maximal_sets [OF fin] assms)
    done
qed

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
    using True assms(2) contf fim that by force
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 ` (\<Union> (\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < i})) \<subseteq> rel_frontier T \<and>
                     (\<forall>x \<in> \<Union>\<G>. 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 \<open>bounded T\<close> have "rel_frontier T \<noteq> {}"
      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}))
                         \<subseteq> 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 \<in> D \<rightarrow> rel_frontier T \<and>
                       (\<forall>x \<in> D \<inter> \<Union>(\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> 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 \<open>D \<noteq> {}\<close> \<open>bounded D\<close> by blast
        have "{F. F facet_of D} \ {E. E face_of C \ aff_dim E < int p}"
          by clarify (metis \<open>D face_of C\<close> affD eq_iff face_of_trans facet_of_def zle_diff1_eq)
        moreover have "polyhedron D"
          using \<open>C \<in> \<F>\<close> \<open>D face_of C\<close> 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 \<open>C \<in> \<F>\<close> him by blast
        have "convex D"
          by (simp add: \<open>polyhedron D\<close> 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 \<open>C \<in> \<F>\<close> 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)) =
                      (\<exists>g. continuous_on UNIV g \<and>  range g \<subseteq> rel_frontier T \<and>
                           (\<forall>x\<in>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 \<open>convex D\<close> \<open>bounded D\<close> \<open>convex T\<close> \<open>bounded T\<close> 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 \<open>C \<in> \<F>\<close> \<open>D face_of C\<close> 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 \<open>C \<in> \<F>\<close> \<open>D face_of C\<close> 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 \<open>finite \<F>\<close> \<open>\<G> \<subseteq> \<F>\<close> rev_finite_subset by blast
    moreover have "finite (?Faces)"
    proof -
      have \<section>: "finite (\<Union> {{D. D face_of C} |C. C \<in> \<F>})"
        by (auto simp: \<open>finite \<F>\<close> finite_polytope_faces poly)
      show ?thesis
        by (auto intro: finite_subset [OF _ \<section>])
    qed
    ultimately have fin: "finite (\ \ ?Faces)"
      by simp
    have clo: "closed S" if "S \ \ \ ?Faces" for S
      using that \<open>\<G> \<subseteq> \<F>\<close> 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) IntI face_of_aff_dim_lt face_of_imp_convex face_of_trans ff inf_commute)
    qed
    obtain g where "continuous_on (\(\ \ ?Faces)) g"
                   "g ` \(\ \ ?Faces) \ rel_frontier T"
                   "(\x \ \(\ \ ?Faces) \
                          \<Union>(\<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> 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 \<open>\<G> \<subseteq> \<F>\<close> face_of_imp_subset by fastforce
    show "\\ \ \(\ \ {D. \C\\. D face_of C \ aff_dim D < i})"
        using face by (intro Union_mono) (fastforce simp: aff i)
  qed
  have "int i \ aff_dim T" by (simp add: i)
  then show ?thesis
    using extendf [of i] that unfolding eq by fastforce
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 (\<Union>\<F> - C) g \<and> g \<in> (\<Union>\<F> - C) \<rightarrow> T
                  \<and> (\<forall>x \<in> (\<Union>\<F> - C) \<inter> K. g x = h x)"
  using assms
proof induction
  case empty then show ?case
    by force
next
  case (insert X \<F>)
  then have "closed X" and clo: "\X. X \ \ \ closed X"
        and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (S - {a}) g \<and> g \<in> (S - {a}) \<rightarrow> T \<and> (\<forall>x \<in> S \<inter> 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 \<F> 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 \<open>a \<notin> U\<close> 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 \<open>closed X\<close> apply blast
        using \<open>closed (\<Union>\<F>)\<close> 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 Pi_iff by fastforce
  qed
qed

lemma extend_map_lemma_cofinite1:
assumes "finite \"
    and \<F>: "\<And>X. X \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (X - {a}) g \<and> g \<in> (X - {a}) \<rightarrow> T \<and> (\<forall>x \<in> X \<inter> 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 ?\<F> = "{X \<in> \<F>. \<forall>Y\<in>\<F>. \<not> X \<subset> Y}"
  have [simp]: "\?\ = \\"
    by (simp add: Union_maximal_sets assms)
  have fin: "finite ?\"
    by (force intro: finite_subset [OF _ \<open>finite \<F>\<close>])
  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: \<open>finite \<F>\<close> card_mono)
  moreover
  obtain C g where "finite C \ disjnt C U \ card C \ card ?\ \
                 continuous_on (\<Union>?\<F> - C) g \<and> g \<in> (\<Union>?\<F> - C) \<rightarrow> T
                  \<and> (\<forall>x \<in> (\<Union>?\<F> - C) \<inter> K. g x = h x)"
    using extend_map_lemma_cofinite0 [OF fin pw, of U T h] by (fastforce intro!: clo \<F>)
  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 \<H> where "\<H> \<equiv> \<G> \<union> {D. \<exists>C \<in> \<F> - \<G>. D face_of C \<and> 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 \<open>finite \<F>\<close> by force
  then have "finite \"
    by (auto simp: \<H>_def \<open>finite \<G>\<close> 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: \<H>_def) (smt (verit) \<open>\<G> \<subseteq> \<F>\<close> 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 \<open>finite \<H>\<close> [unfolded \<H>_def] Un_upper1 T])
    show "\X. \X \ \ \ {D. \C\\ - \. D face_of C \ aff_dim D < aff_dim T}\ \ polytope X"
      using \<open>\<G> \<subseteq> \<F>\<close> face_of_polytope_polytope poly by fastforce
  qed (use * \<H>_def contf fim in auto)
  have "bounded (\\)"
    using \<open>finite \<G>\<close> \<open>\<G> \<subseteq> \<F>\<close> poly polytope_imp_bounded by blast
  then have "\\ \ UNIV"
    by auto
  then obtain a where a: "a \ \\"
    by blast
  have \<F>: "\<exists>a g. a \<notin> \<Union>\<G> \<and> continuous_on (D - {a}) g \<and>
                  g \<in> (D - {a}) \<rightarrow> rel_frontier T \<and> (\<forall>x \<in> D \<inter> \<Union>\<H>. 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!: \<open>a \<notin> \<Union>\<G>\<close> 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: \<H>_def)
    next
      case False
      then have affD: "aff_dim D \ aff_dim T"
        by (simp add: \<open>D \<in> \<F>\<close> aff)
      show ?thesis
      proof (cases "rel_interior D = {}")
        case True
        with \<open>D \<in> \<F>\<close> 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 \<open>\<G> \<subseteq> \<F>\<close> face' that by auto
            with face_of_subset_rel_frontier \<open>E \<in> \<G>\<close> \<open>b \<in> E\<close> brelD rel_interior_subset [of D]
                 D_not_subset rel_frontier_def \<H>_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"
            using rim by auto
          also have "... \ \{E. E face_of D \ aff_dim E < aff_dim T}"
            using affD
            by (force simp: rel_frontier_of_polyhedron [OF \<open>polyhedron D\<close>] facet_of_def)
          also have "... \ \(\)"
            using D_not_subset \<H>_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: \<H>_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 \<open>A \<in> \<G>\<close> \<open>\<G> \<subseteq> \<F>\<close> face \<open>D \<in> \<F>\<close> by blast
                show "D \ A \ D"
                  using \<open>A \<in> \<G>\<close> D_not_subset \<H>_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: \<open>polyhedron D\<close> polyhedron_imp_convex face_of_refl)
                then show "D \ A face_of D"
                  by (meson "2"(2) "2"(3) \<open>D \<in> \<F>\<close> face' face_of_Int_Int face_of_face)
                show "D \ A \ D"
                  using "2" D_not_subset \<H>_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 \<open>finite \<F>\<close> \<F> 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: \<H>_def)
    next
      case False
      have "X \ Y \ X"
        using \<open>\<not> X \<subseteq> Y\<close> by blast
      with XY
      show ?thesis
        by (clarsimp simp: \<H>_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 \<open>\<G> \<subseteq> \<F>\<close> show ?thesis
    by (rule_tac C=C and g=g in that) (auto simp: disjnt_def hf [symmetric] \<H>_def intro!: gh)
qed

text\<open>The next two proofs are similar\<close>
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 _ \<open>closed S\<close>] 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>open V\<close> \<open>S \<subseteq> V\<close> by force
  obtain \<G> where "finite \<G>" "\<Union>\<G> = \<Union>\<F>"
             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 \<open>d>0\<close> \<open>finite \<F>\<close> 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 \<G> "\<G> \<inter> Pow V" T g])
    show "continuous_on (\(\ \ Pow V)) g"
      by (metis Union_Int_subset Union_Pow_eq \<open>continuous_on V g\<close> continuous_on_subset le_inf_iff)
  qed (use \<open>finite \<G>\<close> T polyG affG faceG gim image_subset_iff_funcset in auto)
  show ?thesis
  proof
    show "continuous_on (\\) h"
      using \<open>\<Union>\<G> = \<Union>\<F>\<close> conth by auto
    show "h \ \\ \ rel_frontier T"
      using \<open>\<Union>\<G> = \<Union>\<F>\<close> him by auto
    show "h x = f x" if "x \ S" for x
    proof -
      have "x \ \\"
        using \<open>\<Union>\<G> = \<Union>\<F>\<close> \<open>S \<subseteq> \<Union>\<F>\<close> that by auto
      then obtain X where "x \ X" "X \ \" by blast
      then have "diameter X < d" "bounded X"
        by (auto simp: diaG \<open>X \<in> \<G>\<close> 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 \<open>X \<in> \<G>\<close> \<open>X \<subseteq> V\<close> \<open>x \<in> X\<close> 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 _ \<open>closed S\<close>] 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>open V\<close> \<open>S \<subseteq> V\<close> by force
  obtain \<G> where "finite \<G>" "\<Union>\<G> = \<Union>\<F>"
             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 \<open>d>0\<close> \<open>finite \<F>\<close> 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 \<G> "\<G> \<inter> Pow V" T g])
    show "continuous_on (\(\ \ Pow V)) g"
      by (metis Union_Int_subset Union_Pow_eq \<open>continuous_on V g\<close> continuous_on_subset le_inf_iff)
    show "g \ \(\ \ Pow V) \ rel_frontier T"
      using gim by force
  qed (auto intro: \<open>finite \<G>\<close> T polyG affG dest: faceG)
  have "S \ \(\ \ Pow V)"
  proof
    fix x
    assume "x \ S"
    then have "x \ \\"
      using \<open>\<Union>\<G> = \<Union>\<F>\<close> \<open>S \<subseteq> \<Union>\<F>\<close> by auto
    then obtain X where "x \ X" "X \ \" by blast
    then have "diameter X < d" "bounded X"
      by (auto simp: diaG \<open>X \<in> \<G>\<close> 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 \<open>X \<in> \<G>\<close> \<open>x \<in> X\<close> by blast
  qed
  then show ?thesis
    by (metis PowI Union_Pow_eq \<open>\<Union> \<G> = \<Union> \<F>\<close> \<open>finite C\<close> conth dis disjnt_Union2 gf hg him subsetD that)
qed

subsection\<open> Special cases and corollaries involving spheres\<close>

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 \<in> (T - K) \<rightarrow> rel_frontier U \<and> (\<forall>x \<in> 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 \<open>bounded U\<close> have "aff_dim U \<le> 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 \<open>affine T\<close> affine_bounded_eq_lowdim affine_bounded_eq_trivial by auto
      then show ?thesis
        using \<open>S = {}\<close> 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] \<open>S = {}\<close> by force
    qed
  next
    case False
    have "bounded S"
      by (simp add: \<open>compact S\<close> 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 \<open>S \<subseteq> T\<close> have "S \<subseteq> bbox \<inter> 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 _ \<open>convex U\<close> \<open>bounded U\<close> _ _ _ contf fim])
      show "closed S"
        using \<open>compact S\<close> 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 \<open>affine T\<close>)
      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: \<open>aff_dim (bbox \<inter> T) \<le> aff_dim U\<close>)
    qed auto
    define fro where "fro \ \d. frontier(cbox (-(b + d *\<^sub>R One)) (b + d *\<^sub>R One))"
    obtain d where d12: "1/2 \ d" "d \ 1" and dd: "disjnt K (fro d)"
    proof (rule disjoint_family_elem_disjnt [OF _ \<open>finite K\<close>])
      show "infinite {1/2..1::real}"
        by (simp add: infinite_Icc)
      have dis1: "disjnt (fro x) (fro y)" if "x 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 *\<^sub>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 \<open>affine T\<close>)
    have cpT_ne: "cbox (- c) c \ T \ {}"
      using \<open>S \<noteq> {}\<close> b cbsub(2) \<open>S \<subseteq> T\<close> 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 \<open>S \<noteq> {}\<close> \<open>S \<subseteq> T\<close> b \<open>cbox (- b) b \<subseteq> box (- c) c\<close> by force
      have "convex T"
        by (meson \<open>affine T\<close> affine_imp_convex)
      then have "x \ affine hull (cbox (- c) c \ T)"
          by (metis Int_commute Int_iff \<open>S \<noteq> {}\<close> \<open>S \<subseteq> T\<close> cbsub(1) \<open>x \<in> T\<close> 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 _  \<open>affine T\<close> 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 \<open>affine T\<close>)
        show "closed (cbox (- c) c \ T)"
          using clo_cbT by blast
        show "cbox (- c) c \ T \ {}"
          using \<open>S \<noteq> {}\<close> 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"
        using gim by blast
      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 \<open>S \<subseteq> T\<close> 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 \<open>S \<subseteq> T\<close> 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\<open>Extending maps to spheres\<close>

(*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 \<open>affine U\<close>)
  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 \<union> (C - {a})) \<subseteq> T \<and> (\<forall>x \<in> 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 (metis C \<open>locally connected U\<close> clo closedin_def locally_connected_open_component topspace_euclidean_subtopology)
    then obtain d where "C \ U" "0 < d" and d: "cball a d \ U \ C"
      using openin_contains_cball by (metis \<open>a \<in> C\<close>)
    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 (top_of_set C) (ball a d \ U)"
        by (metis open_ball \<open>C \<subseteq> U\<close> \<open>ball a d \<inter> U \<subseteq> C\<close> inf.absorb_iff2 inf.orderE inf_assoc open_openin openin_subtopology)
      show "openin (top_of_set (affine hull C)) C"
        by (metis \<open>a \<in> C\<close> \<open>openin (top_of_set U) C\<close> affine_hull_eq affine_hull_openin all_not_in_conv \<open>affine U\<close>)
      show "ball a d \ U \ {}"
        using \<open>0 < d\<close> \<open>C \<subseteq> U\<close> \<open>a \<in> C\<close> by force
      show "finite (C \ K)"
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.26 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.