src/HOL/Analysis/Further_Topology.thy

merged

section \<open>Extending Continous Maps, Invariance of Domain, etc..\<close>

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

theory Further_Topology
  imports Equivalence_Lebesgue_Henstock_Integration Weierstrass_Theorems Polytope Complex_Transcendental
begin

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

lemma spheremap_lemma1:
  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
  assumes "subspace S" "subspace T" and dimST: "dim S < dim T"
      and "S \<subseteq> T"
      and diff_f: "f differentiable_on sphere 0 1 \<inter> S"
    shows "f ` (sphere 0 1 \<inter> S) \<noteq> sphere 0 1 \<inter> T"
proof
  assume fim: "f ` (sphere 0 1 \<inter> S) = sphere 0 1 \<inter> T"
  have inS: "\<And>x. \<lbrakk>x \<in> S; x \<noteq> 0\<rbrakk> \<Longrightarrow> (x /\<^sub>R norm x) \<in> S"
    using subspace_mul \<open>subspace S\<close> by blast
  have subS01: "(\<lambda>x. x /\<^sub>R norm x) ` (S - {0}) \<subseteq> sphere 0 1 \<inter> S"
    using \<open>subspace S\<close> subspace_mul by fastforce
  then have diff_f': "f differentiable_on (\<lambda>x. x /\<^sub>R norm x) ` (S - {0})"
    by (rule differentiable_on_subset [OF diff_f])
  define g where "g \<equiv> \<lambda>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 "g ` (S - {0}) \<subseteq> T"
      apply (auto simp: g_def subspace_mul [OF \<open>subspace T\<close>])
      apply (metis (mono_tags, lifting) DiffI subS01 subspace_mul [OF \<open>subspace T\<close>] fim image_subset_iff inf_le2 singletonD)
      done
    moreover have "g ` (S - {0}) \<subseteq> UNIV - {0}"
    proof (clarsimp simp: g_def)
      fix y
      assume "y \<in> S" and f0: "f (y /\<^sub>R norm y) = 0"
      then have "y \<noteq> 0 \<Longrightarrow> y /\<^sub>R norm y \<in> sphere 0 1 \<inter> 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}) \<subseteq> T - {0}"
      by auto
  next
    have *: "sphere 0 1 \<inter> T \<subseteq> f ` (sphere 0 1 \<inter> S)"
      using fim by (simp add: image_subset_iff)
    have "x \<in> (\<lambda>x. norm x *\<^sub>R f (x /\<^sub>R norm x)) ` (S - {0})"
          if "x \<in> T" "x \<noteq> 0" for x
    proof -
      have "x /\<^sub>R norm x \<in> T"
        using \<open>subspace T\<close> subspace_mul that by blast
      then show ?thesis
        using * [THEN subsetD, of "x /\<^sub>R norm x"] that apply clarsimp
        apply (rule_tac x="norm x *\<^sub>R xa" in image_eqI, simp)
        apply (metis norm_eq_zero right_inverse scaleR_one scaleR_scaleR)
        using \<open>subspace S\<close> subspace_mul apply force
        done
    qed
    then have "T - {0} \<subseteq> (\<lambda>x. norm x *\<^sub>R f (x /\<^sub>R norm x)) ` (S - {0})"
      by force
    then show "T - {0} \<subseteq> 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: dim_UNIV T'_def)
  have "\<exists>v1 v2. v1 \<in> span T \<and> (\<forall>w \<in> span T. orthogonal v2 w) \<and> x = v1 + v2" for x
    by (force intro: orthogonal_subspace_decomp_exists [of T x])
  then obtain p1 p2 where p1span: "p1 x \<in> span T"
                      and "\<And>w. w \<in> span T \<Longrightarrow> orthogonal (p2 x) w"
                      and eq: "p1 x + p2 x = x" for x
    by metis
  then have p1: "\<And>z. p1 z \<in> T" and ortho: "\<And>w. w \<in> T \<Longrightarrow> orthogonal (p2 x) w" for x
    using span_eq \<open>subspace T\<close> by blast+
  then have p2: "\<And>z. p2 z \<in> T'"
    by (simp add: T'_def orthogonal_commute)
  have p12_eq: "\<And>x y. \<lbrakk>x \<in> T; y \<in> T'\<rbrakk> \<Longrightarrow> p1(x + y) = x \<and> p2(x + y) = y"
  proof (rule orthogonal_subspace_decomp_unique [OF eq p1span, where T=T'])
    show "\<And>x y. \<lbrakk>x \<in> T; y \<in> T'\<rbrakk> \<Longrightarrow> p2 (x + y) \<in> span T'"
      using span_eq p2 \<open>subspace T'\<close> by blast
    show "\<And>a b. \<lbrakk>a \<in> T; b \<in> T'\<rbrakk> \<Longrightarrow> orthogonal a b"
      using T'_def by blast
  qed (auto simp: span_superset)
  then have "\<And>c x. p1 (c *\<^sub>R x) = c *\<^sub>R p1 x \<and> p2 (c *\<^sub>R x) = c *\<^sub>R p2 x"
    by (metis eq \<open>subspace T\<close> \<open>subspace T'\<close> p1 p2 scaleR_add_right subspace_mul)
  moreover have lin_add: "\<And>x y. p1 (x + y) = p1 x + p1 y \<and> p2 (x + y) = p2 x + p2 y"
  proof (rule orthogonal_subspace_decomp_unique [OF _ p1span, where T=T'])
    show "\<And>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  "\<And>a b. \<lbrakk>a \<in> T; b \<in> T'\<rbrakk> \<Longrightarrow> orthogonal a b"
      using T'_def by blast
  qed (auto simp: p1span p2 span_superset subspace_add)
  ultimately have "linear p1" "linear p2"
    by unfold_locales auto
  have "(\<lambda>z. g (p1 z)) differentiable_on {x + y |x y. x \<in> S - {0} \<and> y \<in> T'}"
    apply (rule differentiable_on_compose [where f=g])
    apply (rule linear_imp_differentiable_on [OF \<open>linear p1\<close>])
    apply (rule differentiable_on_subset [OF gdiff])
    using p12_eq \<open>S \<subseteq> T\<close> apply auto
    done
  then have diff: "(\<lambda>x. g (p1 x) + p2 x) differentiable_on {x + y |x y. x \<in> S - {0} \<and> y \<in> T'}"
    by (intro derivative_intros linear_imp_differentiable_on [OF \<open>linear p2\<close>])
  have "dim {x + y |x y. x \<in> S - {0} \<and> y \<in> T'} \<le> dim {x + y |x y. x \<in> S  \<and> y \<in> T'}"
    by (blast intro: dim_subset)
  also have "... = dim S + dim T' - dim (S \<inter> 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 \<in> S - {0} \<and> y \<in> T'}"
    by (rule negligible_lowdim)
  have "negligible ((\<lambda>x. g (p1 x) + p2 x) ` {x + y |x y. x \<in> S - {0} \<and> y \<in> T'})"
    by (rule negligible_differentiable_image_negligible [OF order_refl neg diff])
  then have "negligible {x + y |x y. x \<in> g ` (S - {0}) \<and> y \<in> T'}"
  proof (rule negligible_subset)
    have "\<lbrakk>t' \<in> T'; s \<in> S; s \<noteq> 0\<rbrakk>
          \<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
      apply (rule_tac x="s + t'" in image_eqI)
      using \<open>S \<subseteq> T\<close> p12_eq by auto
    then show "{x + y |x y. x \<in> g ` (S - {0}) \<and> y \<in> 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' \<subseteq> {x + y |x y. x \<in> g ` (S - {0}) \<and> y \<in> T'}"
  proof clarsimp
    fix z assume "z \<notin> T'"
    show "\<exists>x y. z = x + y \<and> x \<in> g ` (S - {0}) \<and> y \<in> T'"
      apply (rule_tac x="p1 z" in exI)
      apply (rule_tac x="p2 z" in exI)
      apply (simp add: p1 eq p2 geq)
      by (metis \<open>z \<notin> T'\<close> add.left_neutral eq p2)
  qed
  ultimately have "negligible (-T')"
    using negligible_subset by blast
  moreover have "negligible T'"
    using negligible_lowdim
    by (metis add.commute assms(3) diff_add_inverse2 diff_self_eq_0 dim_eq le_add1 le_antisym linordered_semidom_class.add_diff_inverse not_less0)
  ultimately have  "negligible (-T' \<union> 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 \<Rightarrow> 'a::euclidean_space"
  assumes ST: "subspace S" "subspace T" "dim S < dim T"
      and "S \<subseteq> T"
      and contf: "continuous_on (sphere 0 1 \<inter> S) f"
      and fim: "f ` (sphere 0 1 \<inter> S) \<subseteq> sphere 0 1 \<inter> T"
    shows "\<exists>c. homotopic_with (\<lambda>x. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) f (\<lambda>x. c)"
proof -
  have [simp]: "\<And>x. \<lbrakk>norm x = 1; x \<in> S\<rbrakk> \<Longrightarrow> norm (f x) = 1"
    using fim by (simp add: image_subset_iff)
  have "compact (sphere 0 1 \<inter> 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 \<inter> S) \<subseteq> T"
                and g12: "\<And>x. x \<in> sphere 0 1 \<inter> S \<Longrightarrow> norm(f x - g x) < 1/2"
    apply (rule Stone_Weierstrass_polynomial_function_subspace [OF _ contf _ \<open>subspace T\<close>, of "1/2"])
    using fim apply auto
    done
  have gnz: "g x \<noteq> 0" if "x \<in> sphere 0 1 \<inter> 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 \<inter> S"
    by (metis pfg differentiable_on_polynomial_function)
  define h where "h \<equiv> \<lambda>x. inverse(norm(g x)) *\<^sub>R g x"
  have h: "x \<in> sphere 0 1 \<inter> S \<Longrightarrow> h x \<in> sphere 0 1 \<inter> T" for x
    unfolding h_def
    using gnz [of x]
    by (auto simp: subspace_mul [OF \<open>subspace T\<close>] subsetD [OF gim])
  have diffh: "h differentiable_on sphere 0 1 \<inter> S"
    unfolding h_def
    apply (intro derivative_intros diffg differentiable_on_compose [OF diffg])
    using gnz apply auto
    done
  have homfg: "homotopic_with (\<lambda>z. True) (sphere 0 1 \<inter> S) (T - {0}) f g"
  proof (rule homotopic_with_linear [OF contf])
    show "continuous_on (sphere 0 1 \<inter> S) g"
      using pfg by (simp add: differentiable_imp_continuous_on diffg)
  next
    have non0fg: "0 \<notin> closed_segment (f x) (g x)" if "norm x = 1" "x \<in> S" for x
    proof -
      have "f x \<in> sphere 0 1"
        using fim that by (simp add: image_subset_iff)
      moreover have "norm(f x - g x) < 1/2"
        apply (rule g12)
        using that by force
      ultimately show ?thesis
        by (auto simp: norm_minus_commute dest: segment_bound)
    qed
    show "\<And>x. x \<in> sphere 0 1 \<inter> S \<Longrightarrow> closed_segment (f x) (g x) \<subseteq> T - {0}"
      apply (simp add: subset_Diff_insert non0fg)
      apply (simp add: segment_convex_hull)
      apply (rule hull_minimal)
       using fim image_eqI gim apply force
      apply (rule subspace_imp_convex [OF \<open>subspace T\<close>])
      done
  qed
  obtain d where d: "d \<in> (sphere 0 1 \<inter> T) - h ` (sphere 0 1 \<inter> S)"
    using h spheremap_lemma1 [OF ST \<open>S \<subseteq> T\<close> diffh] by force
  then have non0hd: "0 \<notin> closed_segment (h x) (- d)" if "norm x = 1" "x \<in> 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 \<inter> S) h"
    using differentiable_imp_continuous_on diffh by blast
  have hom_hd: "homotopic_with (\<lambda>z. True) (sphere 0 1 \<inter> S) (T - {0}) h (\<lambda>x. -d)"
    apply (rule homotopic_with_linear [OF conth continuous_on_const])
    apply (simp add: subset_Diff_insert non0hd)
    apply (simp add: segment_convex_hull)
    apply (rule hull_minimal)
     using h d apply (force simp: subspace_neg [OF \<open>subspace T\<close>])
    apply (rule subspace_imp_convex [OF \<open>subspace T\<close>])
    done
  have conT0: "continuous_on (T - {0}) (\<lambda>y. inverse(norm y) *\<^sub>R y)"
    by (intro continuous_intros) auto
  have sub0T: "(\<lambda>y. y /\<^sub>R norm y) ` (T - {0}) \<subseteq> sphere 0 1 \<inter> T"
    by (fastforce simp: assms(2) subspace_mul)
  obtain c where homhc: "homotopic_with (\<lambda>z. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) h (\<lambda>x. c)"
    apply (rule_tac c="-d" in that)
    apply (rule homotopic_with_eq)
       apply (rule homotopic_compose_continuous_left [OF hom_hd conT0 sub0T])
    using d apply (auto simp: h_def)
    done
  show ?thesis
    apply (rule_tac x=c in exI)
    apply (rule homotopic_with_trans [OF _ homhc])
    apply (rule homotopic_with_eq)
       apply (rule homotopic_compose_continuous_left [OF homfg conT0 sub0T])
      apply (auto simp: h_def)
    done
qed


lemma spheremap_lemma3:
  assumes "bounded S" "convex S" "subspace U" and affSU: "aff_dim S \<le> dim U"
  obtains T where "subspace T" "T \<subseteq> U" "S \<noteq> {} \<Longrightarrow> aff_dim T = aff_dim S"
                  "(rel_frontier S) homeomorphic (sphere 0 1 \<inter> 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 \<in> S"
    by auto
  then have affS: "aff_dim S = int (dim ((\<lambda>x. -a+x) ` S))"
    by (metis hull_inc aff_dim_eq_dim)
  with affSU have "dim ((\<lambda>x. -a+x) ` S) \<le> dim U"
    by linarith
  with choose_subspace_of_subspace
  obtain T where "subspace T" "T \<subseteq> span U" and dimT: "dim T = dim ((\<lambda>x. -a+x) ` S)" .
  show ?thesis
  proof (rule that [OF \<open>subspace T\<close>])
    show "T \<subseteq> U"
      using span_eq \<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 \<inter> T"
    proof -
      have "aff_dim (ball 0 1 \<inter> 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 \<inter> T)"
        using \<open>aff_dim T = aff_dim S\<close> by simp
      have "rel_frontier S homeomorphic rel_frontier(ball 0 1 \<inter> T)"
        apply (rule homeomorphic_rel_frontiers_convex_bounded_sets [OF \<open>convex S\<close> \<open>bounded S\<close>])
          apply (simp add: \<open>subspace T\<close> convex_Int subspace_imp_convex)
         apply (simp add: bounded_Int)
        apply (rule affS_eq)
        done
      also have "... = frontier (ball 0 1) \<inter> T"
        apply (rule convex_affine_rel_frontier_Int [OF convex_ball])
         apply (simp add: \<open>subspace T\<close> subspace_imp_affine)
        using \<open>subspace T\<close> subspace_0 by force
      also have "... = sphere 0 1 \<inter> T"
        by auto
      finally show ?thesis .
    qed
  qed
qed


proposition inessential_spheremap_lowdim_gen:
  fixes f :: "'M::euclidean_space \<Rightarrow> '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) \<subseteq> rel_frontier T"
  obtains c where "homotopic_with (\<lambda>z. True) (rel_frontier S) (rel_frontier T) f (\<lambda>x. c)"
proof (cases "S = {}")
  case True
  then show ?thesis
    by (simp add: that)
next
  case False
  then show ?thesis
  proof (cases "T = {}")
    case True
    then show ?thesis
      using fim that by auto
  next
    case False
    obtain T':: "'a set"
      where "subspace T'" and affT': "aff_dim T' = aff_dim T"
        and homT: "rel_frontier T homeomorphic sphere 0 1 \<inter> T'"
      apply (rule spheremap_lemma3 [OF \<open>bounded T\<close> \<open>convex T\<close> subspace_UNIV, where 'b='a])
       apply (simp add: dim_UNIV aff_dim_le_DIM)
      using \<open>T \<noteq> {}\<close> by blast
    with homeomorphic_imp_homotopy_eqv
    have relT: "sphere 0 1 \<inter> T'  homotopy_eqv rel_frontier T"
      using homotopy_eqv_sym by blast
    have "aff_dim S \<le> int (dim T')"
      using affT' \<open>subspace T'\<close> 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 \<inter> S'"
        by metis
    with homeomorphic_imp_homotopy_eqv
    have relS: "sphere 0 1 \<inter> S'  homotopy_eqv rel_frontier S"
      using homotopy_eqv_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 "\<exists>c. homotopic_with (\<lambda>z. True) (rel_frontier S) (rel_frontier T) f (\<lambda>x. c)"
      apply (rule homotopy_eqv_homotopic_triviality_null_imp [OF relT contf fim])
      apply (rule homotopy_eqv_cohomotopic_triviality_null[OF relS, THEN iffD1, rule_format])
       apply (metis dimST' \<open>subspace S'\<close>  \<open>subspace T'\<close>  \<open>S' \<subseteq> T'\<close> spheremap_lemma2, blast)
      done
    with that show ?thesis by blast
  qed
qed

lemma inessential_spheremap_lowdim:
  fixes f :: "'M::euclidean_space \<Rightarrow> 'a::euclidean_space"
  assumes
   "DIM('M) < DIM('a)" and f: "continuous_on (sphere a r) f" "f ` (sphere a r) \<subseteq> (sphere b s)"
   obtains c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. c)"
proof (cases "s \<le> 0")
  case True then show ?thesis
    by (meson nullhomotopic_into_contractible f contractible_sphere that)
next
  case False
  show ?thesis
  proof (cases "r \<le> 0")
    case True then show ?thesis
      by (meson f nullhomotopic_from_contractible contractible_sphere that)
  next
    case False
    with \<open>~ s \<le> 0\<close> have "r > 0" "s > 0" by auto
    show ?thesis
      apply (rule inessential_spheremap_lowdim_gen [of "cball a r" "cball b s" f])
      using  \<open>0 < r\<close> \<open>0 < s\<close> assms(1)
             apply (simp_all add: f aff_dim_cball)
      using that by blast
  qed
qed



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

lemma extending_maps_Union_aux:
  assumes fin: "finite \<F>"
      and "\<And>S. S \<in> \<F> \<Longrightarrow> closed S"
      and "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>; S \<noteq> T\<rbrakk> \<Longrightarrow> S \<inter> T \<subseteq> K"
      and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>g. continuous_on S g \<and> g ` S \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
   shows "\<exists>g. continuous_on (\<Union>\<F>) g \<and> g ` (\<Union>\<F>) \<subseteq> T \<and> (\<forall>x \<in> \<Union>\<F> \<inter> 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 \<subseteq> T" and feq: "\<forall>x \<in> S \<inter> K. f x = h x"
    by (meson insertI1)
  obtain g where contg: "continuous_on (\<Union>\<F>) g" and gim: "g ` \<Union>\<F> \<subseteq> T" and geq: "\<forall>x \<in> \<Union>\<F> \<inter> K. g x = h x"
    using insert by auto
  have fg: "f x = g x" if "x \<in> T" "T \<in> \<F>" "x \<in> S" for x T
  proof -
    have "T \<inter> S \<subseteq> K \<or> 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
  show ?case
    apply (rule_tac x="\<lambda>x. if x \<in> S then f x else g x" in exI, simp)
    apply (intro conjI continuous_on_cases)
    apply (simp_all add: insert closed_Union contf contg)
    using fim gim feq geq
    apply (force simp: insert closed_Union contf contg inf_commute intro: fg)+
    done
qed

lemma extending_maps_Union:
  assumes fin: "finite \<F>"
      and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>g. continuous_on S g \<and> g ` S \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
      and "\<And>S. S \<in> \<F> \<Longrightarrow> closed S"
      and K: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>; ~ X \<subseteq> Y; ~ Y \<subseteq> X\<rbrakk> \<Longrightarrow> X \<inter> Y \<subseteq> K"
    shows "\<exists>g. continuous_on (\<Union>\<F>) g \<and> g ` (\<Union>\<F>) \<subseteq> T \<and> (\<forall>x \<in> \<Union>\<F> \<inter> K. g x = h x)"
apply (simp add: Union_maximal_sets [OF fin, symmetric])
apply (rule extending_maps_Union_aux)
apply (simp_all add: Union_maximal_sets [OF fin] assms)
by (metis K psubsetI)


lemma extend_map_lemma:
  assumes "finite \<F>" "\<G> \<subseteq> \<F>" "convex T" "bounded T"
      and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
      and aff: "\<And>X. X \<in> \<F> - \<G> \<Longrightarrow> aff_dim X < aff_dim T"
      and face: "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>\<rbrakk> \<Longrightarrow> (S \<inter> T) face_of S \<and> (S \<inter> T) face_of T"
      and contf: "continuous_on (\<Union>\<G>) f" and fim: "f ` (\<Union>\<G>) \<subseteq> rel_frontier T"
  obtains g where "continuous_on (\<Union>\<F>) g" "g ` (\<Union>\<F>) \<subseteq> rel_frontier T" "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> g x = f x"
proof (cases "\<F> - \<G> = {}")
  case True
  then have "\<Union>\<F> \<subseteq> \<Union>\<G>"
    by (simp add: Union_mono)
  then show ?thesis
    apply (rule_tac g=f in that)
      using contf continuous_on_subset apply blast
     using fim apply blast
    by simp
next
  case False
  then have "0 \<le> 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: "\<Union>{D. D = {} \<and> P D} = {}" for P :: "'a set \<Rightarrow> bool"
    by auto
  have extendf: "\<exists>g. continuous_on (\<Union>(\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < i})) g \<and>
                     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 \<le> aff_dim T" for i::nat
  using that
  proof (induction i)
    case 0 then show ?case
      apply (simp add: Union_empty_eq)
      apply (rule_tac x=f in exI)
      apply (intro conjI)
      using contf continuous_on_subset apply blast
      using fim apply blast
      by simp
  next
    case (Suc p)
    with \<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 \<in> rel_frontier T" by auto
    have ple: "int p \<le> aff_dim T" using Suc.prems by force
    obtain h where conth: "continuous_on (\<Union>(\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < p})) h"
               and him: "h ` (\<Union> (\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < p}))
                         \<subseteq> rel_frontier T"
               and heq: "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> h x = f x"
      using Suc.IH [OF ple] by auto
    let ?Faces = "{D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D \<le> p}"
    have extendh: "\<exists>g. continuous_on D g \<and>
                       g ` D \<subseteq> 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 \<in> \<G> \<union> ?Faces" for D
    proof (cases "D \<subseteq> \<Union>(\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < p})")
      case True
      then show ?thesis
        apply (rule_tac x=h in exI)
        apply (intro conjI)
        apply (blast intro: continuous_on_subset [OF conth])
        using him apply blast
        by simp
    next
      case False
      note notDsub = False
      show ?thesis
      proof (cases "\<exists>a. D = {a}")
        case True
        then obtain a where "D = {a}" by auto
        with notDsub t show ?thesis
          by (rule_tac x="\<lambda>x. t" in exI) simp
      next
        case False
        have "D \<noteq> {}" using notDsub by auto
        have Dnotin: "D \<notin> \<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < p}"
          using notDsub by auto
        then have "D \<notin> \<G>" by simp
        have "D \<in> ?Faces - {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < p}"
          using Dnotin that by auto
        then obtain C where "C \<in> \<F>" "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]: "\<not> affine D"
          using affine_bounded_eq_trivial False \<open>D \<noteq> {}\<close> \<open>bounded D\<close> by blast
        have "{F. F facet_of D} \<subseteq> {E. E face_of C \<and> aff_dim E < int p}"
          apply clarify
          apply (metis \<open>D face_of C\<close> affD eq_iff face_of_trans facet_of_def zle_diff1_eq)
          done
        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 \<subseteq> \<Union> {E. E face_of C \<and> aff_dim E < p}"
          by (simp add: rel_frontier_of_polyhedron Union_mono)
        then have him_relf: "h ` rel_frontier D \<subseteq> 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 *: "(\<exists>c. homotopic_with (\<lambda>x. True) (rel_frontier D) (rel_frontier T) h (\<lambda>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))"
          apply (rule nullhomotopic_into_rel_frontier_extension [OF closed_rel_frontier])
          apply (simp_all add: assms rel_frontier_eq_empty him_relf)
          done
        have "(\<exists>c. homotopic_with (\<lambda>x. True) (rel_frontier D)
              (rel_frontier T) h (\<lambda>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 \<subseteq> rel_frontier T"
                        and gh: "\<And>x. x \<in> rel_frontier D \<Longrightarrow> g x = h x"
          by (metis *)
        have "D \<inter> E \<subseteq> rel_frontier D"
             if "E \<in> \<G> \<union> {D. Bex \<F> ((face_of) D) \<and> aff_dim D < int p}" for E
        proof (rule face_of_subset_rel_frontier)
          show "D \<inter> E face_of D"
            using that \<open>C \<in> \<F>\<close> \<open>D face_of C\<close> face
            apply auto
            apply (meson face_of_Int_subface \<open>\<G> \<subseteq> \<F>\<close> face_of_refl_eq poly polytope_imp_convex subsetD)
            using face_of_Int_subface apply blast
            done