Theory Further_Topology

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 
                           (xrel_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 (metis C locally connected U 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 a  C)
    then have "ball a d  U  C"
      by auto
    obtain h k where homhk: "homeomorphism (S  C) (S  C) h k"
                 and subC: "{x. (¬ (h x = x  k x = x))}  C"
                 and bou: "bounded {x. (¬ (h x = x  k x = x))}"
                 and hin: "x. x  C  K  h x  ball a d  U"
    proof (rule homeomorphism_grouping_points_exists_gen [of C "ball a d  U" "C  K" "S  C"])
      show "openin (top_of_set C) (ball a d  U)"
        by (metis open_ball C  U ball a d  U  C inf.absorb_iff2 inf.orderE inf_assoc open_openin openin_subtopology)
      show "openin (top_of_set (affine hull C)) C"
        by (metis a  C openin (top_of_set U) C affine_hull_eq affine_hull_openin all_not_in_conv affine U)
      show "ball a d  U  {}"
        using 0 < d C  U a  C by force
      show "finite (C  K)"
        by (simp add: finite K)
      show "S  C  affine hull C"
        by (metis S  U a  C affine_hull_eq affine_hull_openin assms(2) empty_iff hull_subset le_sup_iff opeUC)
      show "connected C"
        by (metis C in_components_connected)
    qed auto
    have a_BU: "a  ball a d  U"
      using 0 < d C  U a  C by auto
    have "rel_frontier (cball a d  U) retract_of (affine hull (cball a d  U) - {a})"
    proof (rule rel_frontier_retract_of_punctured_affine_hull)
      show "bounded (cball a d  U)" "convex (cball a d  U)"
        by (auto simp: convex U convex_Int)
      show "a  rel_interior (cball a d  U)"
        by (metis affine U convex_cball empty_iff interior_cball a_BU rel_interior_convex_Int_affine)
    qed
    moreover have "rel_frontier (cball a d  U) = frontier (cball a d)  U"
      by (metis a_BU affine U convex_affine_rel_frontier_Int convex_cball equals0D interior_cball)
    moreover have "affine hull (cball a d  U) = U"
      by (metis convex U a_BU affine_hull_convex_Int_nonempty_interior affine_hull_eq affine U equals0D inf.commute interior_cball)
    ultimately have "frontier (cball a d)  U retract_of (U - {a})"
      by metis
    then obtain r where contr: "continuous_on (U - {a}) r"
                    and rim: "r ` (U - {a})  sphere a d"  "r ` (U - {a})  U"
                    and req: "x. x  sphere a d  U  r x = x"
      using affine U by (force simp: retract_of_def retraction_def hull_same)
    define j where "j  λx. if x  ball a d then r x else x"
    have kj: "x. x  S  k (j x) = x"
      using C  U - S S  U ball a d  U  C j_def subC by auto
    have Uaeq: "U - {a} = (cball a d - {a})  U  (U - ball a d)"
      using 0 < d by auto
    have jim: "j ` (S  (C - {a}))  (S  C) - ball a d"
    proof clarify
      fix y  assume "y  S  (C - {a})"
      then have "y  U - {a}"
        using C  U - S S  U a  C by auto
      then have "r y  sphere a d"
        using rim by auto
      then show "j y  S  C - ball a d"
        unfolding j_def
        using r y  sphere a d y  U - {a} y  S  (C - {a}) d rim
        by (metis Diff_iff Int_iff Un_iff subsetD cball_diff_eq_sphere image_subset_iff)
    qed
    have contj: "continuous_on (U - {a}) j"
      unfolding j_def Uaeq
    proof (intro continuous_on_cases_local continuous_on_id, simp_all add: req closedin_closed Uaeq [symmetric])
      show "T. closed T  (cball a d - {a})  U = (U - {a})  T"
        using affine_closed affine U by (rule_tac x="(cball a d)  U" in exI) blast
      show "T. closed T  U - ball a d = (U - {a})  T"
        using 0 < d affine U
        by (rule_tac x="U - ball a d" in exI) (force simp: affine_closed)
      show "continuous_on ((cball a d - {a})  U) r"
        by (force intro: continuous_on_subset [OF contr])
    qed
    have fT: "x  U - K  f x  T" for x
      using fim by blast
    show ?thesis
    proof (intro conjI exI)
      show "continuous_on (S  (C - {a})) (f  k  j)"
      proof (intro continuous_on_compose)
        have "S  (C - {a})  U - {a}"
          using C  U - S S  U a  C by force
        then show "continuous_on (S  (C - {a})) j"
          by (rule continuous_on_subset [OF contj])
        have "j ` (S  (C - {a}))  S  C"
          using jim C  U - S S  U ball a d  U  C j_def by blast
        then show "continuous_on (j ` (S  (C - {a}))) k"
          by (rule continuous_on_subset [OF homeomorphism_cont2 [OF homhk]])
        show "continuous_on (k ` j ` (S  (C - {a}))) f"
        proof (clarify intro!: continuous_on_subset [OF contf])
          fix y  assume "y  S  (C - {a})"
          have ky: "k y  S  C"
            using homeomorphism_image2 [OF homhk] y  S  (C - {a}) by blast
          have jy: "j y  S  C - ball a d"
            using Un_iff y  S  (C - {a}) jim by auto
          have "k (j y)  U"
            using C  U S  U  homeomorphism_image2 [OF homhk] jy by blast
          moreover have "k (j y)  K"
            using K unfolding disjnt_iff
            by (metis DiffE Int_iff Un_iff hin homeomorphism_def homhk image_eqI jy)
          ultimately show "k (j y)  U - K"
            by blast
        qed
      qed
      have ST: "x. x  S  (f  k  j) x  T"
      proof (simp add: kj)
        show "x. x  S  f x  T"
          using K S  U fT unfolding disjnt_iff by auto
      qed
      moreover have "(f  k  j) x  T" if "x  C" "x  a" "x  S" for x
      proof -
        have rx: "r x  sphere a d"
          using C  U rim that by fastforce
        have jj: "j x  S  C - ball a d"
          using jim that by blast
        have "k (j x) = j x  k (j x)  C  j x  C"
          by (metis Diff_iff Int_iff Un_iff S  U subsetD d j_def jj rx sphere_cball that(1))
        then have kj: "k (j x)  C"
          using homeomorphism_apply2 [OF homhk, of "j x"]   C  U S  U a rx
          by (metis (mono_tags, lifting) Diff_iff subsetD jj mem_Collect_eq subC)
        then show ?thesis
          by (metis DiffE DiffI IntD1 IntI C  U comp_apply fT hin homeomorphism_apply2 homhk jj kj subset_eq)
      qed
      ultimately show "(f  k  j) ` (S  (C - {a}))  T"
        by force
      show "xS. (f  k  j) x = f x" using kj by simp
    qed (auto simp: a)
  qed
  then obtain a h where
    ah: "C. C  components (U - S); C  K  {}
            a C  C  a C  L  continuous_on (S  (C - {a C})) (h C) 
               h C ` (S  (C - {a C}))  T  (x  S. h C x = f x)"
    using that by metis
  define F where "F  {C  components (U - S). C  K  {}}"
  define G where "G  {C  components (U - S). C  K = {}}"
  define UF where "UF  (CF. C - {a C})"
  have "C0  F"
    by (auto simp: F_def C0)
  have "finite F"
  proof (subst finite_image_iff [of "λC. C  K" F, symmetric])
    show "inj_on (λC. C  K) F"
      unfolding F_def inj_on_def
      using components_nonoverlap by blast
    show "finite ((λC. C  K) ` F)"
      unfolding F_def
      by (rule finite_subset [of _ "Pow K"]) (auto simp: finite K)
  qed
  obtain g where contg: "continuous_on (S  UF) g"
             and gh: "x i. i  F; x  (S  UF)  (S  (i - {a i}))
                             g x = h i x"
  proof (rule pasting_lemma_exists_closed [OF finite F])
    let ?X = "top_of_set (S  UF)"
    show "topspace ?X  (CF. S  (C - {a C}))"
      using C0  F by (force simp: UF_def)
    show "closedin (top_of_set (S  UF)) (S  (C - {a C}))"
         if "C  F" for C
    proof (rule closedin_closed_subset [of U "S  C"])
      have "C  components (U - S)"
        using F_def that by blast
      then show "closedin (top_of_set U) (S  C)"
        by (rule closedin_Un_complement_component [OF locally connected U clo])
    next
      have "x = a C'" if "C'  F"  "x  C'" "x  U" for x C'
      proof -
        have "A. x  A  C'  A"
          using x  C' by blast
        with that show "x = a C'"
          by (metis (lifting) DiffD1 F_def Union_components mem_Collect_eq)
      qed
      then show "S  UF  U"
        using S  U by (force simp: UF_def)
    next
      show "S  (C - {a C}) = (S  C)  (S  UF)"
        using F_def UF_def components_nonoverlap that by auto
    qed
    show "continuous_map (subtopology ?X (S  (C' - {a C'}))) euclidean (h C')" if "C'  F" for C'
    proof -
      have C': "C'  components (U - S)" "C'  K  {}"
        using F_def that by blast+
      show ?thesis
        using ah [OF C'] by (auto simp: F_def subtopology_subtopology intro: continuous_on_subset)
    qed
    show "i j x. i  F; j  F;
                   x  topspace ?X  (S  (i - {a i}))  (S  (j - {a j}))
                   h i x = h j x"
      using components_eq by (fastforce simp: components_eq F_def ah)
  qed auto
  have SU': "S  G  (S  UF)  U"
    using S  U in_components_subset by (auto simp: F_def G_def UF_def)
  have clo1: "closedin (top_of_set (S  G  (S  UF))) (S  G)"
  proof (rule closedin_closed_subset [OF _ SU'])
    have *: "C. C  F  openin (top_of_set U) C"
      unfolding F_def
      by (metis (no_types, lifting) locally connected U clo closedin_def locally_connected_open_component mem_Collect_eq topspace_euclidean_subtopology)
    show "closedin (top_of_set U) (U - UF)"
      unfolding UF_def by (force intro: openin_delete *)
    have "(xF. x - {a x})  S = {}" " G  U"
      using in_components_subset by (auto simp: F_def G_def)
    moreover have " G  UF = {}"
      using components_nonoverlap by (fastforce simp: F_def G_def UF_def)
    ultimately show "S  G = (U - UF)  (S  G  (S  UF))"
      using UF_def S  U by auto
  qed
  have clo2: "closedin (top_of_set (S  G  (S  UF))) (S  UF)"
  proof (rule closedin_closed_subset [OF _ SU'])
    show "closedin (top_of_set U) (CF. S  C)"
    proof (rule closedin_Union)
      show "T. T  (∪) S ` F  closedin (top_of_set U) T"
        using F_def locally connected U clo closedin_Un_complement_component by blast
    qed (simp add: finite F)
    show "S  UF = (CF. S  C)  (S  G  (S  UF))"
    proof
      show " ((∪) S ` F)  (S   G  (S  UF))  S  UF"
        using components_eq [of _ "U-S"]
        by (auto simp add: F_def G_def UF_def disjoint_iff_not_equal)
    qed (use UF_def C0  F in blast)
  qed
  have SUG: "S  G  U - K"
    using S  U K in_components_subset[of _ "U-S"] by (force simp: G_def disjnt_iff)
  then have contf': "continuous_on (S  G) f"
    by (rule continuous_on_subset [OF contf])
  have contg': "continuous_on (S  UF) g"
    by (simp add: contg)
  have  "x. S  U; x  S  f x = g x"
    by (subst gh) (auto simp: ah C0 intro: C0  F)
  then have f_eq_g: "x. x  S  UF  x  S  G  f x = g x"
    using S  U components_eq [of _ "U-S"] by (fastforce simp add: F_def G_def UF_def)
  have cont: "continuous_on (S  G  (S  UF)) (λx. if x  S  G then f x else g x)"
    by (blast intro: continuous_on_cases_local [OF clo1 clo2 contf' contg' f_eq_g, of "λx. x  S  G"])
  show ?thesis
  proof
    have UF: "F - L  UF"
      unfolding F_def UF_def using ah by blast
    have "U - S - L = (components (U - S)) - L"
      by simp
    also have "... = F  G - L"
      unfolding F_def G_def by blast
    also have "...  UF  G"
      using UF by blast
    finally have "U - L  S  G  (S  UF)"
      by blast
    then show "continuous_on (U - L) (λx. if x  S  G then f x else g x)"
      by (rule continuous_on_subset [OF cont])
    have "((U - L)  {x. x  S  (xaG. x  xa)})   ((U - L)  (-S  UF))"
      using U - L  S  G  (S  UF) by auto
    moreover have "g ` ((U - L)  (-S  UF))  T"
    proof -
      have "g x  T" if "x  U" "x  L" "x  S" "C  F" "x  C" "x  a C" for x C
      proof (subst gh)
        show "x  (S  UF)  (S  (C - {a C}))"
          using that by (auto simp: UF_def)
        show "h C x  T"
          using ah that by (fastforce simp add: F_def)
      qed (rule that)
      then show ?thesis
        by (force simp: UF_def)
    qed
    ultimately have "g ` ((U - L)  {x. x  S  (xaG. x  xa)})  T"
      using image_mono order_trans by blast
    moreover have "f ` ((U - L)  (S  G))  T"
      using fim SUG by blast
    ultimately show "(λx. if x  S  G then f x else g x)  (U - L)  T"
       by force
    show "x. x  S  (if x  S  G then f x else g x) = f x"
      by (simp add: F_def G_def)
  qed
qed


lemma extend_map_affine_to_sphere2:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "compact S" "convex U" "bounded U" "affine T" "S  T"
      and affTU: "aff_dim T  aff_dim U"
      and contf: "continuous_on S f"
      and fim: "f  S  rel_frontier U"
      and ovlap: "C. C  components(T - S)  C  L  {}"
    obtains K g where "finite K" "K  L" "K  T" "disjnt K S"
                      "continuous_on (T - K) g" "g  (T - K)  rel_frontier U"
                      "x. x  S  g x = f x"
proof -
  obtain K g where K: "finite K" "K  T" "disjnt K S"
               and contg: "continuous_on (T - K) g"
               and gim: "g  (T - K)  rel_frontier U"
               and gf: "x. x  S  g x = f x"
     using assms extend_map_affine_to_sphere_cofinite_simple by metis
  have "(y C. C  components (T - S)  x  C  y  C  y  L)" if "x  K" for x
  proof -
    have "x  T-S"
      using K  T disjnt K S disjnt_def that by fastforce
    then obtain C where "C  components(T - S)" "x  C"
      by (metis UnionE Union_components)
    with ovlap [of C] show ?thesis
      by blast
  qed
  then obtain ξ where ξ: "x. x  K  C. C  components (T - S)  x  C  ξ x  C  ξ x  L"
    by metis
  obtain h where conth: "continuous_on (T - ξ ` K) h"
             and him: "h  (T - ξ ` K)  rel_frontier U"
             and hg: "x. x  S  h x = g x"
  proof (rule extend_map_affine_to_sphere1 [OF finite K affine T contg gim, of S "ξ ` K"])
    show cloTS: "closedin (top_of_set T) S"
      by (simp add: compact S S  T closed_subset compact_imp_closed)
    show "C. C  components (T - S); C  K  {}  C  ξ ` K  {}"
      using ξ components_eq by blast
  qed (use K in auto)
  show ?thesis
  proof
    show *: "ξ ` K  L"
      using ξ by blast
    show "finite (ξ ` K)"
      by (simp add: K)
    show "ξ ` K  T"
      by clarify (meson ξ Diff_iff contra_subsetD in_components_subset)
    show "continuous_on (T - ξ ` K) h"
      by (rule conth)
    show "disjnt (ξ ` K) S"
      using K ξ in_components_subset by (fastforce simp: disjnt_def)
  qed (simp_all add: him hg gf)
qed


proposition extend_map_affine_to_sphere_cofinite_gen:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes SUT: "compact S" "convex U" "bounded U" "affine T" "S  T"
      and aff: "aff_dim T  aff_dim U"
      and contf: "continuous_on S f"
      and fim: "f  S  rel_frontier U"
      and dis: "C. C  components(T - S); bounded C  C  L  {}"
 obtains K g where "finite K" "K  L" "K  T" "disjnt K S" "continuous_on (T - K) g"
                   "g  (T - K)  rel_frontier U"
                   "x. x  S  g x = f x"
proof (cases "S = {}")
  case True
  show ?thesis
  proof (cases "rel_frontier U = {}")
    case True
    with aff have "aff_dim T  0"
      using affine_bounded_eq_lowdim bounded U order_trans 
      by (auto simp add: rel_frontier_eq_empty)
    with aff_dim_geq [of T] consider "aff_dim T = -1" |  "aff_dim T = 0"
      by linarith
    then show ?thesis
    proof cases
      assume "aff_dim T = -1"
      then have "T = {}"
        by (simp add: aff_dim_empty)
      then show ?thesis
        by (rule_tac K="{}" in that) auto
    next
      assume "aff_dim T = 0"
      then obtain a where "T = {a}"
        using aff_dim_eq_0 by blast
      then have "a  L"
        using dis [of "{a}"] S = {} by (auto simp: in_components_self)
      with S = {} T = {a} show ?thesis
        by (rule_tac K="{a}" and g=f in that) auto
    qed
  next
    case False
    then obtain y where "y  rel_frontier U"
      by auto
    with S = {} show ?thesis
      by (rule_tac K="{}" and g="λx. y" in that)  (auto)
  qed
next
  case False
  have "bounded S"
    by (simp add: assms compact_imp_bounded)
  then obtain b where b: "S  cbox (-b) b"
    using bounded_subset_cbox_symmetric by blast
  define LU where "LU  L  ( {C  components (T - S). ¬bounded C} - cbox (-(b+One)) (b+One))"
  obtain K g where "finite K" "K  LU" "K  T" "disjnt K S"
               and contg: "continuous_on (T - K) g"
               and gim: "g ` (T - K)  rel_frontier U"
               and gf:  "x. x  S  g x = f x"
  proof (rule extend_map_affine_to_sphere2 [OF SUT aff contf fim])
    show "C  LU  {}" if "C  components (T - S)" for C
    proof (cases "bounded C")
      case True
      with dis that show ?thesis
        unfolding LU_def by fastforce
    next
      case False
      then have "¬ bounded ({C  components (T - S). ¬ bounded C})"
        by (metis (no_types, lifting) Sup_upper bounded_subset mem_Collect_eq that)
      then show ?thesis
        by (simp add: LU_def disjoint_iff) (meson False bounded_cbox bounded_subset subset_iff that)
    qed
  qed blast
  have *: False if "x  cbox (- b - m *R One) (b + m *R One)"
                   "x  box (- b - n *R One) (b + n *R One)"
                   "0  m" "m < n" "n  1" for m n x
    using that by (auto simp: mem_box algebra_simps)
  have "disjoint_family_on (λd. frontier (cbox (- b - d *R One) (b + d *R One))) {1 / 2..1}"
    by (auto simp: disjoint_family_on_def neq_iff frontier_def dest: *)
  then obtain d where d12: "1/2  d" "d  1"
                  and ddis: "disjnt K (frontier (cbox (-(b + d *R One)) (b + d *R One)))"
    using disjoint_family_elem_disjnt [of "{1/2..1::real}" K "λd. frontier (cbox (-(b + d *R One)) (b + d *R One))"]
    by (auto simp: finite K)
  define c where "c  b + d *R One"
  have cbsub: "cbox (-b) b  box (-c) c"
              "cbox (-b) b  cbox (-c) c"
              "cbox (-c) c  cbox (-(b+One)) (b+One)"
    using d12 by (simp_all add: subset_box c_def inner_diff_left inner_left_distrib)
  have clo_cT: "closed (cbox (- c) c  T)"
    using affine_closed affine T by blast
  have cT_ne: "cbox (- c) c  T  {}"
    using S  {} S  T b cbsub by fastforce
  have S_sub_cc: "S  cbox (- c) c"
    using cbox (- b) b  cbox (- c) c b by auto
  show ?thesis
  proof
    show "finite (K  cbox (-(b+One)) (b+One))"
      using finite K by blast
    show "K  cbox (- (b + One)) (b + One)  L"
      using K  LU by (auto simp: LU_def)
    show "K  cbox (- (b + One)) (b + One)  T"
      using K  T by auto
    show "disjnt (K  cbox (- (b + One)) (b + One)) S"
      using disjnt K S  by (simp add: disjnt_def disjoint_eq_subset_Compl inf.coboundedI1)
    have cloTK: "closest_point (cbox (- c) c  T) x  T - K"
                if "x  T" and Knot: "x  K  x  cbox (- b - One) (b + One)" for x
    proof (cases "x  cbox (- c) c")
      case True
      with x  T show ?thesis
        using cbsub(3) Knot  by (force simp: closest_point_self)
    next
      case False
      have clo_in_rf: "closest_point (cbox (- c) c  T) x  rel_frontier (cbox (- c) c  T)"
      proof (intro closest_point_in_rel_frontier [OF clo_cT cT_ne] DiffI notI)
        have "T  interior (cbox (- c) c)  {}"
          using S  {} S  T b cbsub(1) by fastforce
        then show "x  affine hull (cbox (- c) c  T)"
          by (simp add: Int_commute affine_hull_affine_Int_nonempty_interior affine T hull_inc that(1))
      next
        show "False" if "x  rel_interior (cbox (- c) c  T)"
        proof -
          have "interior (cbox (- c) c)  T  {}"
            using S  {} S  T b cbsub(1) by fastforce
          then have "affine hull (T  cbox (- c) c) = T"
            using affine_hull_convex_Int_nonempty_interior [of T "cbox (- c) c"]
            by (simp add: affine_imp_convex affine T inf_commute)
          then show ?thesis
            by (meson subsetD le_inf_iff rel_interior_subset that False)
        qed
      qed
      have "closest_point (cbox (- c) c  T) x  K"
      proof
        assume inK: "closest_point (cbox (- c) c  T) x  K"
        have "x. x  K  x  frontier (cbox (- (b + d *R One)) (b + d *R One))"
          by (metis ddis disjnt_iff)
        then show False
          by (metis DiffI Int_iff affine T cT_ne c_def clo_cT clo_in_rf closest_point_in_set
                    convex_affine_rel_frontier_Int convex_box(1) empty_iff frontier_cbox inK interior_cbox)
      qed
      then show ?thesis
        using cT_ne clo_cT closest_point_in_set by blast
    qed
    have "convex (cbox (- c) c  T)"
      by (simp add: affine_imp_convex assms(4) convex_Int)
    then show "continuous_on (T - K  cbox (- (b + One)) (b + One)) (g  closest_point (cbox (-c) c  T))"
      using cloTK clo_cT cT_ne
      by (intro continuous_on_compose continuous_on_closest_point continuous_on_subset [OF contg]; force)
    have "g (closest_point (cbox (- c) c  T) x)  rel_frontier U"
         if "x  T" "x  K  x  cbox (- b - One) (b + One)" for x
      using gim [THEN subsetD] that cloTK by blast
    then show "(g  closest_point (cbox (- c) c  T))  (T - K  cbox (- (b + One)) (b + One))
                rel_frontier U"
      by force
    show "x. x  S  (g  closest_point (cbox (- c) c  T)) x = f x"
      by simp (metis (mono_tags, lifting) IntI S  T cT_ne clo_cT closest_point_refl gf subsetD S_sub_cc)
  qed
qed


corollary extend_map_affine_to_sphere_cofinite:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes SUT: "compact S" "affine T" "S  T"
      and aff: "aff_dim T  DIM('b)" and "0  r"
      and contf: "continuous_on S f"
      and fim: "f  S  sphere a r"
      and dis: "C. C  components(T - S); bounded C  C  L  {}"
  obtains K g where "finite K" "K  L" "K  T" "disjnt K S" "continuous_on (T - K) g"
                    "g  (T - K)  sphere a r" "x. x  S  g x = f x"
proof (cases "r = 0")
  case True
  with fim show ?thesis
    by (rule_tac K="{}" and g = "λx. a" in that) (auto)
next
  case False
  show thesis
  proof (rule  extend_map_affine_to_sphere_cofinite_gen
      [OF compact S convex_cball bounded_cball affine T S  T _ contf])
    have "0 < r"
      using assms False by auto
    then show "aff_dim T  aff_dim (cball a r)"
      by (simp add: aff aff_dim_cball)
    show "f  S  rel_frontier (cball a r)"
      by (simp add: False fim)
  qed (use dis False that in auto)
qed

corollary extend_map_UNIV_to_sphere_cofinite:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "DIM('a)  DIM('b)" and "0  r"
      and "compact S"
      and "continuous_on S f"
      and "f  S  sphere a r"
      and "C. C  components(- S); bounded C  C  L  {}"
  obtains K g where "finite K" "K  L" "disjnt K S" "continuous_on (- K) g"
                    "g  (- K)  sphere a r" "x. x  S  g x = f x"
  using extend_map_affine_to_sphere_cofinite
        [OF compact S affine_UNIV subset_UNIV] assms
  by (metis Compl_eq_Diff_UNIV aff_dim_UNIV of_nat_le_iff)

corollary extend_map_UNIV_to_sphere_no_bounded_component:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes aff: "DIM('a)  DIM('b)" and "0  r"
      and SUT: "compact S"
      and contf: "continuous_on S f"
      and fim: "f  S  sphere a r"
      and dis: "C. C  components(- S)  ¬ bounded C"
  obtains g where "continuous_on UNIV g" "g  UNIV  sphere a r" "x. x  S  g x = f x"
  using extend_map_UNIV_to_sphere_cofinite [OF aff 0  r compact S contf fim, of "{}"]
  by (metis Compl_empty_eq dis subset_empty)


theorem Borsuk_separation_theorem_gen:
  fixes S :: "'a::euclidean_space set"
  assumes "compact S"
    shows "(c  components(- S). ¬bounded c) 
           (f. continuous_on S f  f  S  sphere (0::'a) 1
                 (c. homotopic_with_canon (λx. True) S (sphere 0 1) f (λx. c)))"
       (is "?lhs = ?rhs")
proof
  assume L [rule_format]: ?lhs
  show ?rhs
  proof clarify
    fix f :: "'a  'a"
    assume contf: "continuous_on S f" and fim: "f  S  sphere 0 1"
    obtain g where contg: "continuous_on UNIV g" and gim: "g  UNIV  sphere 0 1"
               and gf: "x. x  S  g x = f x"
      by (rule extend_map_UNIV_to_sphere_no_bounded_component [OF _ _ compact S contf fim L]) auto
    then obtain c where c: "homotopic_with_canon (λh. True) UNIV (sphere 0 1) g (λx. c)"
      by (metis contractible_UNIV nullhomotopic_from_contractible)
    then show "c. homotopic_with_canon (λx. True) S (sphere 0 1) f (λx. c)"
      by (metis assms compact_imp_closed contf contg contractible_empty fim gf gim nullhomotopic_from_contractible nullhomotopic_into_sphere_extension image_subset_iff_funcset)
  qed
next
  assume R [rule_format]: ?rhs
  show ?lhs
    unfolding components_def
  proof clarify
    fix a
    assume "a  S" and a: "bounded (connected_component_set (- S) a)"
    have "xS. norm (x - a)  0"
      using a  S by auto
    then have cont: "continuous_on S (λx. inverse(norm(x - a)) *R (x - a))"
      by (intro continuous_intros)
    have im: "(λx. inverse(norm(x - a)) *R (x - a)) ` S  sphere 0 1"
      by clarsimp (metis a  S eq_iff_diff_eq_0 left_inverse norm_eq_zero)
    show False
      using R cont im Borsuk_map_essential_bounded_component [OF compact S a  S] a by blast
  qed
qed


corollary Borsuk_separation_theorem:
  fixes S :: "'a::euclidean_space set"
  assumes "compact S" and 2: "2  DIM('a)"
    shows "connected(- S) 
           (f. continuous_on S f  f  S  sphere (0::'a) 1
                 (c. homotopic_with_canon (λx. True) S (sphere 0 1) f (λx. c)))"
       (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  show ?rhs
  proof (cases "S = {}")
    case True
    then show ?thesis
      using homotopic_with_canon_on_empty by blast
  next
    case False
    then have "(ccomponents (- S). ¬ bounded c)"
      by (metis L assms(1) bounded_empty cobounded_imp_unbounded compact_imp_bounded in_components_maximal order_refl)
    then show ?thesis
      by (simp add: Borsuk_separation_theorem_gen [OF compact S])
  qed
next
  assume R: ?rhs
  then have "ccomponents (- S). ¬ bounded c  connected (- S)"
    by (metis "2" assms(1) cobounded_has_bounded_component compact_imp_bounded double_complement)
  with R show ?lhs
    by (simp add: Borsuk_separation_theorem_gen [OF compact S])
qed


lemma homotopy_eqv_separation:
  fixes S :: "'a::euclidean_space set" and T :: "'a set"
  assumes "S homotopy_eqv T" and "compact S" and "compact T"
  shows "connected(- S)  connected(- T)"
proof -
  consider "DIM('a) = 1" | "2  DIM('a)"
    by (metis DIM_ge_Suc0 One_nat_def Suc_1 dual_order.antisym not_less_eq_eq)
  then show ?thesis
  proof cases
    case 1
    then show ?thesis
      using bounded_connected_Compl_1 compact_imp_bounded homotopy_eqv_empty1 homotopy_eqv_empty2 assms by metis
  next
    case 2
    with assms show ?thesis
      by (simp add: Borsuk_separation_theorem homotopy_eqv_cohomotopic_triviality_null)
  qed
qed

proposition Jordan_Brouwer_separation:
  fixes S :: "'a::euclidean_space set" and a::'a
  assumes hom: "S homeomorphic sphere a r" and "0 < r"
    shows "¬ connected(- S)"
proof -
  have "- sphere a r  ball a r  {}"
    using 0 < r by (simp add: Int_absorb1 subset_eq)
  moreover
  have eq: "- sphere a r - ball a r = - cball a r"
    by auto
  have "- cball a r  {}"
  proof -
    have "frontier (cball a r)  {}"
      using 0 < r by auto
    then show ?thesis
      by (metis frontier_complement frontier_empty)
  qed
  with eq have "- sphere a r - ball a r  {}"
    by auto
  moreover
  have "connected (- S) = connected (- sphere a r)"
  proof (rule homotopy_eqv_separation)
    show "S homotopy_eqv sphere a r"
      using hom homeomorphic_imp_homotopy_eqv by blast
    show "compact (sphere a r)"
      by simp
    then show " compact S"
      using hom homeomorphic_compactness by blast
  qed
  ultimately show ?thesis
    using connected_Int_frontier [of "- sphere a r" "ball a r"] by (auto simp: 0 < r)
qed


proposition Jordan_Brouwer_frontier:
  fixes S :: "'a::euclidean_space set" and a::'a
  assumes S: "S homeomorphic sphere a r" and T: "T  components(- S)" and 2: "2  DIM('a)"
    shows "frontier T = S"
proof (cases r rule: linorder_cases)
  assume "r < 0"
  with S T show ?thesis by auto
next
  assume "r = 0"
  with S T card_eq_SucD obtain b where "S = {b}"
    by (auto simp: homeomorphic_finite [of "{a}" S])
  have "components (- {b}) = { -{b}}"
    using T S = {b} by (auto simp: components_eq_sing_iff connected_punctured_universe 2)
  with T show ?thesis
    by (metis S = {b} cball_trivial frontier_cball frontier_complement singletonD sphere_trivial)
next
  assume "r > 0"
  have "compact S"
    using homeomorphic_compactness compact_sphere S by blast
  show ?thesis
  proof (rule frontier_minimal_separating_closed)
    show "closed S"
      using compact S compact_eq_bounded_closed by blast
    show "¬ connected (- S)"
      using Jordan_Brouwer_separation S 0 < r by blast
    obtain f g where hom: "homeomorphism S (sphere a r) f g"
      using S by (auto simp: homeomorphic_def)
    show "connected (- T)" if "closed T" "T  S" for T
    proof -
      have "f ` T  sphere a r"
        using T  S hom homeomorphism_image1 by blast
      moreover have "f ` T  sphere a r"
        using T  S hom
        by (metis homeomorphism_image2 homeomorphism_of_subsets order_refl psubsetE)
      ultimately have "f ` T  sphere a r" by blast
      then have "connected (- f ` T)"
        by (rule psubset_sphere_Compl_connected [OF _ 0 < r 2])
      moreover have "compact T"
        using compact S bounded_subset compact_eq_bounded_closed that by blast
      moreover then have "compact (f ` T)"
        by (meson compact_continuous_image continuous_on_subset hom homeomorphism_def psubsetE T  S)
      moreover have "T homotopy_eqv f ` T"
        by (meson f ` T  sphere a r dual_order.strict_implies_order hom homeomorphic_def homeomorphic_imp_homotopy_eqv homeomorphism_of_subsets T  S)
      ultimately show ?thesis
        using homotopy_eqv_separation [of T "f`T"] by blast
    qed
  qed (rule T)
qed

proposition Jordan_Brouwer_nonseparation:
  fixes S :: "'a::euclidean_space set" and a::'a
  assumes S: "S homeomorphic sphere a r" and "T  S" and 2: "2  DIM('a)"
    shows "connected(- T)"
proof -
  have *: "connected(C  (S - T))" if "C  components(- S)" for C
  proof (rule connected_intermediate_closure)
    show "connected C"
      using in_components_connected that by auto
    have "S = frontier C"
      using "2" Jordan_Brouwer_frontier S that by blast
    with closure_subset show "C  (S - T)  closure C"
      by (auto simp: frontier_def)
  qed auto
  have "components(- S)  {}"
    by (metis S bounded_empty cobounded_imp_unbounded compact_eq_bounded_closed compact_sphere
              components_eq_empty homeomorphic_compactness)
  then have "- T = (C  components(- S). C  (S - T))"
    using Union_components [of "-S"] T  S by auto
  moreover have "connected ..."
    using T  S by (intro connected_Union) (auto simp: *)
  ultimately show ?thesis
    by simp
qed

subsection‹ Invariance of domain and corollaries›

lemma invariance_of_domain_ball:
  fixes f :: "'a  'a::euclidean_space"
  assumes contf: "continuous_on (cball a r) f" and "0 < r"
     and inj: "inj_on f (cball a r)"
   shows "open(f ` ball a r)"
proof (cases "DIM('a) = 1")
  case True
  obtain h::"'areal" and k
    where "linear h" "linear k" "h ` UNIV = UNIV" "k ` UNIV = UNIV"
      "x. norm(h x) = norm x" "x. norm(k x) = norm x"
      and kh: "x. k(h x) = x" and "x. h(k x) = x"
  proof (rule isomorphisms_UNIV_UNIV)
    show "DIM('a) = DIM(real)"
      using True by force
  qed (metis UNIV_I UNIV_eq_I imageI)
  have cont: "continuous_on S h"  "continuous_on T k" for S T
      by (simp_all add: linear h linear k linear_continuous_on linear_linear)
    have "continuous_on (h ` cball a r) (h  f  k)"
      by (intro continuous_on_compose cont continuous_on_subset [OF contf]) (auto simp: kh)
    moreover have "is_interval (h ` cball a r)"
      by (simp add: is_interval_connected_1 linear h linear_continuous_on linear_linear connected_continuous_image)
    moreover have "inj_on (h  f  k) (h ` cball a r)"
      using inj by (simp add: inj_on_def) (metis x. k (h x) = x)
    ultimately have *: "T. open T; T  h ` cball a r  open ((h  f  k) ` T)"
      using injective_eq_1d_open_map_UNIV by blast
    have "open ((h  f  k) ` (h ` ball a r))"
      by (rule *) (auto simp: linear h range h = UNIV open_surjective_linear_image)
    then have "open ((h  f) ` ball a r)"
      by (simp add: image_comp x. k (h x) = x cong: image_cong)
    then show ?thesis
      unfolding image_comp [symmetric]
      by (metis open_bijective_linear_image_eq linear h kh range h = UNIV bijI inj_on_def)
next
  case False
  then have 2: "DIM('a)  2"
    by (metis DIM_ge_Suc0 One_nat_def Suc_1 antisym not_less_eq_eq)
  have fimsub: "f ` ball a r  - f ` sphere a r"
    using inj  by clarsimp (metis inj_onD less_eq_real_def mem_cball order_less_irrefl)
  have hom: "f ` sphere a r homeomorphic sphere a r"
    by (meson compact_sphere contf continuous_on_subset homeomorphic_compact homeomorphic_sym inj inj_on_subset sphere_cball)
  then have nconn: "¬ connected (- f ` sphere a r)"
    by (rule Jordan_Brouwer_separation) (auto simp: 0 < r)
  have "bounded (f ` sphere a r)"
    by (meson compact_imp_bounded compact_continuous_image_eq compact_sphere contf inj sphere_cball)
  then obtain C where C: "C  components (- f ` sphere a r)" and "bounded C"
    using cobounded_has_bounded_component [OF _ nconn] "2" by auto
  moreover have "f ` (ball a r) = C"
  proof
    have "C  {}"
      by (rule in_components_nonempty [OF C])
    show "C  f ` ball a r"
    proof (rule ccontr)
      assume nonsub: "¬ C  f ` ball a r"
      have "- f ` cball a r  C"
      proof (rule components_maximal [OF C])
        have "f ` cball a r homeomorphic cball a r"
          using compact_cball contf homeomorphic_compact homeomorphic_sym inj by blast
        then show "connected (- f ` cball a r)"
          by (auto intro: connected_complement_homeomorphic_convex_compact 2)
        show "- f ` cball a r  - f ` sphere a r"
          by auto
        then show "C  - f ` cball a r  {}"
          using C  {} in_components_subset [OF C] nonsub
          using image_iff by fastforce
      qed
      then have "bounded (- f ` cball a r)"
        using bounded_subset bounded C by auto
      then have "¬ bounded (f ` cball a r)"
        using cobounded_imp_unbounded by blast
      then show "False"
        using compact_continuous_image [OF contf] compact_cball compact_imp_bounded by blast
    qed
    with C  {} have "C  f ` ball a r  {}"
      by (simp add: inf.absorb_iff1)
    then show "f ` ball a r  C"
      by (metis components_maximal [OF C _ fimsub] connected_continuous_image ball_subset_cball connected_ball contf continuous_on_subset)
  qed
  moreover have "open (- f ` sphere a r)"
    using hom compact_eq_bounded_closed compact_sphere homeomorphic_compactness by blast
  ultimately show ?thesis
    using open_components by blast
qed


text‹Proved by L. E. J. Brouwer (1912)›
theorem invariance_of_domain:
  fixes f :: "'a  'a::euclidean_space"
  assumes "continuous_on S f" "open S" "inj_on f S"
    shows "open(f ` S)"
  unfolding open_subopen [of "f`S"]
proof clarify
  fix a
  assume "a  S"
  obtain δ where "δ > 0" and δ: "cball a δ  S"
    using open S a  S open_contains_cball_eq by blast
  show "T. open T  f a  T  T  f ` S"
  proof (intro exI conjI)
    show "open (f ` (ball a δ))"
      by (meson δ 0 < δ assms continuous_on_subset inj_on_subset invariance_of_domain_ball)
    show "f a  f ` ball a δ"
      by (simp add: 0 < δ)
    show "f ` ball a δ  f ` S"
      using δ ball_subset_cball by blast
  qed
qed

lemma inv_of_domain_ss0:
  fixes f :: "'a  'a::euclidean_space"
  assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U  S"
      and "subspace S" and dimS: "dim S = DIM('b::euclidean_space)"
      and ope: "openin (top_of_set S) U"
    shows "openin (top_of_set S) (f ` U)"
proof -
  have "U  S"
    using ope openin_imp_subset by blast
  have "(UNIV::'b set) homeomorphic S"
    by (simp add: subspace S dimS homeomorphic_subspaces)
  then obtain h k where homhk: "homeomorphism (UNIV::'b set) S h k"
    using homeomorphic_def by blast
  have homkh: "homeomorphism S (k ` S) k h"
    using homhk homeomorphism_image2 homeomorphism_sym by fastforce
  have "open ((k  f  h) ` k ` U)"
  proof (rule invariance_of_domain)
    show "continuous_on (k ` U) (k  f  h)"
    proof (intro continuous_intros)
      show "continuous_on (k ` U) h"
        by (meson continuous_on_subset [OF homeomorphism_cont1 [OF homhk]] top_greatest)
      have "h ` k ` U  U"
        by (metis U  S dual_order.eq_iff homeomorphism_image2 homeomorphism_of_subsets homkh)
      then show "continuous_on (h ` k ` U) f"
        by (rule continuous_on_subset [OF contf])
      have "f ` h ` k ` U  S"
        using h ` k ` U  U fim by blast
      then show "continuous_on (f ` h ` k ` U) k"
        by (rule continuous_on_subset [OF homeomorphism_cont2 [OF homhk]])
    qed
    have ope_iff: "T. open T  openin (top_of_set (k ` S)) T"
      using homhk homeomorphism_image2 open_openin by fastforce
    show "open (k ` U)"
      by (simp add: ope_iff homeomorphism_imp_open_map [OF homkh ope])
    show "inj_on (k  f  h) (k ` U)"
      by (smt (verit) comp_apply inj_on_def U  S fim homeomorphism_apply2 homhk image_iff injf subsetD)
  qed
  moreover
  have eq: "f ` U = h ` (k  f  h  k) ` U"
    unfolding image_comp [symmetric] using U  S fim
    by (metis homeomorphism_image2 homeomorphism_of_subsets homkh subset_image_iff)
  ultimately show ?thesis
    by (metis (no_types, opaque_lifting) homeomorphism_imp_open_map homhk image_comp open_openin subtopology_UNIV)
qed

lemma inv_of_domain_ss1:
  fixes f :: "'a  'a::euclidean_space"
  assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U  S"
      and "subspace S"
      and ope: "openin (top_of_set S) U"
    shows "openin (top_of_set S) (f ` U)"
proof -
  define S' where "S'  {y. x  S. orthogonal x y}"
  have "subspace S'"
    by (simp add: S'_def subspace_orthogonal_to_vectors)
  define g where "g  λz::'a*'a. ((f  fst)z, snd z)"
  have "openin (top_of_set (S × S')) (g ` (U × S'))"
  proof (rule inv_of_domain_ss0)
    show "continuous_on (U × S') g"
      unfolding  g_def
      by (auto intro!: continuous_intros continuous_on_compose2 [OF contf continuous_on_fst])
    show "g ` (U × S')  S × S'"
      using fim  by (auto simp: g_def)
    show "inj_on g (U × S')"
      using injf by (auto simp: g_def inj_on_def)
    show "subspace (S × S')"
      by (simp add: subspace S' subspace S subspace_Times)
    show "openin (top_of_set (S × S')) (U × S')"
      by (simp add: openin_Times [OF ope])
    have "dim (S × S') = dim S + dim S'"
      by (simp add: subspace S' subspace S dim_Times)
    also have "... = DIM('a)"
      using dim_subspace_orthogonal_to_vectors [OF subspace S subspace_UNIV]
      by (simp add: add.commute S'_def)
    finally show "dim (S × S') = DIM('a)" .
  qed
  moreover have "g ` (U × S') = f ` U × S'"
    by (auto simp: g_def image_iff)
  moreover have "0  S'"
    using subspace S' subspace_affine by blast
  ultimately show ?thesis
    by (auto simp: openin_Times_eq)
qed


corollary invariance_of_domain_subspaces:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes ope: "openin (top_of_set U) S"
      and "subspace U" "subspace V" and VU: "dim V  dim U"
      and contf: "continuous_on S f" and fim: "f ` S  V"
      and injf: "inj_on f S"
    shows "openin (top_of_set V) (f ` S)"
proof -
  obtain V' where "subspace V'" "V'  U" "dim V' = dim V"
    using choose_subspace_of_subspace [OF VU]
    by (metis span_eq_iff subspace U)
  then have "V homeomorphic V'"
    by (simp add: subspace V homeomorphic_subspaces)
  then obtain h k where homhk: "homeomorphism V V' h k"
    using homeomorphic_def by blast
  have eq: "f ` S = k ` (h  f) ` S"
  proof -
    have "k ` h ` f ` S = f ` S"
      by (meson fim homeomorphism_def homeomorphism_of_subsets homhk subset_refl)
    then show ?thesis
      by (simp add: image_comp)
  qed
  show ?thesis
    unfolding eq
  proof (rule homeomorphism_imp_open_map)
    show homkh: "homeomorphism V' V k h"
      by (simp add: homeomorphism_symD homhk)
    have hfV': "(h  f) ` S  V'"
      using fim homeomorphism_image1 homhk by fastforce
    moreover have "openin (top_of_set U) ((h  f) ` S)"
    proof (rule inv_of_domain_ss1)
      show "continuous_on S (h  f)"
        by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_cont1 homhk)
      show "inj_on (h  f) S"
        by (smt (verit, ccfv_SIG) comp_apply fim inj_on_def homeomorphism_apply2 [OF homkh] image_subset_iff injf)
      show "(h  f) ` S  U"
        using V'  U hfV' by auto
      qed (auto simp: assms)
    ultimately show "openin (top_of_set V') ((h  f) ` S)"
      using openin_subset_trans V'  U by force
  qed
qed

corollary invariance_of_dimension_subspaces:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes ope: "openin (top_of_set U) S"
      and "subspace U" "subspace V"
      and contf: "continuous_on S f" and fim: "f ` S  V"
      and injf: "inj_on f S" and "S  {}"
    shows "dim U  dim V"
proof -
  have "False" if "dim V < dim U"
  proof -
    obtain T where "subspace T" "T  U" "dim T = dim V"
      using choose_subspace_of_subspace [of "dim V" U]
      by (metis dim V < dim U assms(2) order.strict_implies_order span_eq_iff)
    then have "V homeomorphic T"
      by (simp add: subspace V homeomorphic_subspaces)
    then obtain h k where homhk: "homeomorphism V T h k"
      using homeomorphic_def  by blast
    have "continuous_on S (h  f)"
      by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_cont1 homhk)
    moreover have "(h  f) ` S  U"
      using T  U fim homeomorphism_image1 homhk by fastforce
    moreover have "inj_on (h  f) S"
      by (smt (verit, best) comp_apply inj_on_def fim homeomorphism_apply1 homhk image_subset_iff injf)
    ultimately have ope_hf: "openin (top_of_set U) ((h  f) ` S)"
      using invariance_of_domain_subspaces [OF ope subspace U subspace U] by blast
    have "(h  f) ` S  T"
      using fim homeomorphism_image1 homhk by fastforce
    then have "dim ((h  f) ` S)  dim T"
      by (rule dim_subset)
    also have "dim ((h  f) ` S) = dim U"
      using S  {} subspace U
      by (blast intro: dim_openin ope_hf)
    finally show False
      using dim V < dim U dim T = dim V by simp
  qed
  then show ?thesis
    using not_less by blast
qed

corollary invariance_of_domain_affine_sets:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes ope: "openin (top_of_set U) S"
      and aff: "affine U" "affine V" "aff_dim V  aff_dim U"
      and contf: "continuous_on S f" and fim: "f ` S  V"
      and injf: "inj_on f S"
    shows "openin (top_of_set V) (f ` S)"
proof (cases "S = {}")
  case True
  then show ?thesis by auto
next
  case False
  obtain a b where "a  S" "a  U" "b  V"
    using False fim ope openin_contains_cball by fastforce
  have "openin (top_of_set ((+) (- b) ` V)) (((+) (- b)  f  (+) a) ` (+) (- a) ` S)"
  proof (rule invariance_of_domain_subspaces)
    show "openin (top_of_set ((+) (- a) ` U)) ((+) (- a) ` S)"
      by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois)
    show "subspace ((+) (- a) ` U)"
      by (simp add: a  U affine_diffs_subspace_subtract affine U cong: image_cong_simp)
    show "subspace ((+) (- b) ` V)"
      by (simp add: b  V affine_diffs_subspace_subtract affine V cong: image_cong_simp)
    show "dim ((+) (- b) ` V)  dim ((+) (- a) ` U)"
      by (metis a  U b  V aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
    show "continuous_on ((+) (- a) ` S) ((+) (- b)  f  (+) a)"
      by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
    show "((+) (- b)  f  (+) a) ` (+) (- a) ` S  (+) (- b) ` V"
      using fim by auto
    show "inj_on ((+) (- b)  f  (+) a) ((+) (- a) ` S)"
      by (auto simp: inj_on_def) (meson inj_onD injf)
  qed
  then show ?thesis
    by (metis (no_types, lifting) homeomorphism_imp_open_map homeomorphism_translation image_comp translation_galois)
qed

corollary invariance_of_dimension_affine_sets:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes ope: "openin (top_of_set U) S"
      and aff: "affine U" "affine V"
      and contf: "continuous_on S f" and fim: "f ` S  V"
      and injf: "inj_on f S" and "S  {}"
    shows "aff_dim U  aff_dim V"
proof -
  obtain a b where "a  S" "a  U" "b  V"
    using S  {} fim ope openin_contains_cball by fastforce
  have "dim ((+) (- a) ` U)  dim ((+) (- b) ` V)"
  proof (rule invariance_of_dimension_subspaces)
    show "openin (top_of_set ((+) (- a) ` U)) ((+) (- a) ` S)"
      by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois)
    show "subspace ((+) (- a) ` U)"
      by (simp add: a  U affine_diffs_subspace_subtract affine U cong: image_cong_simp)
    show "subspace ((+) (- b) ` V)"
      by (simp add: b  V affine_diffs_subspace_subtract affine V cong: image_cong_simp)
    show "continuous_on ((+) (- a) ` S) ((+) (- b)  f  (+) a)"
      by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
    show "((+) (- b)  f  (+) a) ` (+) (- a) ` S  (+) (- b) ` V"
      using fim by auto
    show "inj_on ((+) (- b)  f  (+) a) ((+) (- a) ` S)"
      by (auto simp: inj_on_def) (meson inj_onD injf)
  qed (use S  {} in auto)
  then show ?thesis
    by (metis a  U b  V aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
qed

corollary invariance_of_dimension:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes contf: "continuous_on S f" and "open S"
      and injf: "inj_on f S" and "S  {}"
    shows "DIM('a)  DIM('b)"
  using invariance_of_dimension_subspaces [of UNIV S UNIV f] assms
  by auto


corollary continuous_injective_image_subspace_dim_le:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "subspace S" "subspace T"
      and contf: "continuous_on S f" and fim: "f ` S  T"
      and injf: "inj_on f S"
    shows "dim S  dim T"
  using invariance_of_dimension_subspaces [of S S _ f] assms by (auto simp: subspace_affine)

lemma invariance_of_dimension_convex_domain:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "convex S"
      and contf: "continuous_on S f" and fim: "f ` S  affine hull T"
      and injf: "inj_on f S"
    shows "aff_dim S  aff_dim T"
proof (cases "S = {}")
  case True
  then show ?thesis by (simp add: aff_dim_geq)
next
  case False
  have "aff_dim (affine hull S)  aff_dim (affine hull T)"
  proof (rule invariance_of_dimension_affine_sets)
    show "openin (top_of_set (affine hull S)) (rel_interior S)"
      by (simp add: openin_rel_interior)
    show "continuous_on (rel_interior S) f"
      using contf continuous_on_subset rel_interior_subset by blast
    show "f ` rel_interior S  affine hull T"
      using fim rel_interior_subset by blast
    show "inj_on f (rel_interior S)"
      using inj_on_subset injf rel_interior_subset by blast
    show "rel_interior S  {}"
      by (simp add: False convex S rel_interior_eq_empty)
  qed auto
  then show ?thesis
    by simp
qed


lemma homeomorphic_convex_sets_le:
  assumes "convex S" "S homeomorphic T"
  shows "aff_dim S  aff_dim T"
proof -
  obtain h k where homhk: "homeomorphism S T h k"
    using homeomorphic_def assms  by blast
  show ?thesis
  proof (rule invariance_of_dimension_convex_domain [OF convex S])
    show "continuous_on S h"
      using homeomorphism_def homhk by blast
    show "h ` S  affine hull T"
      by (metis homeomorphism_def homhk hull_subset)
    show "inj_on h S"
      by (meson homeomorphism_apply1 homhk inj_on_inverseI)
  qed
qed

lemma homeomorphic_convex_sets:
  assumes "convex S" "convex T" "S homeomorphic T"
  shows "aff_dim S = aff_dim T"
  by (meson assms dual_order.antisym homeomorphic_convex_sets_le homeomorphic_sym)

lemma homeomorphic_convex_compact_sets_eq:
  assumes "convex S" "compact S" "convex T" "compact T"
  shows "S homeomorphic T  aff_dim S = aff_dim T"
  by (meson assms homeomorphic_convex_compact_sets homeomorphic_convex_sets)

lemma invariance_of_domain_gen:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "open S" "continuous_on S f" "inj_on f S" "DIM('b)  DIM('a)"
    shows "open(f ` S)"
  using invariance_of_domain_subspaces [of UNIV S UNIV f] assms by auto

lemma injective_into_1d_imp_open_map_UNIV:
  fixes f :: "'a::euclidean_space  real"
  assumes "open T" "continuous_on S f" "inj_on f S" "T  S"
  shows "open (f ` T)"
proof -
  have "DIM(real)  DIM('a)"
    by simp
  then show ?thesis
    using invariance_of_domain_gen assms continuous_on_subset subset_inj_on by metis
qed

lemma continuous_on_inverse_open:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "open S" "continuous_on S f" "DIM('b)  DIM('a)" and gf: "x. x  S  g(f x) = x"
    shows "continuous_on (f ` S) g"
proof (clarsimp simp add: continuous_openin_preimage_eq)
  fix T :: "'a set"
  assume "open T"
  have eq: "f ` S  g -` T = f ` (S  T)"
    by (auto simp: gf)
  have "open (f ` S)"
    by (rule invariance_of_domain_gen) (use assms inj_on_inverseI in auto)
  moreover have "open (f ` (S  T))"
    using assms
    by (metis open T continuous_on_subset inj_onI inj_on_subset invariance_of_domain_gen openin_open openin_open_eq)
  ultimately show "openin (top_of_set (f ` S)) (f ` S  g -` T)"
    unfolding eq by (auto intro: open_openin_trans)
qed

lemma invariance_of_domain_homeomorphism:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "open S" "continuous_on S f" "DIM('b)  DIM('a)" "inj_on f S"
  obtains g where "homeomorphism S (f ` S) f g"
proof
  show "homeomorphism S (f ` S) f (inv_into S f)"
    by (simp add: assms continuous_on_inverse_open homeomorphism_def)
qed

corollary invariance_of_domain_homeomorphic:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "open S" "continuous_on S f" "DIM('b)  DIM('a)" "inj_on f S"
  shows "S homeomorphic (f ` S)"
  using invariance_of_domain_homeomorphism [OF assms]
  by (meson homeomorphic_def)

lemma continuous_image_subset_interior:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "continuous_on S f" "inj_on f S" "DIM('b)  DIM('a)"
  shows "f ` (interior S)  interior(f ` S)"
proof -
  have "open (f ` interior S)"
    using assms
    by (intro invariance_of_domain_gen) (auto simp: subset_inj_on interior_subset continuous_on_subset)
  then show ?thesis
    by (simp add: image_mono interior_maximal interior_subset)
qed

lemma homeomorphic_interiors_same_dimension:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "S homeomorphic T" and dimeq: "DIM('a) = DIM('b)"
  shows "(interior S) homeomorphic (interior T)"
  using assms [unfolded homeomorphic_minimal]
  unfolding homeomorphic_def
proof (clarify elim!: ex_forward)
  fix f g
  assume S: "xS. f x  T  g (f x) = x" and T: "yT. g y  S  f (g y) = y"
     and contf: "continuous_on S f" and contg: "continuous_on T g"
  then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
    by (auto simp: inj_on_def intro: rev_image_eqI) metis+
  have fim: "f ` interior S  interior T"
    using continuous_image_subset_interior [OF contf inj_on f S] dimeq fST by simp
  have gim: "g ` interior T  interior S"
    using continuous_image_subset_interior [OF contg inj_on g T] dimeq gTS by simp
  show "homeomorphism (interior S) (interior T) f g"
    unfolding homeomorphism_def
  proof (intro conjI ballI)
    show "x. x  interior S  g (f x) = x"
      by (meson xS. f x  T  g (f x) = x subsetD interior_subset)
    have "interior T  f ` interior S"
    proof
      fix x assume "x  interior T"
      then have "g x  interior S"
        using gim by blast
      then show "x  f ` interior S"
        by (metis T x  interior T image_iff interior_subset subsetCE)
    qed
    then show "f ` interior S = interior T"
      using fim by blast
    show "continuous_on (interior S) f"
      by (metis interior_subset continuous_on_subset contf)
    show "y. y  interior T  f (g y) = y"
      by (meson T subsetD interior_subset)
    have "interior S  g ` interior T"
    proof
      fix x assume "x  interior S"
      then have "f x  interior T"
        using fim by blast
      then show "x  g ` interior T"
        by (metis S x  interior S image_iff interior_subset subsetCE)
    qed
    then show "g ` interior T = interior S"
      using gim by blast
    show "continuous_on (interior T) g"
      by (metis interior_subset continuous_on_subset contg)
  qed
qed

lemma homeomorphic_open_imp_same_dimension:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "S homeomorphic T" "open S" "S  {}" "open T" "T  {}"
  shows "DIM('a) = DIM('b)"
    using assms 
    apply (simp add: homeomorphic_minimal)
    apply (rule order_antisym; metis inj_onI invariance_of_dimension)
    done

proposition homeomorphic_interiors:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "S homeomorphic T" "interior S = {}  interior T = {}"
    shows "(interior S) homeomorphic (interior T)"
proof (cases "interior T = {}")
  case False
  then have "DIM('a) = DIM('b)"
    using assms
    apply (simp add: homeomorphic_minimal)
    apply (rule order_antisym; metis continuous_on_subset inj_onI inj_on_subset interior_subset invariance_of_dimension open_interior)
    done
  then show ?thesis
    by (rule homeomorphic_interiors_same_dimension [OF S homeomorphic T])
qed (use assms in auto)

lemma homeomorphic_frontiers_same_dimension:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "S homeomorphic T" "closed S" "closed T" and dimeq: "DIM('a) = DIM('b)"
  shows "(frontier S) homeomorphic (frontier T)"
  using assms [unfolded homeomorphic_minimal]
  unfolding homeomorphic_def
proof (clarify elim!: ex_forward)
  fix f g
  assume S: "xS. f x  T  g (f x) = x" and T: "yT. g y  S  f (g y) = y"
     and contf: "continuous_on S f" and contg: "continuous_on T g"
  then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
    by (auto simp: inj_on_def intro: rev_image_eqI) metis+
  have "g ` interior T  interior S"
    using continuous_image_subset_interior [OF contg inj_on g T] dimeq gTS by simp
  then have fim: "f ` frontier S  frontier T"
    unfolding frontier_def
    using continuous_image_subset_interior assms(2) assms(3) S by auto
  have "f ` interior S  interior T"
    using continuous_image_subset_interior [OF contf inj_on f S] dimeq fST by simp
  then have gim: "g ` frontier T  frontier S"
    unfolding frontier_def
    using continuous_image_subset_interior T assms(2) assms(3) by auto
  show "homeomorphism (frontier S) (frontier T) f g"
    unfolding homeomorphism_def
  proof (intro conjI ballI)
    show gf: "x. x  frontier S  g (f x) = x"
      by (simp add: S assms(2) frontier_def)
    show fg: "y. y  frontier T  f (g y) = y"
      by (simp add: T assms(3) frontier_def)
    have "frontier T  f ` frontier S"
    proof
      fix x assume "x  frontier T"
      then have "g x  frontier S"
        using gim by blast
      then show "x  f ` frontier S"
        by (metis fg x  frontier T imageI)
    qed
    then show "f ` frontier S = frontier T"
      using fim by blast
    show "continuous_on (frontier S) f"
      by (metis Diff_subset assms(2) closure_eq contf continuous_on_subset frontier_def)
    have "frontier S  g ` frontier T"
    proof
      fix x assume "x  frontier S"
      then have "f x  frontier T"
        using fim by blast
      then show "x  g ` frontier T"
        by (metis gf x  frontier S imageI)
    qed
    then show "g ` frontier T = frontier S"
      using gim by blast
    show "continuous_on (frontier T) g"
      by (metis Diff_subset assms(3) closure_closed contg continuous_on_subset frontier_def)
  qed
qed

lemma homeomorphic_frontiers:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "S homeomorphic T" "closed S" "closed T"
          "interior S = {}  interior T = {}"
    shows "(frontier S) homeomorphic (frontier T)"
proof (cases "interior T = {}")
  case True
  then show ?thesis
    by (metis Diff_empty assms closure_eq frontier_def)
next
  case False
  then have "DIM('a) = DIM('b)"
    using assms homeomorphic_interiors homeomorphic_open_imp_same_dimension by blast
  then show ?thesis
    using assms homeomorphic_frontiers_same_dimension by blast
qed

lemma continuous_image_subset_rel_interior:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S  T"
      and TS: "aff_dim T  aff_dim S"
  shows "f ` (rel_interior S)  rel_interior(f ` S)"
proof (rule rel_interior_maximal)
  show "f ` rel_interior S  f ` S"
    by(simp add: image_mono rel_interior_subset)
  show "openin (top_of_set (affine hull f ` S)) (f ` rel_interior S)"
  proof (rule invariance_of_domain_affine_sets)
    show "openin (top_of_set (affine hull S)) (rel_interior S)"
      by (simp add: openin_rel_interior)
    show "aff_dim (affine hull f ` S)  aff_dim (affine hull S)"
      by (metis aff_dim_affine_hull aff_dim_subset fim TS order_trans)
    show "f ` rel_interior S  affine hull f ` S"
      by (meson f ` rel_interior S  f ` S hull_subset order_trans)
    show "continuous_on (rel_interior S) f"
      using contf continuous_on_subset rel_interior_subset by blast
    show "inj_on f (rel_interior S)"
      using inj_on_subset injf rel_interior_subset by blast
  qed auto
qed

lemma homeomorphic_rel_interiors_same_dimension:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T"
  shows "(rel_interior S) homeomorphic (rel_interior T)"
  using assms [unfolded homeomorphic_minimal]
  unfolding homeomorphic_def
proof (clarify elim!: ex_forward)
  fix f g
  assume S: "xS. f x  T  g (f x) = x" and T: "yT. g y  S  f (g y) = y"
     and contf: "continuous_on S f" and contg: "continuous_on T g"
  then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
    by (auto simp: inj_on_def intro: rev_image_eqI) metis+
  have fim: "f ` rel_interior S  rel_interior T"
    by (metis inj_on f S aff contf continuous_image_subset_rel_interior fST order_refl)
  have gim: "g ` rel_interior T  rel_interior S"
    by (metis inj_on g T aff contg continuous_image_subset_rel_interior gTS order_refl)
  show "homeomorphism (rel_interior S) (rel_interior T) f g"
    unfolding homeomorphism_def
  proof (intro conjI ballI)
    show gf: "x. x  rel_interior S  g (f x) = x"
      using S rel_interior_subset by blast
    show fg: "y. y  rel_interior T  f (g y) = y"
      using T mem_rel_interior_ball by blast
    have "rel_interior T  f ` rel_interior S"
    proof
      fix x assume "x  rel_interior T"
      then have "g x  rel_interior S"
        using gim by blast
      then show "x  f ` rel_interior S"
        by (metis fg x  rel_interior T imageI)
    qed
    moreover have "f ` rel_interior S  rel_interior T"
      by (metis inj_on f S aff contf continuous_image_subset_rel_interior fST order_refl)
    ultimately show "f ` rel_interior S = rel_interior T"
      by blast
    show "continuous_on (rel_interior S) f"
      using contf continuous_on_subset rel_interior_subset by blast
    have "rel_interior S  g ` rel_interior T"
    proof
      fix x assume "x  rel_interior S"
      then have "f x  rel_interior T"
        using fim by blast
      then show "x  g ` rel_interior T"
        by (metis gf x  rel_interior S imageI)
    qed
    then show "g ` rel_interior T = rel_interior S"
      using gim by blast
    show "continuous_on (rel_interior T) g"
      using contg continuous_on_subset rel_interior_subset by blast
  qed
qed


lemma homeomorphic_aff_dim_le:
  fixes S :: "'a::euclidean_space set" 
  assumes "S homeomorphic T" "rel_interior S  {}"
    shows "aff_dim (affine hull S)  aff_dim (affine hull T)"
proof -
  obtain f g
    where S: "xS. f x  T  g (f x) = x" and T: "yT. g y  S  f (g y) = y"
      and contf: "continuous_on S f" and contg: "continuous_on T g"
    using assms [unfolded homeomorphic_minimal] by auto
  show ?thesis
  proof (rule invariance_of_dimension_affine_sets)
    show "continuous_on (rel_interior S) f"
      using contf continuous_on_subset rel_interior_subset by blast
    show "f ` rel_interior S  affine hull T"
      by (meson S hull_subset image_subsetI rel_interior_subset rev_subsetD)
    show "inj_on f (rel_interior S)"
      by (metis S inj_on_inverseI inj_on_subset rel_interior_subset)
  qed (simp_all add: openin_rel_interior assms)
qed

lemma homeomorphic_rel_interiors:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "S homeomorphic T" "rel_interior S = {}  rel_interior T = {}"
    shows "(rel_interior S) homeomorphic (rel_interior T)"
proof (cases "rel_interior T = {}")
  case True
  with assms show ?thesis by auto
next
  case False
  have "aff_dim (affine hull S)  aff_dim (affine hull T)"
    using False assms homeomorphic_aff_dim_le by blast
  moreover have "aff_dim (affine hull T)  aff_dim (affine hull S)"
    using False assms(1) homeomorphic_aff_dim_le homeomorphic_sym by auto
  ultimately have "aff_dim S = aff_dim T" by force
  then show ?thesis
    by (rule homeomorphic_rel_interiors_same_dimension [OF S homeomorphic T])
qed


lemma homeomorphic_rel_boundaries_same_dimension:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T"
  shows "(S - rel_interior S) homeomorphic (T - rel_interior T)"
  using assms [unfolded homeomorphic_minimal]
  unfolding homeomorphic_def
proof (clarify elim!: ex_forward)
  fix f g
  assume S: "xS. f x  T  g (f x) = x" and T: "yT. g y  S  f (g y) = y"
     and contf: "continuous_on S f" and contg: "continuous_on T g"
  then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
    by (auto simp: inj_on_def intro: rev_image_eqI) metis+
  have fim: "f ` rel_interior S  rel_interior T"
    by (metis inj_on f S aff contf continuous_image_subset_rel_interior fST order_refl)
  have gim: "g ` rel_interior T  rel_interior S"
    by (metis inj_on g T aff contg continuous_image_subset_rel_interior gTS order_refl)
  show "homeomorphism (S - rel_interior S) (T - rel_interior T) f g"
    unfolding homeomorphism_def
  proof (intro conjI ballI)
    show gf: "x. x  S - rel_interior S  g (f x) = x"
      using S rel_interior_subset by blast
    show fg: "y. y  T - rel_interior T  f (g y) = y"
      using T mem_rel_interior_ball by blast
    show "f ` (S - rel_interior S) = T - rel_interior T"
      using S fST fim gim by auto
    show "continuous_on (S - rel_interior S) f"
      using contf continuous_on_subset rel_interior_subset by blast
    show "g ` (T - rel_interior T) = S - rel_interior S"
      using T gTS gim fim by auto
    show "continuous_on (T - rel_interior T) g"
      using contg continuous_on_subset rel_interior_subset by blast
  qed
qed

lemma homeomorphic_rel_boundaries:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "S homeomorphic T" "rel_interior S = {}  rel_interior T = {}"
    shows "(S - rel_interior S) homeomorphic (T - rel_interior T)"
proof (cases "rel_interior T = {}")
  case True
  with assms show ?thesis by auto
next
  case False
  obtain f g
    where S: "xS. f x  T  g (f x) = x" and T: "yT. g y  S  f (g y) = y"
      and contf: "continuous_on S f" and contg: "continuous_on T g"
    using assms by (auto simp: homeomorphic_minimal)
  have "aff_dim (affine hull S)  aff_dim (affine hull T)"
    using False assms homeomorphic_aff_dim_le by blast
  moreover have "aff_dim (affine hull T)  aff_dim (affine hull S)"
    by (meson False assms(1) homeomorphic_aff_dim_le homeomorphic_sym)
  ultimately have "aff_dim S = aff_dim T" by force
  then show ?thesis
    by (rule homeomorphic_rel_boundaries_same_dimension [OF S homeomorphic T])
qed

proposition uniformly_continuous_homeomorphism_UNIV_trivial:
  fixes f :: "'a::euclidean_space  'a"
  assumes contf: "uniformly_continuous_on S f" and hom: "homeomorphism S UNIV f g"
  shows "S = UNIV"
proof (cases "S = {}")
  case True
  then show ?thesis
    by (metis UNIV_I hom empty_iff homeomorphism_def image_eqI)
next
  case False
  have "inj g"
    by (metis UNIV_I hom homeomorphism_apply2 injI)
  then have "open (g ` UNIV)"
    by (blast intro: invariance_of_domain hom homeomorphism_cont2)
  then have "open S"
    using hom homeomorphism_image2 by blast
  moreover have "complete S"
    unfolding complete_def
  proof clarify
    fix σ
    assume σ: "n. σ n  S" and "Cauchy σ"
    have "Cauchy (f o σ)"
      using uniformly_continuous_imp_Cauchy_continuous Cauchy σ σ contf
      unfolding Cauchy_continuous_on_def by blast
    then obtain l where "(f  σ)  l"
      by (auto simp: convergent_eq_Cauchy [symmetric])
    show "lS. σ  l"
    proof
      show "g l  S"
        using hom homeomorphism_image2 by blast
      have "(g  (f  σ))  g l"
        by (meson UNIV_I (f  σ)  l continuous_on_sequentially hom homeomorphism_cont2)
      then show "σ  g l"
      proof -
        have "n. σ n = (g  (f  σ)) n"
          by (metis (no_types) σ comp_eq_dest_lhs hom homeomorphism_apply1)
        then show ?thesis
          by (metis (no_types) LIMSEQ_iff (g  (f  σ))  g l)
      qed
    qed
  qed
  then have "closed S"
    by (simp add: complete_eq_closed)
  ultimately show ?thesis
    using clopen [of S] False  by simp
qed

subsection‹Formulation of loop homotopy in terms of maps out of type complex›

lemma homotopic_circlemaps_imp_homotopic_loops:
  assumes "homotopic_with_canon (λh. True) (sphere 0 1) S f g"
   shows "homotopic_loops S (f  exp  (λt. 2 * of_real pi * of_real t * 𝗂))
                            (g  exp  (λt. 2 * of_real pi * of_real t * 𝗂))"
proof -
  have "homotopic_with_canon (λf. True) {z. cmod z = 1} S f g"
    using assms by (auto simp: sphere_def)
  moreover have "continuous_on {0..1} (exp  (λt. 2 * of_real pi * of_real t * 𝗂))"
     by (intro continuous_intros)
  moreover have "(exp  (λt. 2 * of_real pi * of_real t * 𝗂)) ` {0..1}  {z. cmod z = 1}"
    by (auto simp: norm_mult)
  ultimately
  show ?thesis
    apply (simp add: homotopic_loops_def comp_assoc)
    apply (rule homotopic_with_compose_continuous_right)
      apply (auto simp: pathstart_def pathfinish_def)
    done
qed

lemma homotopic_loops_imp_homotopic_circlemaps:
  assumes "homotopic_loops S p q"
    shows "homotopic_with_canon (λh. True) (sphere 0 1) S
                          (p  (λz. (Arg2pi z / (2 * pi))))
                          (q  (λz. (Arg2pi z / (2 * pi))))"
proof -
  obtain h where conth: "continuous_on ({0..1::real} × {0..1}) h"
             and him: "h ` ({0..1} × {0..1})  S"
             and h0: "(x. h (0, x) = p x)"
             and h1: "(x. h (1, x) = q x)"
             and h01: "(t{0..1}. h (t, 1) = h (t, 0)) "
    using assms
    by (auto simp: homotopic_loops_def sphere_def homotopic_with_def pathstart_def pathfinish_def)
  define j where "j  λz. if 0  Im (snd z)
                          then h (fst z, Arg2pi (snd z) / (2 * pi))
                          else h (fst z, 1 - Arg2pi (cnj (snd z)) / (2 * pi))"
  have Arg2pi_eq: "1 - Arg2pi (cnj y) / (2 * pi) = Arg2pi y / (2 * pi)  Arg2pi y = 0  Arg2pi (cnj y) = 0" if "cmod y = 1" for y
    using that Arg2pi_eq_0_pi Arg2pi_eq_pi by (force simp: Arg2pi_cnj field_split_simps)
  show ?thesis
  proof (simp add: homotopic_with; intro conjI ballI exI)
    show "continuous_on ({0..1} × sphere 0 1) (λw. h (fst w, Arg2pi (snd w) / (2 * pi)))"
    proof (rule continuous_on_eq)
      show j: "j x = h (fst x, Arg2pi (snd x) / (2 * pi))" if "x  {0..1} × sphere 0 1" for x
        using Arg2pi_eq that h01 by (force simp: j_def)
      have eq:  "S = S  (UNIV × {z. 0  Im z})  S  (UNIV × {z. Im z  0})" for S :: "(real*complex)set"
        by auto
      have §: "Arg2pi z  2 * pi" for z
        by (simp add: Arg2pi order_le_less)
      have c1: "continuous_on ({0..1} × sphere 0 1  UNIV × {z. 0  Im z}) (λx. h (fst x, Arg2pi (snd x) / (2 * pi)))"
        apply (intro continuous_intros continuous_on_compose2 [OF conth]  continuous_on_compose2 [OF continuous_on_upperhalf_Arg2pi])
        by (auto simp: Arg2pi §)
      have c2: "continuous_on ({0..1} × sphere 0 1  UNIV × {z. Im z  0}) (λx. h (fst x, 1 - Arg2pi (cnj (snd x)) / (2 * pi)))"
        apply (intro continuous_intros continuous_on_compose2 [OF conth]  continuous_on_compose2 [OF continuous_on_upperhalf_Arg2pi])
        by (auto simp: Arg2pi §)
      show "continuous_on ({0..1} × sphere 0 1) j"
        apply (simp add: j_def)
        apply (subst eq)
        apply (rule continuous_on_cases_local)
        using Arg2pi_eq h01
        by (force simp add: eq [symmetric] closedin_closed_Int closed_Times closed_halfspace_Im_le closed_halfspace_Im_ge c1 c2)+
    qed
    have "(λw. h (fst w, Arg2pi (snd w) / (2 * pi))) ` ({0..1} × sphere 0 1)  h ` ({0..1} × {0..1})"
      by (auto simp: Arg2pi_ge_0 Arg2pi_lt_2pi less_imp_le)
    also have "...  S"
      using him by blast
    finally show "(λw. h (fst w, Arg2pi (snd w) / (2 * pi))) ` ({0..1} × sphere 0 1)  S" .
  qed (auto simp: h0 h1)
qed

lemma simply_connected_homotopic_loops:
  "simply_connected S 
       (p q. homotopic_loops S p p  homotopic_loops S q q  homotopic_loops S p q)"
unfolding simply_connected_def using homotopic_loops_refl by metis


lemma simply_connected_eq_homotopic_circlemaps1:
  fixes f :: "complex  'a::topological_space" and g :: "complex  'a"
  assumes S: "simply_connected S"
      and contf: "continuous_on (sphere 0 1) f" and fim: "f ` (sphere 0 1)  S"
      and contg: "continuous_on (sphere 0 1) g" and gim: "g ` (sphere 0 1)  S"
    shows "homotopic_with_canon (λh. True) (sphere 0 1) S f g"
proof -
  let ?h = "(λt. complex_of_real (2 * pi * t) * 𝗂)"
  have "homotopic_loops S (f  exp  ?h) (f  exp  ?h)  homotopic_loops S (g  exp  ?h) (g  exp  ?h)"
    by (simp add: homotopic_circlemaps_imp_homotopic_loops contf fim contg gim)
  then have "homotopic_loops S (f  exp  ?h) (g  exp  ?h)"
    using S simply_connected_homotopic_loops by blast
  then show ?thesis
    apply (rule homotopic_with_eq [OF homotopic_loops_imp_homotopic_circlemaps])
      apply (auto simp: o_def complex_norm_eq_1_exp mult.commute)
    done
qed

lemma simply_connected_eq_homotopic_circlemaps2a:
  fixes h :: "complex  'a::topological_space"
  assumes conth: "continuous_on (sphere 0 1) h" and him: "h ` (sphere 0 1)  S"
      and hom: "f g::complex  'a.
                continuous_on (sphere 0 1) f; f ` (sphere 0 1)  S;
                continuous_on (sphere 0 1) g; g ` (sphere 0 1)  S
                 homotopic_with_canon (λh. True) (sphere 0 1) S f g"
            shows "a. homotopic_with_canon (λh. True) (sphere 0 1) S h (λx. a)"
  by (metis conth continuous_on_const him hom image_subset_iff)

lemma simply_connected_eq_homotopic_circlemaps2b:
  fixes S :: "'a::real_normed_vector set"
  assumes "f g::complex  'a.
                continuous_on (sphere 0 1) f; f ` (sphere 0 1)  S;
                continuous_on (sphere 0 1) g; g ` (sphere 0 1)  S
                 homotopic_with_canon (λh. True) (sphere 0 1) S f g"
  shows "path_connected S"
proof (clarsimp simp add: path_connected_eq_homotopic_points)
  fix a b
  assume "a  S" "b  S"
  then show "homotopic_loops S (linepath a a) (linepath b b)"
    using homotopic_circlemaps_imp_homotopic_loops [OF assms [of "λx. a" "λx. b"]]
    by (auto simp: o_def linepath_def)
qed

lemma simply_connected_eq_homotopic_circlemaps3:
  fixes h :: "complex  'a::real_normed_vector"
  assumes "path_connected S"
      and hom: "f::complex  'a.
                  continuous_on (sphere 0 1) f; f `(sphere 0 1)  S
                   a. homotopic_with_canon (λh. True) (sphere 0 1) S f (λx. a)"
    shows "simply_connected S"
proof (clarsimp simp add: simply_connected_eq_contractible_loop_some assms)
  fix p
  assume p: "path p" "path_image p  S" "pathfinish p = pathstart p"
  then have "homotopic_loops S p p"
    by (simp add: homotopic_loops_refl)
  then obtain a where homp: "homotopic_with_canon (λh. True) (sphere 0 1) S (p  (λz. Arg2pi z / (2 * pi))) (λx. a)"
    by (metis homotopic_with_imp_subset2 homotopic_loops_imp_homotopic_circlemaps homotopic_with_imp_continuous hom)
  show "a. a  S  homotopic_loops S p (linepath a a)"
  proof (intro exI conjI)
    show "a  S"
      using homotopic_with_imp_subset2 [OF homp]
      by (metis dist_0_norm image_subset_iff mem_sphere norm_one)
    have teq: "t. 0  t; t  1
                t = Arg2pi (exp (2 * of_real pi * of_real t * 𝗂)) / (2 * pi)  t=1  Arg2pi (exp (2 * of_real pi * of_real t * 𝗂)) = 0"
      using Arg2pi_of_real [of 1] by (force simp: Arg2pi_exp)
    have "homotopic_loops S p (p  (λz. Arg2pi z / (2 * pi))  exp  (λt. 2 * complex_of_real pi * complex_of_real t * 𝗂))"
      using p teq by (fastforce simp: pathfinish_def pathstart_def intro: homotopic_loops_eq [OF p])
    then show "homotopic_loops S p (linepath a a)"
      by (simp add: linepath_refl  homotopic_loops_trans [OF _ homotopic_circlemaps_imp_homotopic_loops [OF homp, simplified K_record_comp]])
  qed
qed


proposition simply_connected_eq_homotopic_circlemaps:
  fixes S :: "'a::real_normed_vector set"
  shows "simply_connected S 
         (f g::complex  'a.
              continuous_on (sphere 0 1) f  f ` (sphere 0 1)  S 
              continuous_on (sphere 0 1) g  g ` (sphere 0 1)  S
               homotopic_with_canon (λh. True) (sphere 0 1) S f g)"
  by (metis simply_connected_eq_homotopic_circlemaps1 simply_connected_eq_homotopic_circlemaps2a 
      simply_connected_eq_homotopic_circlemaps2b simply_connected_eq_homotopic_circlemaps3)

proposition simply_connected_eq_contractible_circlemap:
  fixes S :: "'a::real_normed_vector set"
  shows "simply_connected S 
         path_connected S 
         (f::complex  'a.
              continuous_on (sphere 0 1) f  f `(sphere 0 1)  S
               (a. homotopic_with_canon (λh. True) (sphere 0 1) S f (λx. a)))"
  by (metis simply_connected_eq_homotopic_circlemaps simply_connected_eq_homotopic_circlemaps2a 
      simply_connected_eq_homotopic_circlemaps3 simply_connected_imp_path_connected)

corollary homotopy_eqv_simple_connectedness:
  fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
  shows "S homotopy_eqv T  simply_connected S  simply_connected T"
  by (simp add: simply_connected_eq_homotopic_circlemaps homotopy_eqv_homotopic_triviality image_subset_iff_funcset)


subsection‹Homeomorphism of simple closed curves to circles›

proposition homeomorphic_simple_path_image_circle:
  fixes a :: complex and γ :: "real  'a::t2_space"
  assumes "simple_path γ" and loop: "pathfinish γ = pathstart γ" and "0 < r"
  shows "(path_image γ) homeomorphic sphere a r"
proof -
  have "homotopic_loops (path_image γ) γ γ"
    by (simp add: assms homotopic_loops_refl simple_path_imp_path)
  then have hom: "homotopic_with_canon (λh. True) (sphere 0 1) (path_image γ)
               (γ  (λz. Arg2pi z / (2*pi))) (γ  (λz. Arg2pi z / (2*pi)))"
    by (rule homotopic_loops_imp_homotopic_circlemaps)
  have "g. homeomorphism (sphere 0 1) (path_image γ) (γ  (λz. Arg2pi z / (2*pi))) g"
  proof (rule homeomorphism_compact)
    show "continuous_on (sphere 0 1) (γ  (λz. Arg2pi z / (2*pi)))"
      using hom homotopic_with_imp_continuous by blast
    show "inj_on (γ  (λz. Arg2pi z / (2*pi))) (sphere 0 1)"
    proof
      fix x y
      assume xy: "x  sphere 0 1" "y  sphere 0 1"
         and eq: "(γ  (λz. Arg2pi z / (2*pi))) x = (γ  (λz. Arg2pi z / (2*pi))) y"
      then have "(Arg2pi x / (2*pi)) = (Arg2pi y / (2*pi))"
      proof -
        have "(Arg2pi x / (2*pi))  {0..1}" "(Arg2pi y / (2*pi))  {0..1}"
          using Arg2pi_ge_0 Arg2pi_lt_2pi dual_order.strict_iff_order by fastforce+
        with eq show ?thesis
          using simple_path γ Arg2pi_lt_2pi 
          unfolding simple_path_def loop_free_def o_def
          by (metis eq_divide_eq_1 not_less_iff_gr_or_eq)
      qed
      with xy show "x = y"
        by (metis is_Arg_def Arg2pi Arg2pi_0 dist_0_norm divide_cancel_right dual_order.strict_iff_order mem_sphere)
    qed
    have "z. cmod z = 1  x{0..1}. γ (Arg2pi z / (2*pi)) = γ x"
       by (metis Arg2pi_ge_0 Arg2pi_lt_2pi atLeastAtMost_iff divide_less_eq_1 less_eq_real_def zero_less_mult_iff pi_gt_zero zero_le_divide_iff zero_less_numeral)
     moreover have "zsphere 0 1. γ x = γ (Arg2pi z / (2*pi))" if "0  x" "x  1" for x
     proof (cases "x=1")
       case True
       with Arg2pi_of_real [of 1] loop show ?thesis
         by (rule_tac x=1 in bexI) (auto simp: pathfinish_def pathstart_def 0  x)
     next
       case False
       then have *: "(Arg2pi (exp (𝗂*(2* of_real pi* of_real x))) / (2*pi)) = x"
         using that by (auto simp: Arg2pi_exp field_split_simps)
       show ?thesis
         by (rule_tac x="exp(𝗂 * of_real(2*pi*x))" in bexI) (auto simp: *)
    qed
    ultimately show "(γ  (λz. Arg2pi z / (2*pi))) ` sphere 0 1 = path_image γ"
      by (auto simp: path_image_def image_iff)
    qed auto
    then have "path_image γ homeomorphic sphere (0::complex) 1"
      using homeomorphic_def homeomorphic_sym by blast
  also have "... homeomorphic sphere a r"
    by (simp add: assms homeomorphic_spheres)
  finally show ?thesis .
qed

lemma homeomorphic_simple_path_images:
  fixes γ1 :: "real  'a::t2_space" and γ2 :: "real  'b::t2_space"
  assumes "simple_path γ1" and loop: "pathfinish γ1 = pathstart γ1"
  assumes "simple_path γ2" and loop: "pathfinish γ2 = pathstart γ2"
  shows "(path_image γ1) homeomorphic (path_image γ2)"
  by (meson assms homeomorphic_simple_path_image_circle homeomorphic_sym homeomorphic_trans loop pi_gt_zero)

subsection‹Dimension-based conditions for various homeomorphisms›

lemma homeomorphic_subspaces_eq:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "subspace S" "subspace T"
  shows "S homeomorphic T  dim S = dim T"
proof
  assume "S homeomorphic T"
  then obtain f g where hom: "homeomorphism S T f g"
    using homeomorphic_def by blast
  show "dim S = dim T"
  proof (rule order_antisym)
    show "dim S  dim T"
      by (metis assms dual_order.refl inj_onI homeomorphism_cont1 [OF hom] homeomorphism_apply1 [OF hom] homeomorphism_image1 [OF hom] continuous_injective_image_subspace_dim_le)
    show "dim T  dim S"
      by (metis assms dual_order.refl inj_onI homeomorphism_cont2 [OF hom] homeomorphism_apply2 [OF hom] homeomorphism_image2 [OF hom] continuous_injective_image_subspace_dim_le)
  qed
next
  assume "dim S = dim T"
  then show "S homeomorphic T"
    by (simp add: assms homeomorphic_subspaces)
qed

lemma homeomorphic_affine_sets_eq:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "affine S" "affine T"
  shows "S homeomorphic T  aff_dim S = aff_dim T"
proof (cases "S = {}  T = {}")
  case True
  then show ?thesis
    using assms homeomorphic_affine_sets by force
next
  case False
  then obtain a b where "a  S" "b  T"
    by blast
  then have "subspace ((+) (- a) ` S)" "subspace ((+) (- b) ` T)"
    using affine_diffs_subspace assms by blast+
  then show ?thesis
    by (metis affine_imp_convex assms homeomorphic_affine_sets homeomorphic_convex_sets)
qed

lemma homeomorphic_hyperplanes_eq:
  fixes a :: "'a::euclidean_space" and c :: "'b::euclidean_space"
  assumes "a  0" "c  0"
  shows "({x. a  x = b} homeomorphic {x. c  x = d}  DIM('a) = DIM('b))"
proof -
  have "DIM('a) - Suc 0 = DIM('b) - Suc 0  DIM('a) = DIM('b)"
    by (metis DIM_positive Suc_pred)
  then show ?thesis
    by (auto simp: homeomorphic_affine_sets_eq affine_hyperplane assms)
qed

lemma homeomorphic_UNIV_UNIV:
  shows "(UNIV::'a set) homeomorphic (UNIV::'b set) 
    DIM('a::euclidean_space) = DIM('b::euclidean_space)"
  by (simp add: homeomorphic_subspaces_eq)

lemma simply_connected_sphere_gen:
   assumes "convex S" "bounded S" and 3: "3  aff_dim S"
   shows "simply_connected(rel_frontier S)"
proof -
  have pa: "path_connected (rel_frontier S)"
    using assms by (simp add: path_connected_sphere_gen)
  show ?thesis
  proof (clarsimp simp add: simply_connected_eq_contractible_circlemap pa)
    fix f
    assume f: "continuous_on (sphere (0::complex) 1) f" "f ` sphere 0 1  rel_frontier S"
    have eq: "sphere (0::complex) 1 = rel_frontier(cball 0 1)"
      by simp
    have "convex (cball (0::complex) 1)"
      by (rule convex_cball)
    then obtain c where "homotopic_with_canon (λz. True) (sphere (0::complex) 1) (rel_frontier S) f (λx. c)"
      apply (rule inessential_spheremap_lowdim_gen [OF _ bounded_cball convex S bounded S, where f=f])
      using f 3 by (auto simp: aff_dim_cball)
    then show "a. homotopic_with_canon (λh. True) (sphere 0 1) (rel_frontier S) f (λx. a)"
      by blast
  qed
qed

subsection‹more invariance of domain›(*FIX ME title? *)

proposition invariance_of_domain_sphere_affine_set_gen:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S  T"
      and U: "bounded U" "convex U"
      and "affine T" and affTU: "aff_dim T < aff_dim U"
      and ope: "openin (top_of_set (rel_frontier U)) S"
   shows "openin (top_of_set T) (f ` S)"
proof (cases "rel_frontier U = {}")
  case True
  then show ?thesis
    using ope openin_subset by force
next
  case False
  obtain b c where b: "b  rel_frontier U" and c: "c  rel_frontier U" and "b  c"
    using bounded U rel_frontier_not_sing [of U] subset_singletonD False  by fastforce
  obtain V :: "'a set" where "affine V" and affV: "aff_dim V = aff_dim U - 1"
  proof (rule choose_affine_subset [OF affine_UNIV])
    show "- 1  aff_dim U - 1"
      by (metis aff_dim_empty aff_dim_geq aff_dim_negative_iff affTU diff_0 diff_right_mono not_le)
    show "aff_dim U - 1  aff_dim (UNIV::'a set)"
      by (metis aff_dim_UNIV aff_dim_le_DIM le_cases not_le zle_diff1_eq)
  qed auto
  have SU: "S  rel_frontier U"
    using ope openin_imp_subset by auto
  have homb: "rel_frontier U - {b} homeomorphic V"
   and homc: "rel_frontier U - {c} homeomorphic V"
    using homeomorphic_punctured_sphere_affine_gen [of U _ V]
    by (simp_all add: affine V affV U b c)
  then obtain g h j k
           where gh: "homeomorphism (rel_frontier U - {b}) V g h"
             and jk: "homeomorphism (rel_frontier U - {c}) V j k"
    by (auto simp: homeomorphic_def)
  with SU have hgsub: "(h ` g ` (S - {b}))  S" and kjsub: "(k ` j ` (S - {c}))  S"
    by (simp_all add: homeomorphism_def subset_eq)
  have [simp]: "aff_dim T  aff_dim V"
    by (simp add: affTU affV)
  have "openin (top_of_set T) ((f  h) ` g ` (S - {b}))"
  proof (rule invariance_of_domain_affine_sets [OF _ affine V])
    have "openin (top_of_set (rel_frontier U - {b})) (S - {b})"
      by (meson Diff_mono Diff_subset SU ope openin_delete openin_subset_trans order_refl)
    then show "openin (top_of_set V) (g ` (S - {b}))"
      by (rule homeomorphism_imp_open_map [OF gh])
    show "continuous_on (g ` (S - {b})) (f  h)"
    proof (rule continuous_on_compose)
      show "continuous_on (g ` (S - {b})) h"
        by (meson Diff_mono SU homeomorphism_def homeomorphism_of_subsets gh set_eq_subset)
    qed (use contf continuous_on_subset hgsub in blast)
    show "inj_on (f  h) (g ` (S - {b}))"
      by (smt (verit, del_insts) SU homeomorphism_def inj_on_def injf gh Diff_iff comp_apply imageE subset_iff)
    show "(f  h) ` g ` (S - {b})  T"
      by (metis fim image_comp image_mono hgsub subset_trans)
  qed (auto simp: assms)
  moreover
  have "openin (top_of_set T) ((f  k) ` j ` (S - {c}))"
  proof (rule invariance_of_domain_affine_sets [OF _ affine V])
    show "openin (top_of_set V) (j ` (S - {c}))"
      by (meson Diff_mono Diff_subset SU ope openin_delete openin_subset_trans order_refl homeomorphism_imp_open_map [OF jk])
    show "continuous_on (j ` (S - {c})) (f  k)"
    proof (rule continuous_on_compose)
      show "continuous_on (j ` (S - {c})) k"
        by (meson Diff_mono SU homeomorphism_def homeomorphism_of_subsets jk set_eq_subset)
    qed (use contf continuous_on_subset kjsub in blast)
    show "inj_on (f  k) (j ` (S - {c}))"
      by (smt (verit, del_insts) SU homeomorphism_def inj_on_def injf jk Diff_iff comp_apply imageE subset_iff)
    show "(f  k) ` j ` (S - {c})  T"
      by (metis fim image_comp image_mono kjsub subset_trans)
  qed (auto simp: assms)
  ultimately have "openin (top_of_set T) ((f  h) ` g ` (S - {b})  ((f  k) ` j ` (S - {c})))"
    by (rule openin_Un)
  moreover have "(f  h) ` g ` (S - {b}) = f ` (S - {b})"
  proof -
    have "h ` g ` (S - {b}) = (S - {b})"
    proof
      show "h ` g ` (S - {b})  S - {b}"
        using homeomorphism_apply1 [OF gh] SU by (fastforce simp add: image_iff image_subset_iff)
      show "S - {b}  h ` g ` (S - {b})"
        by (metis Diff_mono SU gh homeomorphism_image2 homeomorphism_of_subsets set_eq_subset)
    qed
    then show ?thesis
      by (metis image_comp)
  qed
  moreover have "(f  k) ` j ` (S - {c}) = f ` (S - {c})"
  proof -
    have "k ` j ` (S - {c}) = (S - {c})"
      using homeomorphism_apply1 [OF jk] SU
      by (meson Diff_mono homeomorphism_def homeomorphism_of_subsets jk subset_refl)
    then show ?thesis
      by (metis image_comp)
  qed
  moreover have "f ` (S - {b})  f ` (S - {c}) = f ` (S)"
    using b  c by blast
  ultimately show ?thesis
    by simp
qed


lemma invariance_of_domain_sphere_affine_set:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S  T"
      and "r  0" "affine T" and affTU: "aff_dim T < DIM('a)"
      and ope: "openin (top_of_set (sphere a r)) S"
   shows "openin (top_of_set T) (f ` S)"
proof (cases "sphere a r = {}")
  case True
  then show ?thesis
    using ope openin_subset by force
next
  case False
  show ?thesis
  proof (rule invariance_of_domain_sphere_affine_set_gen [OF contf injf fim bounded_cball convex_cball affine T])
    show "aff_dim T < aff_dim (cball a r)"
      by (metis False affTU aff_dim_cball assms(4) linorder_cases sphere_empty)
    show "openin (top_of_set (rel_frontier (cball a r))) S"
      by (simp add: r  0 ope)
  qed
qed

lemma no_embedding_sphere_lowdim:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes contf: "continuous_on (sphere a r) f" and injf: "inj_on f (sphere a r)" and "r > 0"
   shows "DIM('a)  DIM('b)"
proof -
  have "False" if "DIM('a) > DIM('b)"
  proof -
    have "compact (f ` sphere a r)"
      using compact_continuous_image
      by (simp add: compact_continuous_image contf)
    then have "¬ open (f ` sphere a r)"
      using compact_open
      by (metis assms(3) image_is_empty not_less_iff_gr_or_eq sphere_eq_empty)
    then show False
      using invariance_of_domain_sphere_affine_set [OF contf injf subset_UNIV] r > 0
      by (metis aff_dim_UNIV affine_UNIV less_irrefl of_nat_less_iff open_openin openin_subtopology_self subtopology_UNIV that)
  qed
  then show ?thesis
    using not_less by blast
qed

lemma simply_connected_sphere:
  fixes a :: "'a::euclidean_space"
  assumes "3  DIM('a)"
    shows "simply_connected(sphere a r)"
proof (cases rule: linorder_cases [of r 0])
  case less
  then show ?thesis by simp
next
  case equal
  then show ?thesis  by (auto simp: convex_imp_simply_connected)
next
  case greater
  then show ?thesis
    using simply_connected_sphere_gen [of "cball a r"] assms
    by (simp add: aff_dim_cball)
qed

lemma simply_connected_sphere_eq:
  fixes a :: "'a::euclidean_space"
  shows "simply_connected(sphere a r)  3  DIM('a)  r  0"  (is "?lhs = ?rhs")
proof (cases "r  0")
  case True
  have "simply_connected (sphere a r)"
    using True less_eq_real_def by (auto intro: convex_imp_simply_connected)
  with True show ?thesis by auto
next
  case False
  show ?thesis
  proof
    assume L: ?lhs
    have "False" if "DIM('a) = 1  DIM('a) = 2"
      using that
    proof
      assume "DIM('a) = 1"
      with L show False
        using connected_sphere_eq simply_connected_imp_connected
        by (metis False Suc_1 not_less_eq_eq order_refl)
    next
      assume "DIM('a) = 2"
      then have "sphere a r homeomorphic sphere (0::complex) 1"
        by (metis DIM_complex False homeomorphic_spheres_gen not_less zero_less_one)
      then have "simply_connected(sphere (0::complex) 1)"
        using L homeomorphic_simply_connected_eq by blast
      then obtain a::complex where "homotopic_with_canon (λh. True) (sphere 0 1) (sphere 0 1) id (λx. a)"
        by (metis continuous_on_id' id_apply image_id subset_refl simply_connected_eq_contractible_circlemap)
      then show False
        using contractible_sphere contractible_def not_one_le_zero by blast
    qed
    with False show ?rhs
      by (metis DIM_ge_Suc0 One_nat_def Suc_1 not_less_eq_eq numeral_3_eq_3 order_antisym_conv)
  next
    assume ?rhs
    with False show ?lhs by (simp add: simply_connected_sphere)
  qed
qed


lemma simply_connected_punctured_universe_eq:
  fixes a :: "'a::euclidean_space"
  shows "simply_connected(- {a})  3  DIM('a)"
proof -
  have [simp]: "a  rel_interior (cball a 1)"
    by (simp add: rel_interior_nonempty_interior)
  have [simp]: "affine hull cball a 1 - {a} = -{a}"
    by (metis Compl_eq_Diff_UNIV aff_dim_cball aff_dim_lt_full not_less_iff_gr_or_eq zero_less_one)
  have "sphere a 1 homotopy_eqv - {a}"
    using homotopy_eqv_rel_frontier_punctured_affine_hull [of "cball a 1" a] by auto
  then have "simply_connected(- {a})  simply_connected(sphere a 1)"
    using homotopy_eqv_simple_connectedness by blast
  also have "...   3  DIM('a)"
    by (simp add: simply_connected_sphere_eq)
  finally show ?thesis .
qed

lemma not_simply_connected_circle:
  fixes a :: complex
  shows "0 < r  ¬ simply_connected(sphere a r)"
by (simp add: simply_connected_sphere_eq)


proposition simply_connected_punctured_convex:
  fixes a :: "'a::euclidean_space"
  assumes "convex S" and 3: "3  aff_dim S"
    shows "simply_connected(S - {a})"
proof (cases "a  rel_interior S")
  case True
  then obtain e where "a  S" "0 < e" and e: "cball a e  affine hull S  S"
    by (auto simp: rel_interior_cball)
  have con: "convex (cball a e  affine hull S)"
    by (simp add: convex_Int)
  have bo: "bounded (cball a e  affine hull S)"
    by (simp add: bounded_Int)
  have "affine hull S  interior (cball a e)  {}"
    using 0 < e a  S hull_subset by fastforce
  then have "3  aff_dim (affine hull S  cball a e)"
    by (simp add: 3 aff_dim_convex_Int_nonempty_interior [OF convex_affine_hull])
  also have "... = aff_dim (cball a e  affine hull S)"
    by (simp add: Int_commute)
  finally have "3  aff_dim (cball a e  affine hull S)" .
  moreover have "rel_frontier (cball a e  affine hull S) homotopy_eqv S - {a}"
  proof (rule homotopy_eqv_rel_frontier_punctured_convex)
    show "a  rel_interior (cball a e  affine hull S)"
      by (meson IntI Int_mono a  S 0 < e e cball a e  affine hull S  S ball_subset_cball centre_in_cball dual_order.strict_implies_order hull_inc hull_mono mem_rel_interior_ball)
    have "closed (cball a e  affine hull S)"
      by blast
    then show "rel_frontier (cball a e  affine hull S)  S"
      by (metis Diff_subset closure_closed dual_order.trans e rel_frontier_def)
    show "S  affine hull (cball a e  affine hull S)"
      by (metis (no_types, lifting) IntI a  S 0 < e affine_hull_convex_Int_nonempty_interior centre_in_ball convex_affine_hull empty_iff hull_subset inf_commute interior_cball subsetCE subsetI)
    qed (auto simp: assms con bo)
  ultimately show ?thesis
    using homotopy_eqv_simple_connectedness simply_connected_sphere_gen [OF con bo]
    by blast
next
  case False
  then have "rel_interior S  S - {a}"
    by (simp add: False rel_interior_subset subset_Diff_insert)
  moreover have "S - {a}  closure S"
    by (meson Diff_subset closure_subset subset_trans)
  ultimately show ?thesis
    by (metis contractible_imp_simply_connected contractible_convex_tweak_boundary_points [OF convex S])
qed

corollary simply_connected_punctured_universe:
  fixes a :: "'a::euclidean_space"
  assumes "3  DIM('a)"
  shows "simply_connected(- {a})"
proof -
  have [simp]: "affine hull cball a 1 = UNIV"
    by (simp add: aff_dim_cball affine_hull_UNIV)
  have "a  rel_interior (cball a 1)"
    by (simp add: rel_interior_interior)
  then
  have "simply_connected (rel_frontier (cball a 1)) = simply_connected (affine hull cball a 1 - {a})"
    using homotopy_eqv_rel_frontier_punctured_affine_hull homotopy_eqv_simple_connectedness by blast
  then show ?thesis
    using simply_connected_sphere [of a 1, OF assms] by (auto simp: Compl_eq_Diff_UNIV)
qed


subsection‹The power, squaring and exponential functions as covering maps›

proposition covering_space_power_punctured_plane:
  assumes "0 < n"
    shows "covering_space (- {0}) (λz::complex. z^n) (- {0})"
proof -
  consider "n = 1" | "2  n" using assms by linarith
  then obtain e where "0 < e"
                and e: "w z. cmod(w - z) < e * cmod z  (w^n = z^n  w = z)"
  proof cases
    assume "n = 1" then show ?thesis
      by (rule_tac e=1 in that) auto
  next
    assume "2  n"
    have eq_if_pow_eq:
         "w = z" if lt: "cmod (w - z) < 2 * sin (pi / real n) * cmod z"
                 and eq: "w^n = z^n" for w z
    proof (cases "z = 0")
      case True with eq assms show ?thesis by (auto simp: power_0_left)
    next
      case False
      then have "z  0" by auto
      have "(w/z)^n = 1"
        by (metis False divide_self_if eq power_divide power_one)
      then obtain j::nat where j: "w / z = exp (2 * of_real pi * 𝗂 * j / n)" and "j < n"
        using Suc_leI assms 2  n complex_roots_unity [THEN eqset_imp_iff, of n "w/z"]
        by force
      have "cmod (w/z - 1) < 2 * sin (pi / real n)"
        using lt assms z  0 by (simp add: field_split_simps norm_divide)
      then have "cmod (exp (𝗂 * of_real (2 * pi * j / n)) - 1) < 2 * sin (pi / real n)"
        by (simp add: j field_simps)
      then have "2 * ¦sin((2 * pi * j / n) / 2)¦ < 2 * sin (pi / real n)"
        by (simp only: dist_exp_i_1)
      then have sin_less: "sin((pi * j / n)) < sin (pi / real n)"
        by (simp add: field_simps)
      then have "w / z = 1"
      proof (cases "j = 0")
        case True then show ?thesis by (auto simp: j)
      next
        case False
        then have "sin (pi / real n)  sin((pi * j / n))"
        proof (cases "j / n  1/2")
          case True
          show ?thesis
            using j  0 j < n True
            by (intro sin_monotone_2pi_le) (auto simp: field_simps intro: order_trans [of _ 0])
        next
          case False
          then have seq: "sin(pi * j / n) = sin(pi * (n - j) / n)"
            using j < n by (simp add: algebra_simps diff_divide_distrib of_nat_diff)
          show ?thesis
            unfolding  seq
            using j < n False
            by (intro sin_monotone_2pi_le) (auto simp: field_simps intro: order_trans [of _ 0])
        qed
        with sin_less show ?thesis by force
      qed
      then show ?thesis by simp
    qed
    show ?thesis
    proof
      show "0 < 2 * sin (pi / real n)"
        by (force simp: 2  n sin_pi_divide_n_gt_0)
    qed (meson eq_if_pow_eq)
  qed
  have zn1: "continuous_on (- {0}) (λz::complex. z^n)"
    by (rule continuous_intros)+
  have zn2: "(λz::complex. z^n) ` (- {0}) = - {0}"
    using assms by (auto simp: image_def elim: exists_complex_root_nonzero [where n = n])
  have zn3: "T. z^n  T  open T  0  T 
               (v. v = -{0}  (λz. z ^ n) -` T 
                    (uv. open u  0  u) 
                    pairwise disjnt v 
                    (uv. Ex (homeomorphism u T (λz. z^n))))"
           if "z  0" for z::complex
  proof -
    define d where "d  min (1/2) (e/4) * norm z"
    have "0 < d"
      by (simp add: d_def 0 < e z  0)
    have iff_x_eq_y: "x^n = y^n  x = y"
         if eq: "w^n = z^n" and x: "x  ball w d" and y: "y  ball w d" for w x y
    proof -
      have [simp]: "norm z = norm w" using that
        by (simp add: assms power_eq_imp_eq_norm)
      show ?thesis
      proof (cases "w = 0")
        case True with z  0 assms eq
        show ?thesis by (auto simp: power_0_left)
      next
        case False
        have "cmod (x - y) < 2*d"
          using x y
          by (simp add: dist_norm [symmetric]) (metis dist_commute mult_2 dist_triangle_less_add)
        also have "...  2 * e / 4 * norm w"
          using e > 0 by (simp add: d_def min_mult_distrib_right)
        also have "... = e * (cmod w / 2)"
          by simp
        also have "...  e * cmod y"
        proof (rule mult_left_mono)
          have "cmod (w - y) < cmod w / 2  cmod w / 2  cmod y"
            by (metis (no_types) dist_0_norm dist_norm norm_triangle_half_l not_le order_less_irrefl)
          then show "cmod w / 2  cmod y"
            using y by (simp add: dist_norm d_def min_mult_distrib_right)
        qed (use e > 0 in auto)
        finally have "cmod (x - y) < e * cmod y" .
        then show ?thesis by (rule e)
      qed
    qed
    then have inj: "inj_on (λw. w^n) (ball z d)"
      by (simp add: inj_on_def)
    have cont: "continuous_on (ball z d) (λw. w ^ n)"
      by (intro continuous_intros)
    have noncon: "¬ (λw::complex. w^n) constant_on UNIV"
      by (metis UNIV_I assms constant_on_def power_one zero_neq_one zero_power)
    have im_eq: "(λw. w^n) ` ball z' d = (λw. w^n) ` ball z d"
                if z': "z'^n = z^n" for z'
    proof -
      have nz': "norm z' = norm z" using that assms power_eq_imp_eq_norm by blast
      have "(w  (λw. w^n) ` ball z' d) = (w  (λw. w^n) ` ball z d)" for w
      proof (cases "w=0")
        case True with assms show ?thesis
          by (simp add: image_def ball_def nz')
      next
        case False
        have "z'  0" using z  0 nz' by force
        have 1: "(z*x / z')^n = x^n" if "x  0" for x
          using z' that by (simp add: field_simps z  0)
        have 2: "cmod (z - z * x / z') = cmod (z' - x)" if "x  0" for x
        proof -
          have "cmod (z - z * x / z') = cmod z * cmod (1 - x / z')"
            by (metis (no_types) ab_semigroup_mult_class.mult_ac(1) divide_complex_def mult.right_neutral norm_mult right_diff_distrib')
          also have "... = cmod z' * cmod (1 - x / z')"
            by (simp add: nz')
          also have "... = cmod (z' - x)"
            by (simp add: z'  0 diff_divide_eq_iff norm_divide)
          finally show ?thesis .
        qed
        have 3: "(z'*x / z)^n = x^n" if "x  0" for x
          using z' that by (simp add: field_simps z  0)
        have 4: "cmod (z' - z' * x / z) = cmod (z - x)" if "x  0" for x
        proof -
          have "cmod (z * (1 - x * inverse z)) = cmod (z - x)"
            by (metis z  0 diff_divide_distrib divide_complex_def divide_self_if nonzero_eq_divide_eq semiring_normalization_rules(7))
          then show ?thesis
            by (metis (no_types) mult.assoc divide_complex_def mult.right_neutral norm_mult nz' right_diff_distrib')
        qed
        show ?thesis
          by (simp add: set_eq_iff image_def ball_def) (metis 1 2 3 4 diff_zero dist_norm nz')
      qed
      then show ?thesis by blast
    qed

    have ex_ball: "B. (z'. B = ball z' d  z'^n = z^n)  x  B"
                  if "x  0" and eq: "x^n = w^n" and dzw: "dist z w < d" for x w
    proof -
      have "w  0" by (metis assms power_eq_0_iff that(1) that(2))
      have [simp]: "cmod x = cmod w"
        using assms power_eq_imp_eq_norm eq by blast
      have [simp]: "cmod (x * z / w - x) = cmod (z - w)"
      proof -
        have "cmod (x * z / w - x) = cmod x * cmod (z / w - 1)"
          by (metis (no_types) mult.right_neutral norm_mult right_diff_distrib' times_divide_eq_right)
        also have "... = cmod w * cmod (z / w - 1)"
          by simp
        also have "... = cmod (z - w)"
          by (simp add: w  0 divide_diff_eq_iff nonzero_norm_divide)
        finally show ?thesis .
      qed
      show ?thesis
      proof (intro exI conjI)
        show "(z / w * x) ^ n = z ^ n"
          by (metis w  0 eq nonzero_eq_divide_eq power_mult_distrib)
        show "x  ball (z / w * x) d"
          using d > 0 that
          by (simp add: ball_eq_ball_iff z  0 w  0 field_simps) (simp add: dist_norm)
      qed auto
    qed

    show ?thesis
    proof (rule exI, intro conjI)
      show "z ^ n  (λw. w ^ n) ` ball z d"
        using d > 0 by simp
      show "open ((λw. w ^ n) ` ball z d)"
        by (rule invariance_of_domain [OF cont open_ball inj])
      show "0  (λw. w ^ n) ` ball z d"
        using z  0 assms by (force simp: d_def)
      show "v. v = - {0}  (λz. z ^ n) -` (λw. w ^ n) ` ball z d 
                (uv. open u  0  u) 
                disjoint v 
                (uv. Ex (homeomorphism u ((λw. w ^ n) ` ball z d) (λz. z ^ n)))"
      proof (rule exI, intro ballI conjI)
        show "{ball z' d |z'. z'^n = z^n} = - {0}  (λz. z ^ n) -` (λw. w ^ n) ` ball z d" (is "?l = ?r")
        proof 
          have "z'. cmod z' < d  z' ^ n  z ^ n"
            by (auto simp add: assms d_def power_eq_imp_eq_norm that)
          then show "?l  ?r"
            by auto (metis im_eq image_eqI mem_ball)
          show "?r  ?l"
            by auto (meson ex_ball)
        qed
        show "u. u  {ball z' d |z'. z' ^ n = z ^ n}  0  u"
          by (force simp add: assms d_def power_eq_imp_eq_norm that)

        show "disjoint {ball z' d |z'. z' ^ n = z ^ n}"
        proof (clarsimp simp add: pairwise_def disjnt_iff)
          fix ξ ζ x
          assume "ξ^n = z^n" "ζ^n = z^n" "ball ξ d  ball ζ d"
            and "dist ξ x < d" "dist ζ x < d"
          then have "dist ξ ζ < d+d"
            using dist_triangle_less_add by blast
          then have "cmod (ξ - ζ) < 2*d"
            by (simp add: dist_norm)
          also have "...  e * cmod z"
            using mult_right_mono 0 < e that by (auto simp: d_def)
          finally have "cmod (ξ - ζ) < e * cmod z" .
          with e have "ξ = ζ"
            by (metis ξ^n = z^n ζ^n = z^n assms power_eq_imp_eq_norm)
          then show "False"
            using ball ξ d  ball ζ d by blast
        qed
        show "Ex (homeomorphism u ((λw. w ^ n) ` ball z d) (λz. z ^ n))"
          if "u  {ball z' d |z'. z' ^ n = z ^ n}" for u
        proof (rule invariance_of_domain_homeomorphism [of "u" "λz. z^n"])
          show "open u"
            using that by auto
          show "continuous_on u (λz. z ^ n)"
            by (intro continuous_intros)
          show "inj_on (λz. z ^ n) u"
            using that by (auto simp: iff_x_eq_y inj_on_def)
          show "g. homeomorphism u ((λz. z ^ n) ` u) (λz. z ^ n) g  Ex (homeomorphism u ((λw. w ^ n) ` ball z d) (λz. z ^ n))"
            using im_eq that by clarify metis
        qed auto
      qed auto
    qed
  qed
  show ?thesis
    using assms
    apply (simp add: covering_space_def zn1 zn2)
    apply (subst zn2 [symmetric])
    apply (simp add: openin_open_eq open_Compl zn3)
    done
qed

corollary covering_space_square_punctured_plane:
  "covering_space (- {0}) (λz::complex. z^2) (- {0})"
  by (simp add: covering_space_power_punctured_plane)


proposition covering_space_exp_punctured_plane:
  "covering_space UNIV (λz::complex. exp z) (- {0})"
proof (simp add: covering_space_def, intro conjI ballI)
  show "continuous_on UNIV (λz::complex. exp z)"
    by (rule continuous_on_exp [OF continuous_on_id])
  show "range exp = - {0::complex}"
    by auto (metis exp_Ln range_eqI)
  show "T. z  T  openin (top_of_set (- {0})) T 
             (v. v = exp -` T  (uv. open u)  disjoint v 
                  (uv. q. homeomorphism u T exp q))"
        if "z  - {0::complex}" for z
  proof -
    have "z  0"
      using that by auto
    have "ball (Ln z) 1  ball (Ln z) pi"
      using pi_ge_two by (simp add: ball_subset_ball_iff)
    then have inj_exp: "inj_on exp (ball (Ln z) 1)"
      using inj_on_exp_pi inj_on_subset by blast
    define twopi where "twopi  λn. of_real (2 * of_int n * pi) * 𝗂"
    define 𝒱 where "𝒱  range (λn. (λx. x + twopi n) ` (ball(Ln z) 1))"
    have exp_eq': "exp w = exp z  (n::int. w = z + twopi n)" for z w
      by (simp add: exp_eq twopi_def)
    show ?thesis
    proof (intro exI conjI)
      show "z  exp ` (ball(Ln z) 1)"
        by (metis z  0 centre_in_ball exp_Ln rev_image_eqI zero_less_one)
      have "open (- {0::complex})"
        by blast
      with inj_exp show "openin (top_of_set (- {0})) (exp ` ball (Ln z) 1)"
        by (auto simp: openin_open_eq invariance_of_domain continuous_on_exp [OF continuous_on_id])
      show UV: "𝒱 = exp -` exp ` ball (Ln z) 1"
        by (force simp: 𝒱_def twopi_def Complex_Transcendental.exp_eq image_iff)
      show "V𝒱. open V"
        by (auto simp: 𝒱_def inj_on_def continuous_intros invariance_of_domain)
      have "2  cmod (twopi m -twopi n)" if "m  n" for m n
      proof -
        have "1  abs (m - n)"
          using that by linarith
        then have "1  cmod (of_int m - of_int n) * 1"
          by (metis mult.right_neutral norm_of_int of_int_1_le_iff of_int_abs of_int_diff)
        also have "...  cmod (of_int m - of_int n) * of_real pi"
          using pi_ge_two
           by (intro mult_left_mono) auto
        also have "...  cmod ((of_int m - of_int n) * of_real pi * 𝗂)"
          by (simp add: norm_mult)
        also have "...  cmod (of_int m * of_real pi * 𝗂 - of_int n * of_real pi * 𝗂)"
          by (simp add: algebra_simps)
        finally have "1  cmod (of_int m * of_real pi * 𝗂 - of_int n * of_real pi * 𝗂)" .
        then have "2 * 1  cmod (2 * (of_int m * of_real pi * 𝗂 - of_int n * of_real pi * 𝗂))"
          by (metis mult_le_cancel_left_pos norm_mult_numeral1 zero_less_numeral)
        then show ?thesis
          by (simp add: algebra_simps twopi_def)
      qed
      then show "disjoint 𝒱"
        unfolding 𝒱_def pairwise_def disjnt_iff
        by (smt (verit, best) add.commute add_diff_cancel_left' add_diff_eq dist_commute dist_complex_def dist_triangle imageE mem_ball)
      show "u𝒱. q. homeomorphism u (exp ` ball (Ln z) 1) exp q"
      proof
        fix u
        assume "u  𝒱"
        then obtain n where n: "u = (λx. x + twopi n) ` (ball(Ln z) 1)"
          by (auto simp: 𝒱_def)
        have "compact (cball (Ln z) 1)"
          by simp
        moreover have "continuous_on (cball (Ln z) 1) exp"
          by (rule continuous_on_exp [OF continuous_on_id])
        moreover have "inj_on exp (cball (Ln z) 1)"
          using pi_ge_two inj_on_subset [OF inj_on_exp_pi [of "Ln z"]]
          by (simp add: subset_iff)
        ultimately obtain γ where hom: "homeomorphism (cball (Ln z) 1) (exp ` cball (Ln z) 1) exp γ"
          using homeomorphism_compact  by blast
        have eq1: "exp ` u = exp ` ball (Ln z) 1"
          by (smt (verit) n exp_eq' image_cong image_image)
        have γexp: "γ (exp x) + twopi n = x" if "x  u" for x
        proof -
          have "exp x = exp (x - twopi n)"
            using exp_eq' by auto
          then have "γ (exp x) = γ (exp (x - twopi n))"
            by simp
          also have "... = x - twopi n"
            using x  u by (auto simp: n intro: homeomorphism_apply1 [OF hom])
          finally show ?thesis
            by simp
        qed
        have exp2n: "exp (γ (exp x) + twopi n) = exp x" if "dist (Ln z) x < 1" for x
          by (metis γexp exp_eq' imageI mem_ball n that)
        have "continuous_on (exp ` ball (Ln z) 1) γ"
          by (meson ball_subset_cball continuous_on_subset hom homeomorphism_cont2 image_mono)
        then have cont: "continuous_on (exp ` ball (Ln z) 1) (λx. γ x + twopi n)"
          by (intro continuous_intros)
        have "homeomorphism u (exp ` ball (Ln z) 1) exp ((λx. x + twopi n)  γ)"
          unfolding homeomorphism_def
          apply (intro conjI ballI eq1 continuous_on_exp [OF continuous_on_id])
             apply (auto simp: γexp exp2n cont n)
           apply (force simp: image_iff homeomorphism_apply1 [OF hom])+
          done
        then show "q. homeomorphism u (exp ` ball (Ln z) 1) exp q" by metis
      qed
    qed
  qed
qed


subsection‹Hence the Borsukian results about mappings into circles›(*FIX ME title *)

lemma inessential_eq_continuous_logarithm:
  fixes f :: "'a::real_normed_vector  complex"
  shows "(a. homotopic_with_canon (λh. True) S (-{0}) f (λt. a)) 
         (g. continuous_on S g  (x  S. f x = exp(g x)))"
  (is "?lhs  ?rhs")
proof
  assume ?lhs thus ?rhs
    by (metis covering_space_lift_inessential_function covering_space_exp_punctured_plane)
next
  assume ?rhs
  then obtain g where contg: "continuous_on S g" and f: "x. x  S  f x = exp(g x)"
    by metis
  obtain a where "homotopic_with_canon (λh. True) S (- {of_real 0}) (exp  g) (λx. a)"
  proof (rule nullhomotopic_through_contractible [OF contg _ _ _ contractible_UNIV])
    show "continuous_on (UNIV::complex set) exp"
      by (intro continuous_intros)
    show "exp  UNIV  -{of_real 0}"
      by auto
  qed force
  then have "homotopic_with_canon (λh. True) S (- {0}) f (λt. a)"
    using f homotopic_with_eq by fastforce
  then show ?lhs ..
qed

corollary inessential_imp_continuous_logarithm_circle:
  fixes f :: "'a::real_normed_vector  complex"
  assumes "homotopic_with_canon (λh. True) S (sphere 0 1) f (λt. a)"
  obtains g where "continuous_on S g" and "x. x  S  f x = exp(g x)"
proof -
  have "homotopic_with_canon (λh. True) S (- {0}) f (λt. a)"
    using assms homotopic_with_subset_right by fastforce
  then show ?thesis
    by (metis inessential_eq_continuous_logarithm that)
qed


lemma inessential_eq_continuous_logarithm_circle:
  fixes f :: "'a::real_normed_vector  complex"
  shows "(a. homotopic_with_canon (λh. True) S (sphere 0 1) f (λt. a)) 
         (g. continuous_on S g  (x  S. f x = exp(𝗂 * of_real(g x))))"
  (is "?lhs  ?rhs")
proof
  assume L: ?lhs
  then obtain g where contg: "continuous_on S g" and g: "x. x  S  f x = exp(g x)"
    using inessential_imp_continuous_logarithm_circle by blast
  have "f ` S  sphere 0 1"
    by (metis L homotopic_with_imp_subset1)
  then have "x. x  S  Re (g x) = 0"
    using g by auto
  then show ?rhs
    by (rule_tac x="Im  g" in exI) (auto simp: Euler g intro: contg continuous_intros)
next
  assume ?rhs
  then obtain g where contg: "continuous_on S g" and g: "x. x  S  f x = exp(𝗂* of_real(g x))"
    by metis
  obtain a where "homotopic_with_canon (λh. True) S (sphere 0 1) ((exp  (λz. 𝗂*z))  (of_real  g)) (λx. a)"
  proof (rule nullhomotopic_through_contractible)
    show "continuous_on S (complex_of_real  g)"
      by (intro conjI contg continuous_intros)
    show "(complex_of_real  g)  S  "
      by auto
    show "continuous_on  (exp  (*)𝗂)"
      by (intro continuous_intros)
    show "(exp  (*)𝗂)    sphere 0 1"
      by (auto simp: complex_is_Real_iff)
  qed (auto simp: convex_Reals convex_imp_contractible)
  moreover have "x. x  S  (exp  (*)𝗂  (complex_of_real  g)) x = f x"
    by (simp add: g)
  ultimately have "homotopic_with_canon (λh. True) S (sphere 0 1) f (λt. a)"
    using homotopic_with_eq by force
  then show ?lhs ..
qed

proposition homotopic_with_sphere_times:
  fixes f :: "'a::real_normed_vector  complex"
  assumes hom: "homotopic_with_canon (λx. True) S (sphere 0 1) f g" and conth: "continuous_on S h"
      and hin: "x. x  S  h x  sphere 0 1"
    shows "homotopic_with_canon (λx. True) S (sphere 0 1) (λx. f x * h x) (λx. g x * h x)"
proof -
  obtain k where contk: "continuous_on ({0..1::real} × S) k"
             and kim: "k ` ({0..1} × S)  sphere 0 1"
             and k0:  "x. k(0, x) = f x"
             and k1: "x. k(1, x) = g x"
    using hom by (auto simp: homotopic_with_def)
  show ?thesis
    apply (simp add: homotopic_with)
    apply (rule_tac x="λz. k z * (h  snd)z" in exI)
    using kim hin by (fastforce simp: conth norm_mult k0 k1 intro!: contk continuous_intros)+
qed

proposition homotopic_circlemaps_divide:
  fixes f :: "'a::real_normed_vector  complex"
    shows "homotopic_with_canon (λx. True) S (sphere 0 1) f g 
           continuous_on S f  f ` S  sphere 0 1 
           continuous_on S g  g ` S  sphere 0 1 
           (c. homotopic_with_canon (λx. True) S (sphere 0 1) (λx. f x / g x) (λx. c))"
proof -
  have "homotopic_with_canon (λx. True) S (sphere 0 1) (λx. f x / g x) (λx. 1)"
       if "homotopic_with_canon (λx. True) S (sphere 0 1) (λx. f x / g x) (λx. c)" for c
  proof -
    have "S = {}  path_component (sphere 0 1) 1 c"
      using homotopic_with_imp_subset2 [OF that] path_connected_sphere [of "0::complex" 1]
      by (auto simp: path_connected_component)
    with subtopology_empty_iff_trivial 
    have "homotopic_with_canon (λx. True) S (sphere 0 1) (λx. 1) (λx. c)"
      by (force simp add: homotopic_constant_maps)
    then show ?thesis
      using homotopic_with_symD homotopic_with_trans that by blast
  qed
  then have *: "(c. homotopic_with_canon (λx. True) S (sphere 0 1) (λx. f x / g x) (λx. c)) 
                homotopic_with_canon (λx. True) S (sphere 0 1) (λx. f x / g x) (λx. 1)"
    by auto
  have "homotopic_with_canon (λx. True) S (sphere 0 1) f g 
           continuous_on S f  f ` S  sphere 0 1 
           continuous_on S g  g ` S  sphere 0 1 
           homotopic_with_canon (λx. True) S (sphere 0 1) (λx. f x / g x) (λx. 1)"
        (is "?lhs  ?rhs")
  proof
    assume L: ?lhs
    have geq1 [simp]: "x. x  S  cmod (g x) = 1"
      using homotopic_with_imp_subset2 [OF L]
      by (simp add: image_subset_iff)
    have cont: "continuous_on S (inverse  g)"
    proof (rule continuous_intros)
      show "continuous_on S g"
        using homotopic_with_imp_continuous [OF L] by blast
      show "continuous_on (g ` S) inverse"
        by (rule continuous_on_subset [of "sphere 0 1", OF continuous_on_inverse]) auto
    qed
    have [simp]: "x. x  S  g x  0"
      using geq1 by fastforce
    have "homotopic_with_canon (λx. True) S (sphere 0 1) (λx. f x / g x) (λx. 1)"
      using homotopic_with_eq [OF homotopic_with_sphere_times [OF L cont]]
      by (auto simp: divide_inverse norm_inverse)
    with L show ?rhs
      by (simp add: homotopic_with_imp_continuous homotopic_with_imp_subset1 homotopic_with_imp_subset2)
  next
    assume ?rhs then show ?lhs
      by (elim conjE homotopic_with_eq [OF homotopic_with_sphere_times]; force)
  qed
  then show ?thesis
    by (simp add: *)
qed

subsection‹Upper and lower hemicontinuous functions›

text‹And relation in the case of preimage map to open and closed maps, and fact that upper and lower
hemicontinuity together imply continuity in the sense of the Hausdorff metric (at points where the
function gives a bounded and nonempty set).›


text‹Many similar proofs below.›
lemma upper_hemicontinuous:
  assumes "x. x  S  f x  T"
    shows "((U. openin (top_of_set T) U
                  openin (top_of_set S) {x  S. f x  U}) 
            (U. closedin (top_of_set T) U
                  closedin (top_of_set S) {x  S. f x  U  {}}))"
          (is "?lhs = ?rhs")
proof (intro iffI allI impI)
  fix U
  assume * [rule_format]: ?lhs and "closedin (top_of_set T) U"
  then have "openin (top_of_set T) (T - U)"
    by (simp add: openin_diff)
  then have "openin (top_of_set S) {x  S. f x  T - U}"
    using * [of "T-U"] by blast
  moreover have "S - {x  S. f x  T - U} = {x  S. f x  U  {}}"
    using assms by blast
  ultimately show "closedin (top_of_set S) {x  S. f x  U  {}}"
    by (simp add: openin_closedin_eq)
next
  fix U
  assume * [rule_format]: ?rhs and "openin (top_of_set T) U"
  then have "closedin (top_of_set T) (T - U)"
    by (simp add: closedin_diff)
  then have "closedin (top_of_set S) {x  S. f x  (T - U)  {}}"
    using * [of "T-U"] by blast
  moreover have "{x  S. f x  (T - U)  {}} = S - {x  S. f x  U}"
    using assms by auto
  ultimately show "openin (top_of_set S) {x  S. f x  U}"
    by (simp add: openin_closedin_eq)
qed

lemma lower_hemicontinuous:
  assumes "x. x  S  f x  T"
    shows "((U. closedin (top_of_set T) U
                  closedin (top_of_set S) {x  S. f x  U}) 
            (U. openin (top_of_set T) U
                  openin (top_of_set S) {x  S. f x  U  {}}))"
          (is "?lhs = ?rhs")
proof (intro iffI allI impI)
  fix U
  assume * [rule_format]: ?lhs and "openin (top_of_set T) U"
  then have "closedin (top_of_set T) (T - U)"
    by (simp add: closedin_diff)
  then have "closedin (top_of_set S) {x  S. f x  T-U}"
    using * [of "T-U"] by blast
  moreover have "{x  S. f x  T-U} = S - {x  S. f x  U  {}}"
    using assms by auto
  ultimately show "openin (top_of_set S) {x  S. f x  U  {}}"
    by (simp add: openin_closedin_eq)
next
  fix U
  assume * [rule_format]: ?rhs and "closedin (top_of_set T) U"
  then have "openin (top_of_set T) (T - U)"
    by (simp add: openin_diff)
  then have "openin (top_of_set S) {x  S. f x  (T - U)  {}}"
    using * [of "T-U"] by blast
  moreover have "S - {x  S. f x  (T - U)  {}} = {x  S. f x  U}"
    using assms by blast
  ultimately show "closedin (top_of_set S) {x  S. f x  U}"
    by (simp add: openin_closedin_eq)
qed

lemma open_map_iff_lower_hemicontinuous_preimage:
  assumes "f ` S  T"
    shows "((U. openin (top_of_set S) U
                  openin (top_of_set T) (f ` U)) 
            (U. closedin (top_of_set S) U
                  closedin (top_of_set T) {y  T. {x. x  S  f x = y}  U}))"
          (is "?lhs = ?rhs")
proof (intro iffI allI impI)
  fix U
  assume * [rule_format]: ?lhs and "closedin (top_of_set S) U"
  then have "openin (top_of_set S) (S - U)"
    by (simp add: openin_diff)
  then have "openin (top_of_set T) (f ` (S - U))"
    using * [of "S-U"] by blast
  moreover have "T - (f ` (S - U)) = {y  T. {x  S. f x = y}  U}"
    using assms by blast
  ultimately show "closedin (top_of_set T) {y  T. {x  S. f x = y}  U}"
    by (simp add: openin_closedin_eq)
next
  fix U
  assume * [rule_format]: ?rhs and opeSU: "openin (top_of_set S) U"
  then have "closedin (top_of_set S) (S - U)"
    by (simp add: closedin_diff)
  then have "closedin (top_of_set T) {y  T. {x  S. f x = y}  S - U}"
    using * [of "S-U"] by blast
  moreover have "{y  T. {x  S. f x = y}  S - U} = T - (f ` U)"
    using assms openin_imp_subset [OF opeSU] by auto
  ultimately show "openin (top_of_set T) (f ` U)"
    using assms openin_imp_subset [OF opeSU] by (force simp: openin_closedin_eq)
qed

lemma closed_map_iff_upper_hemicontinuous_preimage:
  assumes "f ` S  T"
    shows "((U. closedin (top_of_set S) U
                  closedin (top_of_set T) (f ` U)) 
            (U. openin (top_of_set S) U
                  openin (top_of_set T) {y  T. {x. x  S  f x = y}  U}))"
          (is "?lhs = ?rhs")
proof (intro iffI allI impI)
  fix U
  assume * [rule_format]: ?lhs and opeSU: "openin (top_of_set S) U"
  then have "closedin (top_of_set S) (S - U)"
    by (simp add: closedin_diff)
  then have "closedin (top_of_set T) (f ` (S - U))"
    using * [of "S-U"] by blast
  moreover have "f ` (S - U) = T -  {y  T. {x. x  S  f x = y}  U}"
    using assms openin_imp_subset [OF opeSU] by auto
  ultimately show "openin (top_of_set T)  {y  T. {x. x  S  f x = y}  U}"
    using assms openin_imp_subset [OF opeSU] by (force simp: openin_closedin_eq)
next
  fix U
  assume * [rule_format]: ?rhs and cloSU: "closedin (top_of_set S) U"
  then have "openin (top_of_set S) (S - U)"
    by (simp add: openin_diff)
  then have "openin (top_of_set T) {y  T. {x  S. f x = y}  S - U}"
    using * [of "S-U"] by blast
  moreover have "(f ` U) = T - {y  T. {x  S. f x = y}  S - U}"
    using assms closedin_imp_subset [OF cloSU]  by auto
  ultimately show "closedin (top_of_set T) (f ` U)"
    by (simp add: openin_closedin_eq)
qed

proposition upper_lower_hemicontinuous_explicit:
  fixes T :: "('b::{real_normed_vector,heine_borel}) set"
  assumes fST: "x. x  S  f x  T"
      and ope: "U. openin (top_of_set T) U
                      openin (top_of_set S) {x  S. f x  U}"
      and clo: "U. closedin (top_of_set T) U
                      closedin (top_of_set S) {x  S. f x  U}"
      and "x  S" "0 < e" and bofx: "bounded(f x)" and fx_ne: "f x  {}"
  obtains d where "0 < d"
             "x'. x'  S; dist x x' < d
                            (y  f x. y'. y'  f x'  dist y y' < e) 
                               (y'  f x'. y. y  f x  dist y' y < e)"
proof -
  have "openin (top_of_set T) (T  (af x. bball 0 e. {a + b}))"
    by (auto simp: open_sums openin_open_Int)
  with ope have "openin (top_of_set S)
                    {u  S. f u  T  (af x. bball 0 e. {a + b})}" by blast
  with 0 < e x  S obtain d1 where "d1 > 0" and
         d1: "x'. x'  S; dist x' x < d1  f x'  T  f x'  (a  f x. b  ball 0 e. {a + b})"
    by (force simp: openin_euclidean_subtopology_iff dest: fST)
  have oo: "U. openin (top_of_set T) U 
                 openin (top_of_set S) {x  S. f x  U  {}}"
    using lower_hemicontinuous fST clo by blast
  have "compact (closure(f x))"
    by (simp add: bofx)
  moreover have "closure(f x)  (a  f x. ball a (e/2))"
    using 0 < e by (force simp: closure_approachable simp del: divide_const_simps)
  ultimately obtain C where "C  f x" "finite C" "closure(f x)  (a  C. ball a (e/2))"
    by (meson compactE finite_subset_image Elementary_Metric_Spaces.open_ball compactE_image)
  then have fx_cover: "f x  (a  C. ball a (e/2))"
    by (meson closure_subset order_trans)
  with fx_ne have "C  {}"
    by blast
  have xin: "x  (a  C. {x  S. f x  T  ball a (e/2)  {}})"
    using x  S 0 < e fST C  f x by force
  have "openin (top_of_set S) {x  S. f x  (T  ball a (e/2))  {}}" for a
    by (simp add: openin_open_Int oo)
  then have "openin (top_of_set S) (a  C. {x  S. f x  T  ball a (e/2)  {}})"
    by (simp add: Int_assoc openin_INT2 [OF finite C C  {}])
  with xin obtain d2 where "d2>0"
              and d2: "u v. u  S; dist u x < d2; v  C  f u  T  ball v (e/2)  {}"
    unfolding openin_euclidean_subtopology_iff using xin by fastforce
  show ?thesis
  proof (intro that conjI ballI)
    show "0 < min d1 d2"
      using 0 < d1 0 < d2 by linarith
  next
    fix x' y
    assume "x'  S" "dist x x' < min d1 d2" "y  f x"
    then have dd2: "dist x' x < d2"
      by (auto simp: dist_commute)
    obtain a where "a  C" "y  ball a (e/2)"
      using fx_cover y  f x by auto
    then show "y'. y'  f x'  dist y y' < e"
      using d2 [OF x'  S dd2] dist_triangle_half_r by fastforce
  next
    fix x' y'
    assume "x'  S" "dist x x' < min d1 d2" "y'  f x'"
    then have "dist x' x < d1"
      by (auto simp: dist_commute)
    then have "y'  (af x. bball 0 e. {a + b})"
      using d1 [OF x'  S] y'  f x' by force
    then show "y. y  f x  dist y' y < e"
      by clarsimp (metis add_diff_cancel_left' dist_norm)
  qed
qed


subsection‹Complex logs exist on various "well-behaved" sets›

lemma continuous_logarithm_on_contractible:
  fixes f :: "'a::real_normed_vector  complex"
  assumes "continuous_on S f" "contractible S" "z. z  S  f z  0"
  obtains g where "continuous_on S g" "x. x  S  f x = exp(g x)"
proof -
  obtain c where hom: "homotopic_with_canon (λh. True) S (-{0}) f (λx. c)"
    using nullhomotopic_from_contractible assms
    by (metis imageE subset_Compl_singleton image_subset_iff_funcset)
  then show ?thesis
    by (metis inessential_eq_continuous_logarithm that)
qed

lemma continuous_logarithm_on_simply_connected:
  fixes f :: "'a::real_normed_vector  complex"
  assumes contf: "continuous_on S f" and S: "simply_connected S" "locally path_connected S"
      and f: "z. z  S  f z  0"
  obtains g where "continuous_on S g" "x. x  S  f x = exp(g x)"
  using covering_space_lift [OF covering_space_exp_punctured_plane S contf]
  by (metis (full_types) f imageE subset_Compl_singleton image_subset_iff_funcset)

lemma continuous_logarithm_on_cball:
  fixes f :: "'a::real_normed_vector  complex"
  assumes "continuous_on (cball a r) f" and "z. z  cball a r  f z  0"
    obtains h where "continuous_on (cball a r) h" "z. z  cball a r  f z = exp(h z)"
  using assms continuous_logarithm_on_contractible convex_imp_contractible by blast

lemma continuous_logarithm_on_ball:
  fixes f :: "'a::real_normed_vector  complex"
  assumes "continuous_on (ball a r) f" and "z. z  ball a r  f z  0"
  obtains h where "continuous_on (ball a r) h" "z. z  ball a r  f z = exp(h z)"
  using assms continuous_logarithm_on_contractible convex_imp_contractible by blast

lemma continuous_sqrt_on_contractible:
  fixes f :: "'a::real_normed_vector  complex"
  assumes "continuous_on S f" "contractible S"
      and "z. z  S  f z  0"
  obtains g where "continuous_on S g" "x. x  S  f x = (g x) ^ 2"
proof -
  obtain g where contg: "continuous_on S g" and feq: "x. x  S  f x = exp(g x)"
    using continuous_logarithm_on_contractible [OF assms] by blast
  show ?thesis
  proof
    show "continuous_on S (λz. exp (g z / 2))"
      by (rule continuous_on_compose2 [of UNIV exp]; intro continuous_intros contg subset_UNIV) auto
    show "x. x  S  f x = (exp (g x / 2))2"
      by (metis exp_double feq nonzero_mult_div_cancel_left times_divide_eq_right zero_neq_numeral)
  qed
qed

lemma continuous_sqrt_on_simply_connected:
  fixes f :: "'a::real_normed_vector  complex"
  assumes contf: "continuous_on S f" and S: "simply_connected S" "locally path_connected S"
      and f: "z. z  S  f z  0"
  obtains g where "continuous_on S g" "x. x  S  f x = (g x) ^ 2"
proof -
  obtain g where contg: "continuous_on S g" and feq: "x. x  S  f x = exp(g x)"
    using continuous_logarithm_on_simply_connected [OF assms] by blast
  show ?thesis
  proof
    show "continuous_on S (λz. exp (g z / 2))"
      by (rule continuous_on_compose2 [of UNIV exp]; intro continuous_intros contg subset_UNIV) auto
    show "x. x  S  f x = (exp (g x / 2))2"
      by (metis exp_double feq nonzero_mult_div_cancel_left times_divide_eq_right zero_neq_numeral)
  qed
qed


subsection‹Another simple case where sphere maps are nullhomotopic›

lemma inessential_spheremap_2_aux:
  fixes f :: "'a::euclidean_space  complex"
  assumes 2: "2 < DIM('a)" and contf: "continuous_on (sphere a r) f" 
      and fim: "f  (sphere a r)  (sphere 0 1)" 
  obtains c where "homotopic_with_canon (λz. True) (sphere a r) (sphere 0 1) f (λx. c)"
proof -
  obtain g where contg: "continuous_on (sphere a r) g" 
             and feq: "x. x  sphere a r  f x = exp(g x)"
  proof (rule continuous_logarithm_on_simply_connected [OF contf])
    show "simply_connected (sphere a r)"
      using 2 by (simp add: simply_connected_sphere_eq)
    show "locally path_connected (sphere a r)"
      by (simp add: locally_path_connected_sphere)
    show "z.  z  sphere a r  f z  0"
      using fim by force
  qed auto
  have "g. continuous_on (sphere a r) g  (xsphere a r. f x = exp (𝗂 * complex_of_real (g x)))"
  proof (intro exI conjI)
    show "continuous_on (sphere a r) (Im  g)"
      by (intro contg continuous_intros continuous_on_compose)
    show "xsphere a r. f x = exp (𝗂 * complex_of_real ((Im  g) x))"
      using exp_eq_polar feq fim norm_exp_eq_Re
      by (auto simp flip: image_subset_iff_funcset)
  qed
  with inessential_eq_continuous_logarithm_circle that show ?thesis 
    by metis
qed

lemma inessential_spheremap_2:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes a2: "2 < DIM('a)" and b2: "DIM('b) = 2" 
      and contf: "continuous_on (sphere a r) f" and fim: "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
    using contf contractible_sphere fim nullhomotopic_into_contractible that by blast
next
  case False
  then have "sphere b s homeomorphic sphere (0::complex) 1"
    using assms by (simp add: homeomorphic_spheres_gen)
  then obtain h k where hk: "homeomorphism (sphere b s) (sphere (0::complex) 1) h k"
    by (auto simp: homeomorphic_def)
  then have conth: "continuous_on (sphere b s) h"
       and  contk: "continuous_on (sphere 0 1) k"
       and  him: "h  sphere b s  sphere 0 1"
       and  kim: "k  sphere 0 1  sphere b s"
    by (force simp: homeomorphism_def)+
  obtain c where "homotopic_with_canon (λz. True) (sphere a r) (sphere 0 1) (h  f) (λx. c)"
  proof (rule inessential_spheremap_2_aux [OF a2])
    show "continuous_on (sphere a r) (h  f)"
      by (meson contf conth continuous_on_compose continuous_on_subset fim image_subset_iff_funcset)
    show "(h  f)  sphere a r  sphere 0 1"
      using fim him by force
  qed auto
  then have "homotopic_with_canon (λf. True) (sphere a r) (sphere b s) (k  (h  f)) (k  (λx. c))"
    by (rule homotopic_with_compose_continuous_left [OF _ contk kim])
  moreover have "x. r = dist a x  f x = k (h (f x))"
    by (metis fim hk homeomorphism_def image_subset_iff mem_sphere image_subset_iff_funcset)
  ultimately have "homotopic_with_canon (λz. True) (sphere a r) (sphere b s) f (λx. k c)"
    by (auto intro: homotopic_with_eq)
  then show ?thesis
    by (metis that)
qed


subsection‹Holomorphic logarithms and square roots›

lemma g_imp_holomorphic_log:
  assumes holf: "f holomorphic_on S"
      and contg: "continuous_on S g" and feq: "x. x  S  f x = exp (g x)"
      and fnz: "z. z  S  f z  0"
  obtains g where "g holomorphic_on S" "z. z  S  f z = exp(g z)"
proof -
  have contf: "continuous_on S f"
    by (simp add: holf holomorphic_on_imp_continuous_on)
  have "g field_differentiable at z within S" if "f field_differentiable at z within S" "z  S" for z
  proof -
    obtain f' where f': "((λy. (f y - f z) / (y - z))  f') (at z within S)"
      using f field_differentiable at z within S by (auto simp: field_differentiable_def has_field_derivative_iff)
    then have ee: "((λx. (exp(g x) - exp(g z)) / (x - z))  f') (at z within S)"
      by (simp add: feq z  S Lim_transform_within [OF _ zero_less_one])
    have "(((λy. if y = g z then exp (g z) else (exp y - exp (g z)) / (y - g z))  g)  exp (g z))
          (at z within S)"
    proof (rule tendsto_compose_at)
      show "(g  g z) (at z within S)"
        using contg continuous_on z  S by blast
      show "(λy. if y = g z then exp (g z) else (exp y - exp (g z)) / (y - g z)) g z exp (g z)"
        by (simp add: LIM_offset_zero_iff DERIV_D cong: if_cong Lim_cong_within)
      qed auto
    then have dd: "((λx. if g x = g z then exp(g z) else (exp(g x) - exp(g z)) / (g x - g z))  exp(g z)) (at z within S)"
      by (simp add: o_def)
    have "continuous (at z within S) g"
      using contg continuous_on_eq_continuous_within z  S by blast
    then have "(F x in at z within S. dist (g x) (g z) < 2*pi)"
      by (simp add: continuous_within tendsto_iff)
    then have "F x in at z within S. exp (g x) = exp (g z)  g x  g z  x = z"
      by (rule eventually_mono) (auto simp: exp_eq dist_norm norm_mult)
    then have "((λy. (g y - g z) / (y - z))  f' / exp (g z)) (at z within S)"
      by (auto intro!: Lim_transform_eventually [OF tendsto_divide [OF ee dd]])
    then show ?thesis
      by (auto simp: field_differentiable_def has_field_derivative_iff)
  qed
  then have "g holomorphic_on S"
    using holf holomorphic_on_def by auto
  then show ?thesis
    using feq that by auto
qed

lemma contractible_imp_holomorphic_log:
  assumes holf: "f holomorphic_on S"
      and S: "contractible S"
      and fnz: "z. z  S  f z  0"
  obtains g where "g holomorphic_on S" "z. z  S  f z = exp(g z)"
proof -
  have contf: "continuous_on S f"
    by (simp add: holf holomorphic_on_imp_continuous_on)
  obtain g where contg: "continuous_on S g" and feq: "x. x  S  f x = exp (g x)"
    by (metis continuous_logarithm_on_contractible [OF contf S fnz])
  then show thesis
    using fnz g_imp_holomorphic_log holf that by blast
qed

lemma simply_connected_imp_holomorphic_log:
  assumes holf: "f holomorphic_on S"
      and S: "simply_connected S" "locally path_connected S"
      and fnz: "z. z  S  f z  0"
  obtains g where "g holomorphic_on S" "z. z  S  f z = exp(g z)"
proof -
  have contf: "continuous_on S f"
    by (simp add: holf holomorphic_on_imp_continuous_on)
  obtain g where contg: "continuous_on S g" and feq: "x. x  S  f x = exp (g x)"
    by (metis continuous_logarithm_on_simply_connected [OF contf S fnz])
  then show thesis
    using fnz g_imp_holomorphic_log holf that by blast
qed

lemma contractible_imp_holomorphic_sqrt:
  assumes holf: "f holomorphic_on S"
      and S: "contractible S"
      and fnz: "z. z  S  f z  0"
  obtains g where "g holomorphic_on S" "z. z  S  f z = g z ^ 2"
proof -
  obtain g where holg: "g holomorphic_on S" and feq: "z. z  S  f z = exp(g z)"
    using contractible_imp_holomorphic_log [OF assms] by blast
  show ?thesis
  proof
    show "exp  (λz. z / 2)  g holomorphic_on S"
      by (intro holomorphic_on_compose holg holomorphic_intros) auto
    show "z. z  S  f z = ((exp  (λz. z / 2)  g) z)2"
      by (simp add: feq flip: exp_double)
  qed
qed

lemma simply_connected_imp_holomorphic_sqrt:
  assumes holf: "f holomorphic_on S"
      and S: "simply_connected S" "locally path_connected S"
      and fnz: "z. z  S  f z  0"
  obtains g where "g holomorphic_on S" "z. z  S  f z = g z ^ 2"
proof -
  obtain g where holg: "g holomorphic_on S" and feq: "z. z  S  f z = exp(g z)"
    using simply_connected_imp_holomorphic_log [OF assms] by blast
  show ?thesis
  proof
    show "exp  (λz. z / 2)  g holomorphic_on S"
      by (intro holomorphic_on_compose holg holomorphic_intros) auto
    show "z. z  S  f z = ((exp  (λz. z / 2)  g) z)2"
      by (simp add: feq flip: exp_double)
  qed
qed

text‹ Related theorems about holomorphic inverse cosines.›

lemma contractible_imp_holomorphic_arccos:
  assumes holf: "f holomorphic_on S" and S: "contractible S"
      and non1: "z. z  S  f z  1  f z  -1"
  obtains g where "g holomorphic_on S" "z. z  S  f z = cos(g z)"
proof -
  have hol1f: "(λz. 1 - f z ^ 2) holomorphic_on S"
    by (intro holomorphic_intros holf)
  obtain g where holg: "g holomorphic_on S" and eq: "z. z  S  1 - (f z)2 = (g z)2"
    using contractible_imp_holomorphic_sqrt [OF hol1f S]
    by (metis eq_iff_diff_eq_0 non1 power2_eq_1_iff)
  have holfg: "(λz. f z + 𝗂*g z) holomorphic_on S"
    by (intro holf holg holomorphic_intros)
  have "z. z  S  f z + 𝗂*g z  0"
    by (metis Arccos_body_lemma eq add.commute add.inverse_unique complex_i_mult_minus power2_csqrt power2_eq_iff)
  then obtain h where holh: "h holomorphic_on S" and fgeq: "z. z  S  f z + 𝗂*g z = exp (h z)"
    using contractible_imp_holomorphic_log [OF holfg S] by metis
  show ?thesis
  proof
    show "(λz. -𝗂*h z) holomorphic_on S"
      by (intro holh holomorphic_intros)
    show "f z = cos (- 𝗂*h z)" if "z  S" for z
    proof -
      have "(f z + 𝗂*g z)*(f z - 𝗂*g z) = 1"
        using that eq by (auto simp: algebra_simps power2_eq_square)
      then have "f z - 𝗂*g z = inverse (f z + 𝗂*g z)"
        using inverse_unique by force
      also have "... = exp (- h z)"
        by (simp add: exp_minus fgeq that)
      finally have "f z = exp (- h z) + 𝗂*g z"
        by (simp add: diff_eq_eq)
      with that show ?thesis
        by (simp add: cos_exp_eq flip: fgeq)
    qed
  qed
qed


lemma contractible_imp_holomorphic_arccos_bounded:
  assumes holf: "f holomorphic_on S" and S: "contractible S" and "a  S"
      and non1: "z. z  S  f z  1  f z  -1"
  obtains g where "g holomorphic_on S" "norm(g a)  pi + norm(f a)" "z. z  S  f z = cos(g z)"
proof -
  obtain g where holg: "g holomorphic_on S" and feq: "z. z  S  f z = cos (g z)"
    using contractible_imp_holomorphic_arccos [OF holf S non1] by blast
  obtain b where "cos b = f a" "norm b  pi + norm (f a)"
    using cos_Arccos norm_Arccos_bounded by blast
  then have "cos b = cos (g a)"
    by (simp add: a  S feq)
  then consider n where "n  " "b = g a + of_real(2*n*pi)" | n where "n  " "b = -g a + of_real(2*n*pi)"
    by (auto simp: complex_cos_eq)
  then show ?thesis
  proof cases
    case 1
    show ?thesis
    proof
      show "(λz. g z + of_real(2*n*pi)) holomorphic_on S"
        by (intro holomorphic_intros holg)
      show "cmod (g a + of_real(2*n*pi))  pi + cmod (f a)"
        using "1" cmod b  pi + cmod (f a) by blast
      show "z. z  S  f z = cos (g z + complex_of_real (2*n*pi))"
        by (metis n   complex_cos_eq feq)
    qed
  next
    case 2
    show ?thesis
    proof
      show "(λz. -g z + of_real(2*n*pi)) holomorphic_on S"
        by (intro holomorphic_intros holg)
      show "cmod (-g a + of_real(2*n*pi))  pi + cmod (f a)"
        using "2" cmod b  pi + cmod (f a) by blast
      show "z. z  S  f z = cos (-g z + complex_of_real (2*n*pi))"
        by (metis n   complex_cos_eq feq)
    qed
  qed
qed


subsection‹The "Borsukian" property of sets›

text‹This doesn't have a standard name. Kuratowski uses ``contractible with respect to [S1]›''
 while Whyburn uses ``property b''. It's closely related to unicoherence.›

definitiontag important› Borsukian where
    "Borsukian S 
        f. continuous_on S f  f  S  (- {0::complex})
             (a. homotopic_with_canon (λh. True) S (- {0}) f (λx. a))"

lemma Borsukian_retraction_gen:
  assumes "Borsukian S" "continuous_on S h" "h ` S = T"
          "continuous_on T k"  "k  T  S"  "y. y  T  h(k y) = y"
    shows "Borsukian T"
proof -
  interpret R: Retracts S h T k
    using assms by (simp add: image_subset_iff_funcset Retracts.intro)
  show ?thesis
    using assms
    apply (clarsimp simp add: Borsukian_def)
    apply (rule R.cohomotopically_trivial_retraction_null_gen [OF TrueI TrueI refl, of "-{0}"], auto)
    done
qed

lemma retract_of_Borsukian: "Borsukian T; S retract_of T  Borsukian S"
  by (smt (verit) Borsukian_retraction_gen retract_of_def retraction retraction_def retraction_subset image_subset_iff_funcset)

lemma homeomorphic_Borsukian: "Borsukian S; S homeomorphic T  Borsukian T"
  using Borsukian_retraction_gen order_refl
  by (fastforce simp add: homeomorphism_def homeomorphic_def)

lemma homeomorphic_Borsukian_eq:
   "S homeomorphic T  Borsukian S  Borsukian T"
  by (meson homeomorphic_Borsukian homeomorphic_sym)

lemma Borsukian_translation:
  fixes S :: "'a::real_normed_vector set"
  shows "Borsukian (image (λx. a + x) S)  Borsukian S"
  using homeomorphic_Borsukian_eq homeomorphic_translation by blast

lemma Borsukian_injective_linear_image:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "linear f" "inj f"
    shows "Borsukian(f ` S)  Borsukian S"
  using assms homeomorphic_Borsukian_eq linear_homeomorphic_image by blast

lemma homotopy_eqv_Borsukianness:
  fixes S :: "'a::real_normed_vector set"
    and T :: "'b::real_normed_vector set"
   assumes "S homotopy_eqv T"
     shows "(Borsukian S  Borsukian T)"
  by (meson Borsukian_def assms homotopy_eqv_cohomotopic_triviality_null image_subset_iff_funcset)

lemma Borsukian_alt:
  fixes S :: "'a::real_normed_vector set"
  shows
   "Borsukian S 
        (f g. continuous_on S f  f  S  -{0} 
               continuous_on S g  g  S  -{0}
                homotopic_with_canon (λh. True) S (- {0::complex}) f g)"
  unfolding Borsukian_def homotopic_triviality
  by (force simp add: path_connected_punctured_universe)

lemma Borsukian_continuous_logarithm:
  fixes S :: "'a::real_normed_vector set"
  shows "Borsukian S 
            (f. continuous_on S f  f  S  (- {0::complex})
                  (g. continuous_on S g  (x  S. f x = exp(g x))))"
  by (simp add: Borsukian_def inessential_eq_continuous_logarithm)

lemma Borsukian_continuous_logarithm_circle:
  fixes S :: "'a::real_normed_vector set"
  shows "Borsukian S 
             (f. continuous_on S f  f  S  sphere (0::complex) 1
                   (g. continuous_on S g  (x  S. f x = exp(g x))))"
   (is "?lhs = ?rhs")
proof
  assume ?lhs then show ?rhs
    by (force simp: Borsukian_continuous_logarithm)
next
  assume RHS [rule_format]: ?rhs
  show ?lhs
  proof (clarsimp simp: Borsukian_continuous_logarithm Pi_iff)
    fix f :: "'a  complex"
    assume contf: "continuous_on S f" and 0: "iS. f i  0"
    then have "continuous_on S (λx. f x / complex_of_real (cmod (f x)))"
      by (intro continuous_intros) auto
    moreover have "(λx. f x / complex_of_real (cmod (f x)))  S  sphere 0 1"
      using 0 by (auto simp: norm_divide)
    ultimately obtain g where contg: "continuous_on S g"
                  and fg: "x  S. f x / complex_of_real (cmod (f x)) = exp(g x)"
      using RHS [of "λx. f x / of_real(norm(f x))"] by auto
    show "g. continuous_on S g  (xS. f x = exp (g x))"
    proof (intro exI ballI conjI)
      show "continuous_on S (λx. (Ln  of_real  norm  f)x + g x)"
        by (intro continuous_intros contf contg conjI) (use "0" in auto)
      show "f x = exp ((Ln  complex_of_real  cmod  f) x + g x)" if "x  S" for x
        using 0 that
        apply (simp add: exp_add)
        by (metis div_by_0 exp_Ln exp_not_eq_zero fg mult.commute nonzero_eq_divide_eq)
    qed
  qed
qed


lemma Borsukian_continuous_logarithm_circle_real:
  fixes S :: "'a::real_normed_vector set"
  shows "Borsukian S 
         (f. continuous_on S f  f  S  sphere (0::complex) 1
               (g. continuous_on S (complex_of_real  g)  (x  S. f x = exp(𝗂 * of_real(g x)))))"
   (is "?lhs = ?rhs")
proof
  assume LHS: ?lhs
  show ?rhs
  proof (clarify)
    fix f :: "'a  complex"
    assume "continuous_on S f" and f01: "f  S  sphere 0 1"
    then obtain g where contg: "continuous_on S g" and "x. x  S  f x = exp(g x)"
      using LHS by (auto simp: Borsukian_continuous_logarithm_circle)
    then have "xS. f x = exp (𝗂 * complex_of_real ((Im  g) x))"
      using f01 exp_eq_polar norm_exp_eq_Re by (fastforce simp: Pi_iff)
    then show "g. continuous_on S (complex_of_real  g)  (xS. f x = exp (𝗂 * complex_of_real (g x)))"
      by (rule_tac x="Im  g" in exI) (force intro: continuous_intros contg)
  qed
next
  assume RHS [rule_format]: ?rhs
  show ?lhs
  proof (clarsimp simp: Borsukian_continuous_logarithm_circle)
    fix f :: "'a  complex"
    assume "continuous_on S f" and f01: "f  S  sphere 0 1"
    then obtain g where contg: "continuous_on S (complex_of_real  g)" and "x. x  S  f x =  exp(𝗂 * of_real(g x))"
      by (metis RHS)
    then show "g. continuous_on S g  (xS. f x = exp (g x))"
      by (rule_tac x="λx. 𝗂* of_real(g x)" in exI) (auto simp: continuous_intros contg)
  qed
qed

lemma Borsukian_circle:
  fixes S :: "'a::real_normed_vector set"
  shows "Borsukian S 
         (f. continuous_on S f  f  S  sphere (0::complex) 1
               (a. homotopic_with_canon (λh. True) S (sphere (0::complex) 1) f (λx. a)))"
by (simp add: inessential_eq_continuous_logarithm_circle Borsukian_continuous_logarithm_circle_real)

lemma contractible_imp_Borsukian: "contractible S  Borsukian S"
  by (meson Borsukian_def nullhomotopic_from_contractible image_subset_iff_funcset)

lemma simply_connected_imp_Borsukian:
  fixes S :: "'a::real_normed_vector set"
  shows  "simply_connected S; locally path_connected S  Borsukian S"
  by (smt (verit, del_insts) continuous_logarithm_on_simply_connected Borsukian_continuous_logarithm_circle
      PiE mem_sphere_0 norm_eq_zero zero_neq_one)

lemma starlike_imp_Borsukian:
  fixes S :: "'a::real_normed_vector set"
  shows "starlike S  Borsukian S"
  by (simp add: contractible_imp_Borsukian starlike_imp_contractible)

lemma Borsukian_empty: "Borsukian {}"
  by (auto simp: contractible_imp_Borsukian)

lemma Borsukian_UNIV: "Borsukian (UNIV :: 'a::real_normed_vector set)"
  by (auto simp: contractible_imp_Borsukian)

lemma convex_imp_Borsukian:
  fixes S :: "'a::real_normed_vector set"
  shows "convex S  Borsukian S"
  by (meson Borsukian_def convex_imp_contractible nullhomotopic_from_contractible)

proposition Borsukian_sphere:
  fixes a :: "'a::euclidean_space"
  shows "3  DIM('a)  Borsukian (sphere a r)"
  using ENR_sphere 
  by (blast intro: simply_connected_imp_Borsukian ENR_imp_locally_path_connected simply_connected_sphere)

lemma Borsukian_Un_lemma:
  fixes S :: "'a::real_normed_vector set"
  assumes BS: "Borsukian S" and BT: "Borsukian T" and ST: "connected(S  T)"
    and *:  "f g::'a  complex. 
                 continuous_on S f; continuous_on T g; x. x  S  x  T  f x = g x
            continuous_on (S  T) (λx. if x  S then f x else g x)"
  shows "Borsukian(S  T)"
proof (clarsimp simp add: Borsukian_continuous_logarithm Pi_iff)
  fix f :: "'a  complex"
  assume contf: "continuous_on (S  T) f" and 0: "iS  T. f i  0"
  then have contfS: "continuous_on S f" and contfT: "continuous_on T f"
    using continuous_on_subset by auto
  have "continuous_on S f; f ` S  -{0}  g. continuous_on S g  (x  S. f x = exp(g x))"
    using BS by (auto simp: Borsukian_continuous_logarithm)
  then obtain g where contg: "continuous_on S g" and fg: "x. x  S  f x = exp(g x)"
    using "0" contfS by force
  have "continuous_on T f; f ` T  -{0}  g. continuous_on T g  (x  T. f x = exp(g x))"
    using BT by (auto simp: Borsukian_continuous_logarithm)
  then obtain h where conth: "continuous_on T h" and fh: "x. x  T  f x = exp(h x)"
    using "0" contfT by force
  show "g. continuous_on (S  T) g  (xS  T. f x = exp (g x))"
  proof (cases "S  T = {}")
    case True
    show ?thesis
    proof (intro exI conjI)
      show "continuous_on (S  T) (λx. if x  S then g x else h x)"
        using True * [OF contg conth]
        by (meson disjoint_iff)
      show "xS  T. f x = exp (if x  S then g x else h x)"
        using fg fh by auto
    qed
  next
    case False
    have "(λx. g x - h x) constant_on S  T"
    proof (rule continuous_discrete_range_constant [OF ST])
      show "continuous_on (S  T) (λx. g x - h x)"
        by (metis contg conth continuous_on_diff continuous_on_subset inf_le1 inf_le2)
      show "e>0. y. y  S  T  g y - h y  g x - h x  e  cmod (g y - h y - (g x - h x))"
           if "x  S  T" for x
      proof -
        have "g y - g x = h y - h x"
              if "y  S" "y  T" "cmod (g y - g x - (h y - h x)) < 2 * pi" for y
        proof (rule exp_complex_eqI)
          have "¦Im (g y - g x) - Im (h y - h x)¦  cmod (g y - g x - (h y - h x))"
            by (metis abs_Im_le_cmod minus_complex.simps(2))
          then show "¦Im (g y - g x) - Im (h y - h x)¦ < 2 * pi"
            using that by linarith
          have "exp (g x) = exp (h x)" "exp (g y) = exp (h y)"
            using fg fh that x  S  T by fastforce+
          then show "exp (g y - g x) = exp (h y - h x)"
            by (simp add: exp_diff)
        qed
        then show ?thesis
          by (rule_tac x="2*pi" in exI) (fastforce simp add: algebra_simps)
      qed
    qed 
    then obtain a where a: "x. x  S  T  g x - h x = a"
      by (auto simp: constant_on_def)
    with False have "exp a = 1"
      by (metis IntI disjoint_iff_not_equal divide_self_if exp_diff exp_not_eq_zero fg fh)
    with a show ?thesis
      apply (rule_tac x="λx. if x  S then g x else a + h x" in exI)
      apply (intro * contg conth continuous_intros conjI)
       apply (auto simp: algebra_simps fg fh exp_add)
      done
  qed
qed

proposition Borsukian_open_Un:
  fixes S :: "'a::real_normed_vector set"
  assumes opeS: "openin (top_of_set (S  T)) S"
      and opeT: "openin (top_of_set (S  T)) T"
      and BS: "Borsukian S" and BT: "Borsukian T" and ST: "connected(S  T)"
    shows "Borsukian(S  T)"
  by (force intro: Borsukian_Un_lemma [OF BS BT ST] continuous_on_cases_local_open [OF opeS opeT])

lemma Borsukian_closed_Un:
  fixes S :: "'a::real_normed_vector set"
  assumes cloS: "closedin (top_of_set (S  T)) S"
      and cloT: "closedin (top_of_set (S  T)) T"
      and BS: "Borsukian S" and BT: "Borsukian T" and ST: "connected(S  T)"
    shows "Borsukian(S  T)"
  by (force intro: Borsukian_Un_lemma [OF BS BT ST] continuous_on_cases_local [OF cloS cloT])

lemma Borsukian_separation_compact:
  fixes S :: "complex set"
  assumes "compact S"
    shows "Borsukian S  connected(- S)"
  by (simp add: Borsuk_separation_theorem Borsukian_circle assms)

lemma Borsukian_monotone_image_compact:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "Borsukian S" and contf: "continuous_on S f" and fim: "f ` S = T"
      and "compact S" and conn: "y. y  T  connected {x. x  S  f x = y}"
    shows "Borsukian T"
proof (clarsimp simp: Borsukian_continuous_logarithm Pi_iff)
  fix g :: "'b  complex"
  assume contg: "continuous_on T g" and 0: "iT. g i  0"
  have "continuous_on S (g  f)"
    using contf contg continuous_on_compose fim by blast
  moreover have "(g  f) ` S  -{0}"
    using fim 0 by auto
  ultimately obtain h where conth: "continuous_on S h" and gfh: "x. x  S  (g  f) x = exp(h x)"
    using Borsukian S by (auto simp: Borsukian_continuous_logarithm)
  have "y. x. y  T  x  S  f x = y"
    using fim by auto
  then obtain f' where f': "y. y  T  f' y  S  f (f' y) = y"
    by metis
  have *: "(λx. h x - h(f' y)) constant_on {x. x  S  f x = y}" if "y  T" for y
  proof (rule continuous_discrete_range_constant [OF conn [OF that], of "λx. h x - h (f' y)"], simp_all add: algebra_simps)
    show "continuous_on {x  S. f x = y} (λx. h x - h (f' y))"
      by (intro continuous_intros continuous_on_subset [OF conth]) auto
    show "e>0. u. u  S  f u = y  h u  h x  e  cmod (h u - h x)"
      if x: "x  S  f x = y" for x
    proof -
      have "h u = h x" if "u  S" "f u = y" "cmod (h u - h x) < 2 * pi" for u
      proof (rule exp_complex_eqI)
        have "¦Im (h u) - Im (h x)¦  cmod (h u - h x)"
          by (metis abs_Im_le_cmod minus_complex.simps(2))
        then show "¦Im (h u) - Im (h x)¦ < 2 * pi"
          using that by linarith
        show "exp (h u) = exp (h x)"
          by (simp add: gfh [symmetric] x that)
      qed
      then show ?thesis
        by (rule_tac x="2*pi" in exI) (fastforce simp add: algebra_simps)
    qed
  qed 
  show "h. continuous_on T h  (xT. g x = exp (h x))"
  proof (intro exI conjI)
    show "continuous_on T (h  f')"
    proof (rule continuous_from_closed_graph [of "h ` S"])
      show "compact (h ` S)"
        by (simp add: compact S compact_continuous_image conth)
      show "(h  f')  T  h ` S"
        by (auto simp: f')
      have "h x = h (f' (f x))" if "x  S" for x
        using * [of "f x"] fim that unfolding constant_on_def by clarsimp (metis f' imageI right_minus_eq)
      moreover have "x. x  T  u. u  S  x = f u  h (f' x) = h u"
        using f' by fastforce
      ultimately
      have eq: "((λx. (x, (h  f') x)) ` T) =
                {p. x. x  S  (x, p)  (S × UNIV)  ((λz. snd z - ((f  fst) z, (h  fst) z)) -` {0})}"
        using fim by (auto simp: image_iff)
      moreover have "closed "
        apply (intro closed_compact_projection [OF compact S] continuous_closed_preimage
                     continuous_intros continuous_on_subset [OF contf] continuous_on_subset [OF conth])
        by (auto simp: compact S closed_Times compact_imp_closed)
      ultimately show "closed ((λx. (x, (h  f') x)) ` T)"
        by simp
    qed
  qed (use f' gfh in fastforce)
qed


lemma Borsukian_open_map_image_compact:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "Borsukian S" and contf: "continuous_on S f" and fim: "f ` S = T" and "compact S"
      and ope: "U. openin (top_of_set S) U
                      openin (top_of_set T) (f ` U)"
    shows "Borsukian T"
proof (clarsimp simp add: Borsukian_continuous_logarithm_circle_real)
  fix g :: "'b  complex"
  assume contg: "continuous_on T g" and gim: "g  T  sphere 0 1"
  have "continuous_on S (g  f)"
    using contf contg continuous_on_compose fim by blast
  moreover have "(g  f)  S  sphere 0 1"
    using fim gim by auto
  ultimately obtain h where cont_cxh: "continuous_on S (complex_of_real  h)"
                       and gfh: "x. x  S  (g  f) x = exp(𝗂 * of_real(h x))"
    using Borsukian S Borsukian_continuous_logarithm_circle_real  by metis
  then have conth: "continuous_on S h"
    by simp
  have "x. x  S  f x = y  (x'  S. f x' = y  h x  h x')" if "y  T" for y
  proof -
    have 1: "compact (h ` {x  S. f x = y})"
    proof (rule compact_continuous_image)
      show "continuous_on {x  S. f x = y} h"
        by (rule continuous_on_subset [OF conth]) auto
      have "compact (S  f -` {y})"
        using that proper_map_from_compact [OF contf _ compact S] fim
        by force
      then show "compact {x  S. f x = y}" 
        by (auto simp: vimage_def Int_def)
    qed
    have 2: "h ` {x  S. f x = y}  {}"
      using fim that by auto
    have "s  h ` {x  S. f x = y}. t  h ` {x  S. f x = y}. s  t"
      using compact_attains_inf [OF 1 2] by blast
    then show ?thesis by auto
  qed
  then obtain k where kTS: "y. y  T  k y  S"
                  and fk:  "y. y  T  f (k y) = y "
                  and hle: "x' y. y  T; x'  S; f x' = y  h (k y)  h x'"
    by metis
  have "continuous_on T (h  k)"
  proof (clarsimp simp add: continuous_on_iff)
    fix y and e::real
    assume "y  T" "0 < e"
    moreover have "uniformly_continuous_on S (complex_of_real  h)"
      using compact S cont_cxh compact_uniformly_continuous by blast
    ultimately obtain d where "0 < d"
                  and d: "x x'. xS; x'S; dist x' x < d  dist (h x') (h x) < e"
      by (force simp: uniformly_continuous_on_def)
    obtain δ where "0 < δ" and δ:
      "x'. x'  T; dist y x' < δ
                (v  {z  S. f z = y}. v'. v'  {z  S. f z = x'}  dist v v' < d) 
                   (v'  {z  S. f z = x'}. v. v  {z  S. f z = y}  dist v' v < d)"
    proof (rule upper_lower_hemicontinuous_explicit [of T "λy. {z  S. f z = y}" S])
      show "U. openin (top_of_set S) U
                  openin (top_of_set T) {x  T. {z  S. f z = x}  U}"
        using closed_map_iff_upper_hemicontinuous_preimage [OF fim [THEN equalityD1]]
        by (simp add: Abstract_Topology_2.continuous_imp_closed_map compact S contf fim)
      show "U. closedin (top_of_set S) U 
                 closedin (top_of_set T) {x  T. {z  S. f z = x}  U}"
        using ope open_map_iff_lower_hemicontinuous_preimage [OF fim [THEN equalityD1]]
        by meson
      show "bounded {z  S. f z = y}"
        by (metis (no_types, lifting) compact_imp_bounded [OF compact S] bounded_subset mem_Collect_eq subsetI)
    qed (use y  T 0 < d fk kTS in force+)
    have "dist (h (k y')) (h (k y)) < e" if "y'  T" "dist y y' < δ" for y'
    proof -
      have k1: "k y  S" "f (k y) = y" and k2: "k y'  S" "f (k y') = y'"
        by (auto simp: y  T y'  T kTS fk)
      have 1: "v. v  S; f v = y  v'. v'  {z  S. f z = y'}  dist v v' < d"
       and 2: "v'. v'  S; f v' = y'  v. v  {z  S. f z = y}  dist v' v < d"
        using δ [OF that] by auto
      then obtain w' w where "w'  S" "f w' = y'" "dist (k y) w' < d"
        and "w  S" "f w = y" "dist (k y') w < d"
        using 1 [OF k1] 2 [OF k2] by auto
      then show ?thesis
        using d [of w "k y'"] d [of w' "k y"] k1 k2 y'  T  y  T hle
        by (fastforce simp: dist_norm abs_diff_less_iff algebra_simps)
    qed
    then show "d>0. x'T. dist x' y < d  dist (h (k x')) (h (k y)) < e"
      using 0 < δ by (auto simp: dist_commute)
  qed
  then show "h. continuous_on T h  (xT. g x = exp (𝗂 * complex_of_real (h x)))"
    using fk gfh kTS by force
qed


text‹If two points are separated by a closed set, there's a minimal one.›
proposition closed_irreducible_separator:
  fixes a :: "'a::real_normed_vector"
  assumes "closed S" and ab: "¬ connected_component (- S) a b"
  obtains T where "T  S" "closed T" "T  {}" "¬ connected_component (- T) a b"
                  "U. U  T  connected_component (- U) a b"
proof (cases "a  S  b  S")
  case True
  then show ?thesis
  proof
    assume *: "a  S"
    show ?thesis
    proof
      show "{a}  S"
        using * by blast
      show "¬ connected_component (- {a}) a b"
        using connected_component_in by auto
      show "U. U  {a}  connected_component (- U) a b"
        by (metis connected_component_UNIV UNIV_I compl_bot_eq connected_component_eq_eq less_le_not_le subset_singletonD)
    qed auto
  next
    assume *: "b  S"
    show ?thesis
    proof
      show "{b}  S"
        using * by blast
      show "¬ connected_component (- {b}) a b"
        using connected_component_in by auto
      show "U. U  {b}  connected_component (- U) a b"
        by (metis connected_component_UNIV UNIV_I compl_bot_eq connected_component_eq_eq less_le_not_le subset_singletonD)
    qed auto
  qed
next
  case False
  define A where "A  connected_component_set (- S) a"
  define B where "B  connected_component_set (- (closure A)) b"
  have "a  A"
    using False A_def by auto
  have "b  B"
    unfolding A_def B_def closure_Un_frontier
    using ab False closed S frontier_complement frontier_of_connected_component_subset frontier_subset_closed by force
  have "frontier B  frontier (connected_component_set (- closure A) b)"
    using B_def by blast
  also have frsub: "...  frontier A"
  proof -
    have "A. closure (- closure (- A))  closure A"
      by (metis (no_types) closure_mono closure_subset compl_le_compl_iff double_compl)
    then show ?thesis
      by (metis (no_types) closure_closure double_compl frontier_closures frontier_of_connected_component_subset le_inf_iff subset_trans)
  qed
  finally have frBA: "frontier B  frontier A" .
  show ?thesis
  proof
    show "frontier B  S"
    proof -
      have "frontier S  S"
        by (simp add: closed S frontier_subset_closed)
      then show ?thesis
        using frsub frontier_complement frontier_of_connected_component_subset
        unfolding A_def B_def by blast
    qed
    show "closed (frontier B)"
      by simp
    show "¬ connected_component (- frontier B) a b"
      unfolding connected_component_def
    proof clarify
      fix T
      assume "connected T" and TB: "T  - frontier B" and "a  T" and "b  T"
      have "a  B"
        by (metis A_def B_def ComplD a  A assms(1) closed_open connected_component_subset in_closure_connected_component subsetD)
      have "T  B  {}"
        using b  B b  T by blast
      moreover have "T - B  {}"
        using a  B a  T by blast
      ultimately show "False"
        using connected_Int_frontier [of T B] TB connected T by blast
    qed
    moreover have "connected_component (- frontier B) a b" if "frontier B = {}"
      using connected_component_eq_UNIV that by auto
    ultimately show "frontier B  {}"
      by blast
    show "connected_component (- U) a b" if "U  frontier B" for U
    proof -
      obtain p where Usub: "U  frontier B" and p: "p  frontier B" "p  U"
        using U  frontier B by blast
      show ?thesis
        unfolding connected_component_def
      proof (intro exI conjI)
        have "connected ((insert p A)  (insert p B))"
        proof (rule connected_Un)
          show "connected (insert p A)"
            by (metis A_def IntD1 frBA p  frontier B closure_insert closure_subset connected_connected_component connected_intermediate_closure frontier_closures insert_absorb subsetCE subset_insertI)
          show "connected (insert p B)"
            by (metis B_def IntD1 p  frontier B closure_insert closure_subset connected_connected_component connected_intermediate_closure frontier_closures insert_absorb subset_insertI)
        qed blast
        then show "connected (insert p (B  A))"
          by (simp add: sup.commute)
        have "A  - U"
          using A_def Usub frontier B  S connected_component_subset by fastforce
        moreover have "B  - U"
          using B_def Usub connected_component_subset frBA frontier_closures by fastforce
        ultimately show "insert p (B  A)  - U"
          using p by auto
      qed (auto simp: a  A b  B)
    qed
  qed
qed

lemma frontier_minimal_separating_closed_pointwise:
  fixes S :: "'a::real_normed_vector set"
  assumes S: "closed S" "a  S" and nconn: "¬ connected_component (- S) a b"
      and conn: "T. closed T; T  S  connected_component (- T) a b"
    shows "frontier(connected_component_set (- S) a) = S" (is "?F = S")
proof -
  have "?F  S"
    by (simp add: S componentsI frontier_of_components_closed_complement)
  moreover have False if "?F  S"
  proof -
    have "connected_component (- ?F) a b"
      by (simp add: conn that)
    then obtain T where "connected T" "T  -?F" "a  T" "b  T"
      by (auto simp: connected_component_def)
    moreover have "T  ?F  {}"
    proof (rule connected_Int_frontier [OF connected T])
      show "T  connected_component_set (- S) a  {}"
        using a  S a  T by fastforce
      show "T - connected_component_set (- S) a  {}"
        using b  T nconn by blast
    qed
    ultimately show ?thesis
      by blast
  qed
  ultimately show ?thesis
    by blast
qed


subsection‹Unicoherence (closed)›

definitiontag important› unicoherent where
  "unicoherent U 
  S T. connected S  connected T  S  T = U 
        closedin (top_of_set U) S  closedin (top_of_set U) T
         connected (S  T)"

lemma unicoherentI [intro?]:
  assumes "S T. connected S; connected T; U = S  T; closedin (top_of_set U) S; closedin (top_of_set U) T
           connected (S  T)"
  shows "unicoherent U"
  using assms unfolding unicoherent_def by blast

lemma unicoherentD:
  assumes "unicoherent U" "connected S" "connected T" "U = S  T" "closedin (top_of_set U) S" "closedin (top_of_set U) T"
  shows "connected (S  T)"
  using assms unfolding unicoherent_def by blast

proposition homeomorphic_unicoherent:
  assumes ST: "S homeomorphic T" and S: "unicoherent S"
  shows "unicoherent T"
proof -
  obtain f g where gf: "x. x  S  g (f x) = x" and fim: "T = f ` S" and gfim: "g ` f ` S = S"
    and contf: "continuous_on S f" and contg: "continuous_on (f ` S) g"
    using ST by (auto simp: homeomorphic_def homeomorphism_def)
  show ?thesis
  proof
    fix U V
    assume "connected U" "connected V" and T: "T = U  V"
      and cloU: "closedin (top_of_set T) U"
      and cloV: "closedin (top_of_set T) V"
    have "f ` (g ` U  g ` V)  U" "f ` (g ` U  g ` V)  V"
      using gf fim T by auto (metis UnCI image_iff)+
    moreover have "U  V  f ` (g ` U  g ` V)"
      using gf fim by (force simp: image_iff T)
    ultimately have "U  V = f ` (g ` U  g ` V)" by blast
    moreover have "connected (f ` (g ` U  g ` V))"
    proof (rule connected_continuous_image)
      show "continuous_on (g ` U  g ` V) f"
        using T fim gfim by (metis Un_upper1 contf continuous_on_subset image_mono inf_le1) 
      show "connected (g ` U  g ` V)"
      proof (intro conjI unicoherentD [OF S])
        show "connected (g ` U)" "connected (g ` V)"
          using connected U cloU connected V cloV
          by (metis Topological_Spaces.connected_continuous_image closedin_imp_subset contg continuous_on_subset fim)+
        show "S = g ` U  g ` V"
          using T fim gfim by auto
        have hom: "homeomorphism T S g f"
          by (simp add: contf contg fim gf gfim homeomorphism_def)
        have "closedin (top_of_set T) U" "closedin (top_of_set T) V"
          by (simp_all add: cloU cloV)
        then show "closedin (top_of_set S) (g ` U)"
                  "closedin (top_of_set S) (g ` V)"
          by (blast intro: homeomorphism_imp_closed_map [OF hom])+
      qed
    qed
    ultimately show "connected (U  V)" by metis
  qed
qed


lemma homeomorphic_unicoherent_eq:
   "S homeomorphic T  (unicoherent S  unicoherent T)"
  by (meson homeomorphic_sym homeomorphic_unicoherent)

lemma unicoherent_translation:
  fixes S :: "'a::real_normed_vector set"
  shows
   "unicoherent (image (λx. a + x) S)  unicoherent S"
  using homeomorphic_translation homeomorphic_unicoherent_eq by blast

lemma unicoherent_injective_linear_image:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "linear f" "inj f"
  shows "(unicoherent(f ` S)  unicoherent S)"
  using assms homeomorphic_unicoherent_eq linear_homeomorphic_image by blast


lemma Borsukian_imp_unicoherent:
  fixes U :: "'a::euclidean_space set"
  assumes "Borsukian U"  shows "unicoherent U"
  unfolding unicoherent_def
proof clarify
  fix S T
  assume "connected S" "connected T" "U = S  T"
     and cloS: "closedin (top_of_set (S  T)) S"
     and cloT: "closedin (top_of_set (S  T)) T"
  show "connected (S  T)"
    unfolding connected_closedin_eq
  proof clarify
    fix V W
    assume "closedin (top_of_set (S  T)) V"
       and "closedin (top_of_set (S  T)) W"
       and VW: "V  W = S  T" "V  W = {}" and "V  {}" "W  {}"
    then have cloV: "closedin (top_of_set U) V" and cloW: "closedin (top_of_set U) W"
      using U = S  T cloS cloT closedin_trans by blast+
    obtain q where contq: "continuous_on U q"
         and q01: "x. x  U  q x  {0..1::real}"
         and qV: "x. x  V  q x = 0" and qW: "x. x  W  q x = 1"
      by (rule Urysohn_local [OF cloV cloW V  W = {}, of 0 1])
         (fastforce simp: closed_segment_eq_real_ivl)
    let ?h = "λx. if x  S then exp(pi * 𝗂 * q x) else 1 / exp(pi * 𝗂 * q x)"
    have eqST: "exp(pi * 𝗂 * q x) = 1 / exp(pi * 𝗂 * q x)" if "x  S  T" for x
    proof -
      have "x  V  W"
        using that V  W = S  T by blast
      with qV qW show ?thesis by force
    qed
    obtain g where contg: "continuous_on U g"
      and circle: "g  U  sphere 0 1"
      and S: "x. x  S  g x = exp(pi * 𝗂 * q x)"
      and T: "x. x  T  g x = 1 / exp(pi * 𝗂 * q x)"
    proof
      show "continuous_on U ?h"
        unfolding U = S  T
      proof (rule continuous_on_cases_local [OF cloS cloT])
        show "continuous_on S (λx. exp (pi * 𝗂 * q x))"
        proof (intro continuous_intros)
          show "continuous_on S q"
            using U = S  T continuous_on_subset contq by blast
        qed
        show "continuous_on T (λx. 1 / exp (pi * 𝗂 * q x))"
        proof (intro continuous_intros)
          show "continuous_on T q"
            using U = S  T continuous_on_subset contq by auto
        qed auto
      qed (use eqST in auto)
    qed (use eqST in auto simp: norm_divide)
    then obtain h where conth: "continuous_on U h" and heq: "x. x  U  g x = exp (h x)"
      by (metis Borsukian_continuous_logarithm_circle assms)
    obtain v w where "v  V" "w  W"
      using V  {} W  {} by blast
    then have vw: "v  S  T" "w  S  T"
      using VW by auto
    have iff: "2 * pi  cmod (2 * of_int m * of_real pi * 𝗂 - 2 * of_int n * of_real pi * 𝗂)
           1  abs (m - n)" for m n
    proof -
      have "2 * pi  cmod (2 * of_int m * of_real pi * 𝗂 - 2 * of_int n * of_real pi * 𝗂)
             2 * pi  cmod ((2 * pi * 𝗂) * (of_int m - of_int n))"
        by (simp add: algebra_simps)
      also have "...  2 * pi  2 * pi * cmod (of_int m - of_int n)"
        by (simp add: norm_mult)
      also have "...  1  abs (m - n)"
        by simp (metis norm_of_int of_int_1_le_iff of_int_abs of_int_diff)
      finally show ?thesis .
    qed
    have *: "n::int. h x - (pi * 𝗂 * q x) = (of_int(2*n) * pi) * 𝗂" if "x  S" for x
      using that S U = S  T heq exp_eq [symmetric] by (simp add: algebra_simps)
    moreover have "(λx. h x - (pi * 𝗂 * q x)) constant_on S"
    proof (rule continuous_discrete_range_constant [OF connected S])
      have "continuous_on S h" "continuous_on S q"
        using U = S  T continuous_on_subset conth contq by blast+
      then show "continuous_on S (λx. h x - (pi * 𝗂 * q x))"
        by (intro continuous_intros)
      have "2*pi  cmod (h y - (pi * 𝗂 * q y) - (h x - (pi * 𝗂 * q x)))"
        if "x  S" "y  S" and ne: "h y - (pi * 𝗂 * q y)  h x - (pi * 𝗂 * q x)" for x y
        using * [OF x  S] * [OF y  S] ne by (auto simp: iff)
      then show "x. x  S 
         e>0. y. y  S  h y - (pi * 𝗂 * q y)  h x - (pi * 𝗂 * q x) 
                   e  cmod (h y - (pi * 𝗂 * q y) - (h x - (pi * 𝗂 * q x)))"
        by (rule_tac x="2*pi" in exI) auto
    qed
    ultimately
    obtain m where m: "x. x  S  h x - (pi * 𝗂 * q x) = (of_int(2*m) * pi) * 𝗂"
      using vw by (force simp: constant_on_def)
    have *: "n::int. h x = - (pi * 𝗂 * q x) + (of_int(2*n) * pi) * 𝗂" if "x  T" for x
      unfolding exp_eq [symmetric]
      using that T U = S  T by (simp add: exp_minus field_simps  heq [symmetric])
    moreover have "(λx. h x + (pi * 𝗂 * q x)) constant_on T"
    proof (rule continuous_discrete_range_constant [OF connected T])
      have "continuous_on T h" "continuous_on T q"
        using U = S  T continuous_on_subset conth contq by blast+
      then show "continuous_on T (λx. h x + (pi * 𝗂 * q x))"
        by (intro continuous_intros)
      have "2*pi  cmod (h y + (pi * 𝗂 * q y) - (h x + (pi * 𝗂 * q x)))"
        if "x  T" "y  T" and ne: "h y + (pi * 𝗂 * q y)  h x + (pi * 𝗂 * q x)" for x y
        using * [OF x  T] * [OF y  T] ne by (auto simp: iff)
      then show "x. x  T 
         e>0. y. y  T  h y + (pi * 𝗂 * q y)  h x + (pi * 𝗂 * q x) 
                   e  cmod (h y + (pi * 𝗂 * q y) - (h x + (pi * 𝗂 * q x)))"
        by (rule_tac x="2*pi" in exI) auto
    qed
    ultimately
    obtain n where n: "x. x  T  h x + (pi * 𝗂 * q x) = (of_int(2*n) * pi) * 𝗂"
      using vw by (force simp: constant_on_def)
    show "False"
      using m [of v] m [of w] n [of v] n [of w] vw
      by (auto simp: algebra_simps v  V w  W qV qW)
  qed
qed


corollary contractible_imp_unicoherent:
  fixes U :: "'a::euclidean_space set"
  assumes "contractible U"  shows "unicoherent U"
  by (simp add: Borsukian_imp_unicoherent assms contractible_imp_Borsukian)

corollary convex_imp_unicoherent:
  fixes U :: "'a::euclidean_space set"
  assumes "convex U"  shows "unicoherent U"
  by (simp add: Borsukian_imp_unicoherent assms convex_imp_Borsukian)

text‹If the type class constraint can be relaxed, I don't know how!›
corollary unicoherent_UNIV: "unicoherent (UNIV :: 'a :: euclidean_space set)"
  by (simp add: convex_imp_unicoherent)


lemma unicoherent_monotone_image_compact:
  fixes T :: "'b :: t2_space set"
  assumes S: "unicoherent S" "compact S" and contf: "continuous_on S f" and fim: "f ` S = T"
  and conn: "y. y  T  connected (S  f -` {y})"
  shows "unicoherent T"
proof
  fix U V
  assume UV: "connected U" "connected V" "T = U  V"
     and cloU: "closedin (top_of_set T) U"
     and cloV: "closedin (top_of_set T) V"
  moreover have "compact T"
    using compact S compact_continuous_image contf fim by blast
  ultimately have "closed U" "closed V"
    by (auto simp: closedin_closed_eq compact_imp_closed)
  let ?SUV = "(S  f -` U)  (S  f -` V)"
  have UV_eq: "f ` ?SUV = U  V"
    using T = U  V fim by force+
  have "connected (f ` ?SUV)"
  proof (rule connected_continuous_image)
    show "continuous_on ?SUV f"
      by (meson contf continuous_on_subset inf_le1)
    show "connected ?SUV"
    proof (rule unicoherentD [OF unicoherent S, of "S  f -` U" "S  f -` V"])
      have "C. closedin (top_of_set S) C  closedin (top_of_set T) (f ` C)"
        by (metis compact S closed_subset closedin_compact closedin_imp_subset compact_continuous_image compact_imp_closed contf continuous_on_subset fim image_mono)
      then show "connected (S  f -` U)" "connected (S  f -` V)"
        using UV by (auto simp: conn intro: connected_closed_monotone_preimage [OF contf fim])
      show "S = (S  f -` U)  (S  f -` V)"
        using UV fim by blast
      show "closedin (top_of_set S) (S  f -` U)"
            "closedin (top_of_set S) (S  f -` V)"
        by (auto simp: continuous_on_imp_closedin cloU cloV contf fim)
    qed
  qed
  with UV_eq show "connected (U  V)"
    by simp
qed


subsection‹Several common variants of unicoherence›

lemma connected_frontier_simple:
  fixes S :: "'a :: euclidean_space set"
  assumes "connected S" "connected(- S)" shows "connected(frontier S)"
  unfolding frontier_closures
  by (rule unicoherentD [OF unicoherent_UNIV]; simp add: assms connected_imp_connected_closure flip: closure_Un)

lemma connected_frontier_component_complement:
  fixes S :: "'a :: euclidean_space set"
  assumes "connected S" "C  components(- S)" shows "connected(frontier C)"
  by (meson assms component_complement_connected connected_frontier_simple in_components_connected)

lemma connected_frontier_disjoint:
  fixes S :: "'a :: euclidean_space set"
  assumes "connected S" "connected T" "disjnt S T" and ST: "frontier S  frontier T"
  shows "connected(frontier S)"
proof (cases "S = UNIV")
  case True then show ?thesis
    by simp
next
  case False
  then have "-S  {}"
    by blast
  then obtain C where C: "C  components(- S)" and "T  C"
    by (metis ComplI disjnt_iff subsetI exists_component_superset disjnt S T connected T)
  moreover have "frontier S = frontier C"
  proof -
    have "frontier C  frontier S"
      using C frontier_complement frontier_of_components_subset by blast
    moreover have "x  frontier C" if "x  frontier S" for x
    proof -
      have "x  closure C"
        using that unfolding frontier_def
        by (metis (no_types) Diff_eq ST T  C closure_mono contra_subsetD frontier_def le_inf_iff that)
      moreover have "x  interior C"
        using that unfolding frontier_def
        by (metis C Compl_eq_Diff_UNIV Diff_iff subsetD in_components_subset interior_diff interior_mono)
      ultimately show ?thesis
        by (auto simp: frontier_def)
    qed
    ultimately show ?thesis
      by blast
  qed
  ultimately show ?thesis
    using connected S connected_frontier_component_complement by auto
qed


subsection‹Some separation results›

lemma separation_by_component_closed_pointwise:
  fixes S :: "'a :: euclidean_space set"
  assumes "closed S" "¬ connected_component (- S) a b"
  obtains C where "C  components S" "¬ connected_component(- C) a b"
proof (cases "a  S  b  S")
  case True
  then show ?thesis
    using connected_component_in componentsI that by fastforce
next
  case False
  obtain T where "T  S" "closed T" "T  {}"
             and nab: "¬ connected_component (- T) a b"
             and conn: "U. U  T  connected_component (- U) a b"
    using closed_irreducible_separator [OF assms] by metis
  moreover have "connected T"
  proof -
    have ab: "frontier(connected_component_set (- T) a) = T" "frontier(connected_component_set (- T) b) = T"
      using frontier_minimal_separating_closed_pointwise
      by (metis False T  S closed T connected_component_sym conn connected_component_eq_empty connected_component_intermediate_subset empty_subsetI nab)+
    have "connected (frontier (connected_component_set (- T) a))"
    proof (rule connected_frontier_disjoint)
      show "disjnt (connected_component_set (- T) a) (connected_component_set (- T) b)"
        unfolding disjnt_iff
        by (metis connected_component_eq connected_component_eq_empty connected_component_idemp mem_Collect_eq nab)
      show "frontier (connected_component_set (- T) a)  frontier (connected_component_set (- T) b)"
        by (simp add: ab)
    qed auto
    with ab closed T show ?thesis
      by simp
  qed
  ultimately obtain C where "C  components S" "T  C"
    using exists_component_superset [of T S] by blast
  then show ?thesis
    by (meson Compl_anti_mono connected_component_of_subset nab that)
qed


lemma separation_by_component_closed:
  fixes S :: "'a :: euclidean_space set"
  assumes "closed S" "¬ connected(- S)"
  obtains C where "C  components S" "¬ connected(- C)"
proof -
  obtain x y where "closed S" "x  S" "y  S" and "¬ connected_component (- S) x y"
    using assms by (auto simp: connected_iff_connected_component)
  then obtain C where "C  components S" "¬ connected_component(- C) x y"
    using separation_by_component_closed_pointwise by metis
  then show "thesis"
    by (metis Compl_iff x  S y  S connected_component_eq_self in_components_subset mem_Collect_eq subsetD that)
qed

lemma separation_by_Un_closed_pointwise:
  fixes S :: "'a :: euclidean_space set"
  assumes ST: "closed S" "closed T" "S  T = {}"
      and conS: "connected_component (- S) a b" and conT: "connected_component (- T) a b"
    shows "connected_component (- (S  T)) a b"
proof (rule ccontr)
  have "a  S" "b  S" "a  T" "b  T"
    using conS conT connected_component_in by auto
  assume "¬ connected_component (- (S  T)) a b"
  then obtain C where "C  components (S  T)" and C: "¬ connected_component(- C) a b"
    using separation_by_component_closed_pointwise assms by blast
  then have "C  S  C  T"
  proof -
    have "connected C" "C  S  T"
      using C  components (S  T) in_components_subset by (blast elim: componentsE)+
    moreover then have "C  T = {}  C  S = {}"
      by (metis Int_empty_right ST inf.commute connected_closed)
    ultimately show ?thesis
      by blast
  qed
  then show False
    by (meson Compl_anti_mono C conS conT connected_component_of_subset)
qed

lemma separation_by_Un_closed:
  fixes S :: "'a :: euclidean_space set"
  assumes ST: "closed S" "closed T" "S  T = {}" and conS: "connected(- S)" and conT: "connected(- T)"
  shows "connected(- (S  T))"
  using assms separation_by_Un_closed_pointwise
  by (fastforce simp add: connected_iff_connected_component)

lemma open_unicoherent_UNIV:
  fixes S :: "'a :: euclidean_space set"
  assumes "open S" "open T" "connected S" "connected T" "S  T = UNIV"
  shows "connected(S  T)"
proof -
  have "connected(- (-S  -T))"
    by (metis closed_Compl compl_sup compl_top_eq double_compl separation_by_Un_closed assms)
  then show ?thesis
    by simp
qed

lemma separation_by_component_open_aux:
  fixes S :: "'a :: euclidean_space set"
  assumes ST: "closed S" "closed T" "S  T = {}"
      and "S  {}" "T  {}"
  obtains C where "C  components(-(S  T))" "C  {}" "frontier C  S  {}" "frontier C  T  {}"
proof (rule ccontr)
  let ?S = "S  {C  components(- (S  T)). frontier C  S}"
  let ?T = "T  {C  components(- (S  T)). frontier C  T}"
  assume "¬ thesis"
  with that have *: "frontier C  S = {}  frontier C  T = {}"
            if C: "C  components (- (S  T))" "C  {}" for C
    using C by blast
  have "A B::'a set. closed A  closed B  UNIV  A  B  A  B = {}  A  {}  B  {}"
  proof (intro exI conjI)
    have "frontier ({C  components (- S  - T). frontier C  S})  S"
      using subset_trans [OF frontier_Union_subset_closure]
      by (metis (no_types, lifting) SUP_least closed S closure_minimal mem_Collect_eq)
    then have "frontier ?S  S"
      by (simp add: frontier_subset_eq assms  subset_trans [OF frontier_Un_subset])
    then show "closed ?S"
      using frontier_subset_eq by fastforce
    have "frontier ({C  components (- S  - T). frontier C  T})  T"
      using subset_trans [OF frontier_Union_subset_closure]
      by (metis (no_types, lifting) SUP_least closed T closure_minimal mem_Collect_eq)
    then have "frontier ?T  T"
      by (simp add: frontier_subset_eq assms  subset_trans [OF frontier_Un_subset])
    then show "closed ?T"
      using frontier_subset_eq by fastforce
    have "UNIV  (S  T)  (components(- (S  T)))"
      using Union_components by blast
    also have "...   ?S  ?T"
    proof -
      have "C  components (-(S  T))  frontier C  S 
            C  components (-(S  T))  frontier C  T"
        if "C  components (- (S  T))" "C  {}" for C
        using * [OF that] that
        by clarify (metis (no_types, lifting) UnE closed S closed T closed_Un disjoint_iff_not_equal frontier_of_components_closed_complement subsetCE)
      then show ?thesis
        by blast
    qed
    finally show "UNIV  ?S  ?T" .
    have "{C  components (- (S  T)). frontier C  S} 
          {C  components (- (S  T)). frontier C  T}  - (S  T)"
      using in_components_subset by fastforce
    moreover have "{C  components (- (S  T)). frontier C  S} 
                   {C  components (- (S  T)). frontier C  T} = {}"
    proof -
      have "C  C' = {}" if "C  components (- (S  T))" "frontier C  S"
                            "C'  components (- (S  T))" "frontier C'  T" for C C'
      proof -
        have NUN: "- S  - T  UNIV"
          using T  {} by blast
        have "C  C'"
        proof
          assume "C = C'"
          with that have "frontier C'  S  T"
            by simp
          also have "... = {}"
            using S  T = {} by blast
          finally have "C' = {}  C' = UNIV"
            using frontier_eq_empty by auto
          then show False
            using C = C' NUN that by (force simp: dest: in_components_nonempty in_components_subset)
        qed
        with that show ?thesis
          by (simp add: components_nonoverlap [of _ "-(S  T)"])
      qed
      then show ?thesis
        by blast
    qed
    ultimately show "?S  ?T = {}"
      using ST by blast
    show "?S  {}" "?T  {}"
      using S  {} T  {} by blast+
  qed
    then show False
      by (metis Compl_disjoint connected_UNIV compl_bot_eq compl_unique connected_closedD inf_sup_absorb sup_compl_top_left1 top.extremum_uniqueI)
qed


proposition separation_by_component_open:
  fixes S :: "'a :: euclidean_space set"
  assumes "open S" and non: "¬ connected(- S)"
  obtains C where "C  components S" "¬ connected(- C)"
proof -
  obtain T U
    where "closed T" "closed U" and TU: "T  U = - S" "T  U = {}" "T  {}" "U  {}"
    using assms by (auto simp: connected_closed_set closed_def)
  then obtain C where C: "C  components(-(T  U))" "C  {}"
          and "frontier C  T  {}" "frontier C  U  {}"
    using separation_by_component_open_aux [OF closed T closed U T  U = {}] by force
  show "thesis"
  proof
    show "C  components S"
      using C(1) TU(1) by auto
    show "¬ connected (- C)"
    proof
      assume "connected (- C)"
      then have "connected (frontier C)"
        using connected_frontier_simple [of C] C  components S in_components_connected by blast
      then show False
        unfolding connected_closed
        by (metis C(1) TU(2) closed T closed U frontier C  T  {} frontier C  U  {} closed_Un frontier_of_components_closed_complement inf_bot_right inf_commute)
    qed
  qed
qed

lemma separation_by_Un_open:
  fixes S :: "'a :: euclidean_space set"
  assumes "open S" "open T" "S  T = {}" and cS: "connected(-S)" and cT: "connected(-T)"
    shows "connected(- (S  T))"
  using assms unicoherent_UNIV unfolding unicoherent_def by force


lemma nonseparation_by_component_eq:
  fixes S :: "'a :: euclidean_space set"
  assumes "open S  closed S"
  shows "((C  components S. connected(-C))  connected(- S))" (is "?lhs = ?rhs")
proof
  assume ?lhs with assms show ?rhs
    by (meson separation_by_component_closed separation_by_component_open)
next
  assume ?rhs with assms show ?lhs
    using component_complement_connected by force
qed


text‹Another interesting equivalent of an inessential mapping into C-{0}›
proposition inessential_eq_extensible:
  fixes f :: "'a::euclidean_space  complex"
  assumes "closed S"
  shows "(a. homotopic_with_canon (λh. True) S (-{0}) f (λt. a)) 
         (g. continuous_on UNIV g  (x  S. g x = f x)  (x. g x  0))"
     (is "?lhs = ?rhs")
proof
  assume ?lhs
  then obtain a where a: "homotopic_with_canon (λh. True) S (-{0}) f (λt. a)" ..
  show ?rhs
  proof (cases "S = {}")
    case True
    with a show ?thesis by force
  next
    case False
    have anr: "ANR (-{0::complex})"
      by (simp add: ANR_delete open_Compl open_imp_ANR)
    obtain g where contg: "continuous_on UNIV g" and gim: "g ` UNIV  -{0}"
                   and gf: "x. x  S  g x = f x"
    proof (rule Borsuk_homotopy_extension_homotopic [OF _ _ continuous_on_const _ homotopic_with_symD [OF a]])
      show "closedin (top_of_set UNIV) S"
        using assms by auto
      show "(λt. a)  UNIV  - {0}"
        using a homotopic_with_imp_subset2 False by blast
    qed (use anr that in force+)
    then show ?thesis
      by force
  qed
next
  assume ?rhs
  then obtain g where contg: "continuous_on UNIV g"
          and gf: "x. x  S  g x = f x" and non0: "x. g x  0"
    by metis
  obtain h k::"'a'a" where hk: "homeomorphism (ball 0 1) UNIV h k"
    using homeomorphic_ball01_UNIV homeomorphic_def by blast
  then have "continuous_on (ball 0 1) (g  h)"
    by (meson contg continuous_on_compose continuous_on_subset homeomorphism_cont1 top_greatest)
  then obtain j where contj: "continuous_on (ball 0 1) j"
                  and j: "z. z  ball 0 1  exp(j z) = (g  h) z"
    by (metis (mono_tags, opaque_lifting) continuous_logarithm_on_ball comp_apply non0)
  have [simp]: "x. x  S  h (k x) = x"
    using hk homeomorphism_apply2 by blast
  have "ζ. continuous_on S ζ (xS. f x = exp (ζ x))"
  proof (intro exI conjI ballI)
    show "continuous_on S (j  k)"
    proof (rule continuous_on_compose)
      show "continuous_on S k"
        by (meson continuous_on_subset hk homeomorphism_cont2 top_greatest)
      show "continuous_on (k ` S) j"
        by (auto intro: continuous_on_subset [OF contj] simp flip: homeomorphism_image2 [OF hk])
    qed
    show "f x = exp ((j  k) x)" if "x  S" for x
    proof -
      have "f x = (g  h) (k x)"
        by (simp add: gf that)
      also have "... = exp (j (k x))"
        by (metis rangeI homeomorphism_image2 [OF hk] j)
      finally show ?thesis by simp
    qed
  qed
  then show ?lhs
    by (simp add: inessential_eq_continuous_logarithm)
qed

lemma inessential_on_clopen_Union:
  fixes  :: "'a::euclidean_space set set"
  assumes T: "path_connected T"
      and "S. S    closedin (top_of_set ()) S"
      and "S. S    openin (top_of_set ()) S"
      and hom: "S. S    a. homotopic_with_canon (λx. True) S T f (λx. a)"
  obtains a where "homotopic_with_canon (λx. True) () T f (λx. a)"
proof (cases " = {}")
  case True
  with that show ?thesis
    using homotopic_with_canon_on_empty by fastforce
next
  case False
  then obtain C where "C  " "C  {}"
    by blast
  then obtain a where clo: "closedin (top_of_set ()) C"
    and ope: "openin (top_of_set ()) C"
    and "homotopic_with_canon (λx. True) C T f (λx. a)"
    using assms by blast
  with C  {} have "f ` C  T" "a  T"
    using homotopic_with_imp_subset1 homotopic_with_imp_subset2 by blast+
  have "homotopic_with_canon (λx. True) () T f (λx. a)"
  proof (rule homotopic_on_clopen_Union)
    show "S. S    closedin (top_of_set ()) S"
         "S. S    openin (top_of_set ()) S"
      by (simp_all add: assms)
    show "homotopic_with_canon (λx. True) S T f (λx. a)" if "S  " for S
    proof (cases "S = {}")
      case False
      then obtain b where "b  S"
        by blast
      obtain c where c: "homotopic_with_canon (λx. True) S T f (λx. c)"
        using S   hom by blast
      then have "c  T"
        using b  S homotopic_with_imp_subset2 by blast
      then have "homotopic_with_canon (λx. True) S T (λx. a) (λx. c)"
        using T a  T by (simp add: homotopic_constant_maps path_connected_component)
      then show ?thesis
        using c homotopic_with_symD homotopic_with_trans by blast
    qed (simp add: homotopic_on_empty)
  qed
  then show ?thesis ..
qed

proposition Janiszewski_dual:
  fixes S :: "complex set"
  assumes
   "compact S" "compact T" "connected S" "connected T" "connected(- (S  T))"
 shows "connected(S  T)"
proof -
  have ST: "compact (S  T)"
    by (simp add: assms compact_Un)
  with Borsukian_imp_unicoherent [of "S  T"] ST assms
  show ?thesis
    by (simp add: Borsukian_separation_compact closed_subset compact_imp_closed unicoherentD)
qed

end