Theory Homeomorphism

theory Homeomorphism
imports Path_Connected
(*  Title:      HOL/Analysis/Homeomorphism.thy
    Author: LC Paulson (ported from HOL Light)
*)

section ‹Homeomorphism Theorems›

theory Homeomorphism
imports Path_Connected
begin

lemma homeomorphic_spheres':
  fixes a ::"'a::euclidean_space" and b ::"'b::euclidean_space"
  assumes "0 < δ" and dimeq: "DIM('a) = DIM('b)"
  shows "(sphere a δ) homeomorphic (sphere b δ)"
proof -
  obtain f :: "'a⇒'b" and g where "linear f" "linear g"
     and fg: "⋀x. norm(f x) = norm x" "⋀y. norm(g y) = norm y" "⋀x. g(f x) = x" "⋀y. f(g y) = y"
    by (blast intro: isomorphisms_UNIV_UNIV [OF dimeq])
  then have "continuous_on UNIV f" "continuous_on UNIV g"
    using linear_continuous_on linear_linear by blast+
  then show ?thesis
    unfolding homeomorphic_minimal
    apply(rule_tac x="λx. b + f(x - a)" in exI)
    apply(rule_tac x="λx. a + g(x - b)" in exI)
    using assms
    apply (force intro: continuous_intros
                  continuous_on_compose2 [of _ f] continuous_on_compose2 [of _ g] simp: dist_commute dist_norm fg)
    done
qed

lemma homeomorphic_spheres_gen:
    fixes a :: "'a::euclidean_space" and b :: "'b::euclidean_space"
  assumes "0 < r" "0 < s" "DIM('a::euclidean_space) = DIM('b::euclidean_space)"
  shows "(sphere a r homeomorphic sphere b s)"
  apply (rule homeomorphic_trans [OF homeomorphic_spheres homeomorphic_spheres'])
  using assms  apply auto
  done

subsection ‹Homeomorphism of all convex compact sets with nonempty interior›

proposition ray_to_rel_frontier:
  fixes a :: "'a::real_inner"
  assumes "bounded S"
      and a: "a ∈ rel_interior S"
      and aff: "(a + l) ∈ affine hull S"
      and "l ≠ 0"
  obtains d where "0 < d" "(a + d *R l) ∈ rel_frontier S"
           "⋀e. ⟦0 ≤ e; e < d⟧ ⟹ (a + e *R l) ∈ rel_interior S"
proof -
  have aaff: "a ∈ affine hull S"
    by (meson a hull_subset rel_interior_subset rev_subsetD)
  let ?D = "{d. 0 < d ∧ a + d *R l ∉ rel_interior S}"
  obtain B where "B > 0" and B: "S ⊆ ball a B"
    using bounded_subset_ballD [OF ‹bounded S›] by blast
  have "a + (B / norm l) *R l ∉ ball a B"
    by (simp add: dist_norm ‹l ≠ 0›)
  with B have "a + (B / norm l) *R l ∉ rel_interior S"
    using rel_interior_subset subsetCE by blast
  with ‹B > 0› ‹l ≠ 0› have nonMT: "?D ≠ {}"
    using divide_pos_pos zero_less_norm_iff by fastforce
  have bdd: "bdd_below ?D"
    by (metis (no_types, lifting) bdd_belowI le_less mem_Collect_eq)
  have relin_Ex: "⋀x. x ∈ rel_interior S ⟹
                    ∃e>0. ∀x'∈affine hull S. dist x' x < e ⟶ x' ∈ rel_interior S"
    using openin_rel_interior [of S] by (simp add: openin_euclidean_subtopology_iff)
  define d where "d = Inf ?D"
  obtain ε where "0 < ε" and ε: "⋀η. ⟦0 ≤ η; η < ε⟧ ⟹ (a + η *R l) ∈ rel_interior S"
  proof -
    obtain e where "e>0"
            and e: "⋀x'. x' ∈ affine hull S ⟹ dist x' a < e ⟹ x' ∈ rel_interior S"
      using relin_Ex a by blast
    show thesis
    proof (rule_tac ε = "e / norm l" in that)
      show "0 < e / norm l" by (simp add: ‹0 < e› ‹l ≠ 0›)
    next
      show "a + η *R l ∈ rel_interior S" if "0 ≤ η" "η < e / norm l" for η
      proof (rule e)
        show "a + η *R l ∈ affine hull S"
          by (metis (no_types) add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff)
        show "dist (a + η *R l) a < e"
          using that by (simp add: ‹l ≠ 0› dist_norm pos_less_divide_eq)
      qed
    qed
  qed
  have inint: "⋀e. ⟦0 ≤ e; e < d⟧ ⟹ a + e *R l ∈ rel_interior S"
    unfolding d_def using cInf_lower [OF _ bdd]
    by (metis (no_types, lifting) a add.right_neutral le_less mem_Collect_eq not_less real_vector.scale_zero_left)
  have "ε ≤ d"
    unfolding d_def
    apply (rule cInf_greatest [OF nonMT])
    using ε dual_order.strict_implies_order le_less_linear by blast
  with ‹0 < ε› have "0 < d" by simp
  have "a + d *R l ∉ rel_interior S"
  proof
    assume adl: "a + d *R l ∈ rel_interior S"
    obtain e where "e > 0"
             and e: "⋀x'. x' ∈ affine hull S ⟹ dist x' (a + d *R l) < e ⟹ x' ∈ rel_interior S"
      using relin_Ex adl by blast
    have "d + e / norm l ≤ Inf {d. 0 < d ∧ a + d *R l ∉ rel_interior S}"
    proof (rule cInf_greatest [OF nonMT], clarsimp)
      fix x::real
      assume "0 < x" and nonrel: "a + x *R l ∉ rel_interior S"
      show "d + e / norm l ≤ x"
      proof (cases "x < d")
        case True with inint nonrel ‹0 < x›
          show ?thesis by auto
      next
        case False
          then have dle: "x < d + e / norm l ⟹ dist (a + x *R l) (a + d *R l) < e"
            by (simp add: field_simps ‹l ≠ 0›)
          have ain: "a + x *R l ∈ affine hull S"
            by (metis add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff)
          show ?thesis
            using e [OF ain] nonrel dle by force
      qed
    qed
    then show False
      using ‹0 < e› ‹l ≠ 0› by (simp add: d_def [symmetric] divide_simps)
  qed
  moreover have "a + d *R l ∈ closure S"
  proof (clarsimp simp: closure_approachable)
    fix η::real assume "0 < η"
    have 1: "a + (d - min d (η / 2 / norm l)) *R l ∈ S"
      apply (rule subsetD [OF rel_interior_subset inint])
      using ‹l ≠ 0› ‹0 < d› ‹0 < η› by auto
    have "norm l * min d (η / (norm l * 2)) ≤ norm l * (η / (norm l * 2))"
      by (metis min_def mult_left_mono norm_ge_zero order_refl)
    also have "... < η"
      using ‹l ≠ 0› ‹0 < η› by (simp add: divide_simps)
    finally have 2: "norm l * min d (η / (norm l * 2)) < η" .
    show "∃y∈S. dist y (a + d *R l) < η"
      apply (rule_tac x="a + (d - min d (η / 2 / norm l)) *R l" in bexI)
      using 1 2 ‹0 < d› ‹0 < η› apply (auto simp: algebra_simps)
      done
  qed
  ultimately have infront: "a + d *R l ∈ rel_frontier S"
    by (simp add: rel_frontier_def)
  show ?thesis
    by (rule that [OF ‹0 < d› infront inint])
qed

corollary ray_to_frontier:
  fixes a :: "'a::euclidean_space"
  assumes "bounded S"
      and a: "a ∈ interior S"
      and "l ≠ 0"
  obtains d where "0 < d" "(a + d *R l) ∈ frontier S"
           "⋀e. ⟦0 ≤ e; e < d⟧ ⟹ (a + e *R l) ∈ interior S"
proof -
  have "interior S = rel_interior S"
    using a rel_interior_nonempty_interior by auto
  then have "a ∈ rel_interior S"
    using a by simp
  then show ?thesis
    apply (rule ray_to_rel_frontier [OF ‹bounded S› _ _ ‹l ≠ 0›])
     using a affine_hull_nonempty_interior apply blast
    by (simp add: ‹interior S = rel_interior S› frontier_def rel_frontier_def that)
qed


lemma segment_to_rel_frontier_aux:
  fixes x :: "'a::euclidean_space"
  assumes "convex S" "bounded S" and x: "x ∈ rel_interior S" and y: "y ∈ S" and xy: "x ≠ y"
  obtains z where "z ∈ rel_frontier S" "y ∈ closed_segment x z"
                   "open_segment x z ⊆ rel_interior S"
proof -
  have "x + (y - x) ∈ affine hull S"
    using hull_inc [OF y] by auto
  then obtain d where "0 < d" and df: "(x + d *R (y-x)) ∈ rel_frontier S"
                  and di: "⋀e. ⟦0 ≤ e; e < d⟧ ⟹ (x + e *R (y-x)) ∈ rel_interior S"
    by (rule ray_to_rel_frontier [OF ‹bounded S› x]) (use xy in auto)
  show ?thesis
  proof
    show "x + d *R (y - x) ∈ rel_frontier S"
      by (simp add: df)
  next
    have "open_segment x y ⊆ rel_interior S"
      using rel_interior_closure_convex_segment [OF ‹convex S› x] closure_subset y by blast
    moreover have "x + d *R (y - x) ∈ open_segment x y" if "d < 1"
      using xy
      apply (auto simp: in_segment)
      apply (rule_tac x="d" in exI)
      using ‹0 < d› that apply (auto simp: divide_simps algebra_simps)
      done
    ultimately have "1 ≤ d"
      using df rel_frontier_def by fastforce
    moreover have "x = (1 / d) *R x + ((d - 1) / d) *R x"
      by (metis ‹0 < d› add.commute add_divide_distrib diff_add_cancel divide_self_if less_irrefl scaleR_add_left scaleR_one)
    ultimately show "y ∈ closed_segment x (x + d *R (y - x))"
      apply (auto simp: in_segment)
      apply (rule_tac x="1/d" in exI)
      apply (auto simp: divide_simps algebra_simps)
      done
  next
    show "open_segment x (x + d *R (y - x)) ⊆ rel_interior S"
      apply (rule rel_interior_closure_convex_segment [OF ‹convex S› x])
      using df rel_frontier_def by auto
  qed
qed

lemma segment_to_rel_frontier:
  fixes x :: "'a::euclidean_space"
  assumes S: "convex S" "bounded S" and x: "x ∈ rel_interior S"
      and y: "y ∈ S" and xy: "~(x = y ∧ S = {x})"
  obtains z where "z ∈ rel_frontier S" "y ∈ closed_segment x z"
                  "open_segment x z ⊆ rel_interior S"
proof (cases "x=y")
  case True
  with xy have "S ≠ {x}"
    by blast
  with True show ?thesis
    by (metis Set.set_insert all_not_in_conv ends_in_segment(1) insert_iff segment_to_rel_frontier_aux[OF S x] that y)
next
  case False
  then show ?thesis
    using segment_to_rel_frontier_aux [OF S x y] that by blast
qed

proposition rel_frontier_not_sing:
  fixes a :: "'a::euclidean_space"
  assumes "bounded S"
    shows "rel_frontier S ≠ {a}"
proof (cases "S = {}")
  case True  then show ?thesis  by simp
next
  case False
  then obtain z where "z ∈ S"
    by blast
  then show ?thesis
  proof (cases "S = {z}")
    case True then show ?thesis  by simp
  next
    case False
    then obtain w where "w ∈ S" "w ≠ z"
      using ‹z ∈ S› by blast
    show ?thesis
    proof
      assume "rel_frontier S = {a}"
      then consider "w ∉ rel_frontier S" | "z ∉ rel_frontier S"
        using ‹w ≠ z› by auto
      then show False
      proof cases
        case 1
        then have w: "w ∈ rel_interior S"
          using ‹w ∈ S› closure_subset rel_frontier_def by fastforce
        have "w + (w - z) ∈ affine hull S"
          by (metis ‹w ∈ S› ‹z ∈ S› affine_affine_hull hull_inc mem_affine_3_minus scaleR_one)
        then obtain e where "0 < e" "(w + e *R (w - z)) ∈ rel_frontier S"
          using ‹w ≠ z›  ‹z ∈ S› by (metis assms ray_to_rel_frontier right_minus_eq w)
        moreover obtain d where "0 < d" "(w + d *R (z - w)) ∈ rel_frontier S"
          using ray_to_rel_frontier [OF ‹bounded S› w, of "1 *R (z - w)"]  ‹w ≠ z›  ‹z ∈ S›
          by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one)
        ultimately have "d *R (z - w) = e *R (w - z)"
          using ‹rel_frontier S = {a}› by force
        moreover have "e ≠ -d "
          using ‹0 < e› ‹0 < d› by force
        ultimately show False
          by (metis (no_types, lifting) ‹w ≠ z› eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus)
      next
        case 2
        then have z: "z ∈ rel_interior S"
          using ‹z ∈ S› closure_subset rel_frontier_def by fastforce
        have "z + (z - w) ∈ affine hull S"
          by (metis ‹z ∈ S› ‹w ∈ S› affine_affine_hull hull_inc mem_affine_3_minus scaleR_one)
        then obtain e where "0 < e" "(z + e *R (z - w)) ∈ rel_frontier S"
          using ‹w ≠ z›  ‹w ∈ S› by (metis assms ray_to_rel_frontier right_minus_eq z)
        moreover obtain d where "0 < d" "(z + d *R (w - z)) ∈ rel_frontier S"
          using ray_to_rel_frontier [OF ‹bounded S› z, of "1 *R (w - z)"]  ‹w ≠ z›  ‹w ∈ S›
          by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one)
        ultimately have "d *R (w - z) = e *R (z - w)"
          using ‹rel_frontier S = {a}› by force
        moreover have "e ≠ -d "
          using ‹0 < e› ‹0 < d› by force
        ultimately show False
          by (metis (no_types, lifting) ‹w ≠ z› eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus)
      qed
    qed
  qed
qed

proposition
  fixes S :: "'a::euclidean_space set"
  assumes "compact S" and 0: "0 ∈ rel_interior S"
      and star: "⋀x. x ∈ S ⟹ open_segment 0 x ⊆ rel_interior S"
    shows starlike_compact_projective1_0:
            "S - rel_interior S homeomorphic sphere 0 1 ∩ affine hull S"
            (is "?SMINUS homeomorphic ?SPHER")
      and starlike_compact_projective2_0:
            "S homeomorphic cball 0 1 ∩ affine hull S"
            (is "S homeomorphic ?CBALL")
proof -
  have starI: "(u *R x) ∈ rel_interior S" if "x ∈ S" "0 ≤ u" "u < 1" for x u
  proof (cases "x=0 ∨ u=0")
    case True with 0 show ?thesis by force
  next
    case False with that show ?thesis
      by (auto simp: in_segment intro: star [THEN subsetD])
  qed
  have "0 ∈ S"  using assms rel_interior_subset by auto
  define proj where "proj ≡ λx::'a. x /R norm x"
  have eqI: "x = y" if "proj x = proj y" "norm x = norm y" for x y
    using that  by (force simp: proj_def)
  then have iff_eq: "⋀x y. (proj x = proj y ∧ norm x = norm y) ⟷ x = y"
    by blast
  have projI: "x ∈ affine hull S ⟹ proj x ∈ affine hull S" for x
    by (metis ‹0 ∈ S› affine_hull_span_0 hull_inc span_mul proj_def)
  have nproj1 [simp]: "x ≠ 0 ⟹ norm(proj x) = 1" for x
    by (simp add: proj_def)
  have proj0_iff [simp]: "proj x = 0 ⟷ x = 0" for x
    by (simp add: proj_def)
  have cont_proj: "continuous_on (UNIV - {0}) proj"
    unfolding proj_def by (rule continuous_intros | force)+
  have proj_spherI: "⋀x. ⟦x ∈ affine hull S; x ≠ 0⟧ ⟹ proj x ∈ ?SPHER"
    by (simp add: projI)
  have "bounded S" "closed S"
    using ‹compact S› compact_eq_bounded_closed by blast+
  have inj_on_proj: "inj_on proj (S - rel_interior S)"
  proof
    fix x y
    assume x: "x ∈ S - rel_interior S"
       and y: "y ∈ S - rel_interior S" and eq: "proj x = proj y"
    then have xynot: "x ≠ 0" "y ≠ 0" "x ∈ S" "y ∈ S" "x ∉ rel_interior S" "y ∉ rel_interior S"
      using 0 by auto
    consider "norm x = norm y" | "norm x < norm y" | "norm x > norm y" by linarith
    then show "x = y"
    proof cases
      assume "norm x = norm y"
        with iff_eq eq show "x = y" by blast
    next
      assume *: "norm x < norm y"
      have "x /R norm x = norm x *R (x /R norm x) /R norm (norm x *R (x /R norm x))"
        by force
      then have "proj ((norm x / norm y) *R y) = proj x"
        by (metis (no_types) divide_inverse local.proj_def eq scaleR_scaleR)
      then have [simp]: "(norm x / norm y) *R y = x"
        by (rule eqI) (simp add: ‹y ≠ 0›)
      have no: "0 ≤ norm x / norm y" "norm x / norm y < 1"
        using * by (auto simp: divide_simps)
      then show "x = y"
        using starI [OF ‹y ∈ S› no] xynot by auto
    next
      assume *: "norm x > norm y"
      have "y /R norm y = norm y *R (y /R norm y) /R norm (norm y *R (y /R norm y))"
        by force
      then have "proj ((norm y / norm x) *R x) = proj y"
        by (metis (no_types) divide_inverse local.proj_def eq scaleR_scaleR)
      then have [simp]: "(norm y / norm x) *R x = y"
        by (rule eqI) (simp add: ‹x ≠ 0›)
      have no: "0 ≤ norm y / norm x" "norm y / norm x < 1"
        using * by (auto simp: divide_simps)
      then show "x = y"
        using starI [OF ‹x ∈ S› no] xynot by auto
    qed
  qed
  have "∃surf. homeomorphism (S - rel_interior S) ?SPHER proj surf"
  proof (rule homeomorphism_compact)
    show "compact (S - rel_interior S)"
       using ‹compact S› compact_rel_boundary by blast
    show "continuous_on (S - rel_interior S) proj"
      using 0 by (blast intro: continuous_on_subset [OF cont_proj])
    show "proj ` (S - rel_interior S) = ?SPHER"
    proof
      show "proj ` (S - rel_interior S) ⊆ ?SPHER"
        using 0 by (force simp: hull_inc projI intro: nproj1)
      show "?SPHER ⊆ proj ` (S - rel_interior S)"
      proof (clarsimp simp: proj_def)
        fix x
        assume "x ∈ affine hull S" and nox: "norm x = 1"
        then have "x ≠ 0" by auto
        obtain d where "0 < d" and dx: "(d *R x) ∈ rel_frontier S"
                   and ri: "⋀e. ⟦0 ≤ e; e < d⟧ ⟹ (e *R x) ∈ rel_interior S"
          using ray_to_rel_frontier [OF ‹bounded S› 0] ‹x ∈ affine hull S› ‹x ≠ 0› by auto
        show "x ∈ (λx. x /R norm x) ` (S - rel_interior S)"
          apply (rule_tac x="d *R x" in image_eqI)
          using ‹0 < d›
          using dx ‹closed S› apply (auto simp: rel_frontier_def divide_simps nox)
          done
      qed
    qed
  qed (rule inj_on_proj)
  then obtain surf where surf: "homeomorphism (S - rel_interior S) ?SPHER proj surf"
    by blast
  then have cont_surf: "continuous_on (proj ` (S - rel_interior S)) surf"
    by (auto simp: homeomorphism_def)
  have surf_nz: "⋀x. x ∈ ?SPHER ⟹ surf x ≠ 0"
    by (metis "0" DiffE homeomorphism_def imageI surf)
  have cont_nosp: "continuous_on (?SPHER) (λx. norm x *R ((surf o proj) x))"
    apply (rule continuous_intros)+
    apply (rule continuous_on_subset [OF cont_proj], force)
    apply (rule continuous_on_subset [OF cont_surf])
    apply (force simp: homeomorphism_image1 [OF surf] dest: proj_spherI)
    done
  have surfpS: "⋀x. ⟦norm x = 1; x ∈ affine hull S⟧ ⟹ surf (proj x) ∈ S"
    by (metis (full_types) DiffE ‹0 ∈ S› homeomorphism_def image_eqI norm_zero proj_spherI real_vector.scale_zero_left scaleR_one surf)
  have *: "∃y. norm y = 1 ∧ y ∈ affine hull S ∧ x = surf (proj y)"
          if "x ∈ S" "x ∉ rel_interior S" for x
  proof -
    have "proj x ∈ ?SPHER"
      by (metis (full_types) "0" hull_inc proj_spherI that)
    moreover have "surf (proj x) = x"
      by (metis Diff_iff homeomorphism_def surf that)
    ultimately show ?thesis
      by (metis ‹⋀x. x ∈ ?SPHER ⟹ surf x ≠ 0› hull_inc inverse_1 local.proj_def norm_sgn projI scaleR_one sgn_div_norm that(1))
  qed
  have surfp_notin: "⋀x. ⟦norm x = 1; x ∈ affine hull S⟧ ⟹ surf (proj x) ∉ rel_interior S"
    by (metis (full_types) DiffE one_neq_zero homeomorphism_def image_eqI norm_zero proj_spherI surf)
  have no_sp_im: "(λx. norm x *R surf (proj x)) ` (?SPHER) = S - rel_interior S"
    by (auto simp: surfpS image_def Bex_def surfp_notin *)
  have inj_spher: "inj_on (λx. norm x *R surf (proj x)) ?SPHER"
  proof
    fix x y
    assume xy: "x ∈ ?SPHER" "y ∈ ?SPHER"
       and eq: " norm x *R surf (proj x) = norm y *R surf (proj y)"
    then have "norm x = 1" "norm y = 1" "x ∈ affine hull S" "y ∈ affine hull S"
      using 0 by auto
    with eq show "x = y"
      by (simp add: proj_def) (metis surf xy homeomorphism_def)
  qed
  have co01: "compact ?SPHER"
    by (simp add: closed_affine_hull compact_Int_closed)
  show "?SMINUS homeomorphic ?SPHER"
    apply (subst homeomorphic_sym)
    apply (rule homeomorphic_compact [OF co01 cont_nosp [unfolded o_def] no_sp_im inj_spher])
    done
  have proj_scaleR: "⋀a x. 0 < a ⟹ proj (a *R x) = proj x"
    by (simp add: proj_def)
  have cont_sp0: "continuous_on (affine hull S - {0}) (surf o proj)"
    apply (rule continuous_on_compose [OF continuous_on_subset [OF cont_proj]], force)
    apply (rule continuous_on_subset [OF cont_surf])
    using homeomorphism_image1 proj_spherI surf by fastforce
  obtain B where "B>0" and B: "⋀x. x ∈ S ⟹ norm x ≤ B"
    by (metis compact_imp_bounded ‹compact S› bounded_pos_less less_eq_real_def)
  have cont_nosp: "continuous (at x within ?CBALL) (λx. norm x *R surf (proj x))"
         if "norm x ≤ 1" "x ∈ affine hull S" for x
  proof (cases "x=0")
    case True
    show ?thesis using True
      apply (simp add: continuous_within)
      apply (rule lim_null_scaleR_bounded [where B=B])
      apply (simp_all add: tendsto_norm_zero eventually_at)
      apply (rule_tac x=B in exI)
      using B surfpS proj_def projI apply (auto simp: ‹B > 0›)
      done
  next
    case False
    then have "∀F x in at x. (x ∈ affine hull S - {0}) = (x ∈ affine hull S)"
      apply (simp add: eventually_at)
      apply (rule_tac x="norm x" in exI)
      apply (auto simp: False)
      done
    with cont_sp0 have *: "continuous (at x within affine hull S) (λx. surf (proj x))"
      apply (simp add: continuous_on_eq_continuous_within)
      apply (drule_tac x=x in bspec, force simp: False that)
      apply (simp add: continuous_within Lim_transform_within_set)
      done
    show ?thesis
      apply (rule continuous_within_subset [where s = "affine hull S", OF _ Int_lower2])
      apply (rule continuous_intros *)+
      done
  qed
  have cont_nosp2: "continuous_on ?CBALL (λx. norm x *R ((surf o proj) x))"
    by (simp add: continuous_on_eq_continuous_within cont_nosp)
  have "norm y *R surf (proj y) ∈ S"  if "y ∈ cball 0 1" and yaff: "y ∈ affine hull S" for y
  proof (cases "y=0")
    case True then show ?thesis
      by (simp add: ‹0 ∈ S›)
  next
    case False
    then have "norm y *R surf (proj y) = norm y *R surf (proj (y /R norm y))"
      by (simp add: proj_def)
    have "norm y ≤ 1" using that by simp
    have "surf (proj (y /R norm y)) ∈ S"
      apply (rule surfpS)
      using proj_def projI yaff
      by (auto simp: False)
    then have "surf (proj y) ∈ S"
      by (simp add: False proj_def)
    then show "norm y *R surf (proj y) ∈ S"
      by (metis dual_order.antisym le_less_linear norm_ge_zero rel_interior_subset scaleR_one
                starI subset_eq ‹norm y ≤ 1›)
  qed
  moreover have "x ∈ (λx. norm x *R surf (proj x)) ` (?CBALL)" if "x ∈ S" for x
  proof (cases "x=0")
    case True with that hull_inc  show ?thesis by fastforce
  next
    case False
    then have psp: "proj (surf (proj x)) = proj x"
      by (metis homeomorphism_def hull_inc proj_spherI surf that)
    have nxx: "norm x *R proj x = x"
      by (simp add: False local.proj_def)
    have affineI: "(1 / norm (surf (proj x))) *R x ∈ affine hull S"
      by (metis ‹0 ∈ S› affine_hull_span_0 hull_inc span_clauses(4) that)
    have sproj_nz: "surf (proj x) ≠ 0"
      by (metis False proj0_iff psp)
    then have "proj x = proj (proj x)"
      by (metis False nxx proj_scaleR zero_less_norm_iff)
    moreover have scaleproj: "⋀a r. r *R proj a = (r / norm a) *R a"
      by (simp add: divide_inverse local.proj_def)
    ultimately have "(norm (surf (proj x)) / norm x) *R x ∉ rel_interior S"
      by (metis (no_types) sproj_nz divide_self_if hull_inc norm_eq_zero nproj1 projI psp scaleR_one surfp_notin that)
    then have "(norm (surf (proj x)) / norm x) ≥ 1"
      using starI [OF that] by (meson starI [OF that] le_less_linear norm_ge_zero zero_le_divide_iff)
    then have nole: "norm x ≤ norm (surf (proj x))"
      by (simp add: le_divide_eq_1)
    show ?thesis
      apply (rule_tac x="inverse(norm(surf (proj x))) *R x" in image_eqI)
      apply (metis (no_types, hide_lams) mult.commute scaleproj abs_inverse abs_norm_cancel divide_inverse norm_scaleR nxx positive_imp_inverse_positive proj_scaleR psp sproj_nz zero_less_norm_iff)
      apply (auto simp: divide_simps nole affineI)
      done
  qed
  ultimately have im_cball: "(λx. norm x *R surf (proj x)) ` ?CBALL = S"
    by blast
  have inj_cball: "inj_on (λx. norm x *R surf (proj x)) ?CBALL"
  proof
    fix x y
    assume "x ∈ ?CBALL" "y ∈ ?CBALL"
       and eq: "norm x *R surf (proj x) = norm y *R surf (proj y)"
    then have x: "x ∈ affine hull S" and y: "y ∈ affine hull S"
      using 0 by auto
    show "x = y"
    proof (cases "x=0 ∨ y=0")
      case True then show "x = y" using eq proj_spherI surf_nz x y by force
    next
      case False
      with x y have speq: "surf (proj x) = surf (proj y)"
        by (metis eq homeomorphism_apply2 proj_scaleR proj_spherI surf zero_less_norm_iff)
      then have "norm x = norm y"
        by (metis ‹x ∈ affine hull S› ‹y ∈ affine hull S› eq proj_spherI real_vector.scale_cancel_right surf_nz)
      moreover have "proj x = proj y"
        by (metis (no_types) False speq homeomorphism_apply2 proj_spherI surf x y)
      ultimately show "x = y"
        using eq eqI by blast
    qed
  qed
  have co01: "compact ?CBALL"
    by (simp add: closed_affine_hull compact_Int_closed)
  show "S homeomorphic ?CBALL"
    apply (subst homeomorphic_sym)
    apply (rule homeomorphic_compact [OF co01 cont_nosp2 [unfolded o_def] im_cball inj_cball])
    done
qed

corollary
  fixes S :: "'a::euclidean_space set"
  assumes "compact S" and a: "a ∈ rel_interior S"
      and star: "⋀x. x ∈ S ⟹ open_segment a x ⊆ rel_interior S"
    shows starlike_compact_projective1:
            "S - rel_interior S homeomorphic sphere a 1 ∩ affine hull S"
      and starlike_compact_projective2:
            "S homeomorphic cball a 1 ∩ affine hull S"
proof -
  have 1: "compact (op+ (-a) ` S)" by (meson assms compact_translation)
  have 2: "0 ∈ rel_interior (op+ (-a) ` S)"
    by (simp add: a rel_interior_translation)
  have 3: "open_segment 0 x ⊆ rel_interior (op+ (-a) ` S)" if "x ∈ (op+ (-a) ` S)" for x
  proof -
    have "x+a ∈ S" using that by auto
    then have "open_segment a (x+a) ⊆ rel_interior S" by (metis star)
    then show ?thesis using open_segment_translation
      using rel_interior_translation by fastforce
  qed
  have "S - rel_interior S homeomorphic (op+ (-a) ` S) - rel_interior (op+ (-a) ` S)"
    by (metis rel_interior_translation translation_diff homeomorphic_translation)
  also have "... homeomorphic sphere 0 1 ∩ affine hull (op+ (-a) ` S)"
    by (rule starlike_compact_projective1_0 [OF 1 2 3])
  also have "... = op+ (-a) ` (sphere a 1 ∩ affine hull S)"
    by (metis affine_hull_translation left_minus sphere_translation translation_Int)
  also have "... homeomorphic sphere a 1 ∩ affine hull S"
    using homeomorphic_translation homeomorphic_sym by blast
  finally show "S - rel_interior S homeomorphic sphere a 1 ∩ affine hull S" .

  have "S homeomorphic (op+ (-a) ` S)"
    by (metis homeomorphic_translation)
  also have "... homeomorphic cball 0 1 ∩ affine hull (op+ (-a) ` S)"
    by (rule starlike_compact_projective2_0 [OF 1 2 3])
  also have "... = op+ (-a) ` (cball a 1 ∩ affine hull S)"
    by (metis affine_hull_translation left_minus cball_translation translation_Int)
  also have "... homeomorphic cball a 1 ∩ affine hull S"
    using homeomorphic_translation homeomorphic_sym by blast
  finally show "S homeomorphic cball a 1 ∩ affine hull S" .
qed

corollary starlike_compact_projective_special:
  assumes "compact S"
    and cb01: "cball (0::'a::euclidean_space) 1 ⊆ S"
    and scale: "⋀x u. ⟦x ∈ S; 0 ≤ u; u < 1⟧ ⟹ u *R x ∈ S - frontier S"
  shows "S homeomorphic (cball (0::'a::euclidean_space) 1)"
proof -
  have "ball 0 1 ⊆ interior S"
    using cb01 interior_cball interior_mono by blast
  then have 0: "0 ∈ rel_interior S"
    by (meson centre_in_ball subsetD interior_subset_rel_interior le_numeral_extra(2) not_le)
  have [simp]: "affine hull S = UNIV"
    using ‹ball 0 1 ⊆ interior S› by (auto intro!: affine_hull_nonempty_interior)
  have star: "open_segment 0 x ⊆ rel_interior S" if "x ∈ S" for x
  proof
    fix p assume "p ∈ open_segment 0 x"
    then obtain u where "x ≠ 0" and u: "0 ≤ u" "u < 1" and p: "u *R x = p"
      by (auto simp: in_segment)
    then show "p ∈ rel_interior S"
      using scale [OF that u] closure_subset frontier_def interior_subset_rel_interior by fastforce
  qed
  show ?thesis
    using starlike_compact_projective2_0 [OF ‹compact S› 0 star] by simp
qed

lemma homeomorphic_convex_lemma:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "convex S" "compact S" "convex T" "compact T"
      and affeq: "aff_dim S = aff_dim T"
    shows "(S - rel_interior S) homeomorphic (T - rel_interior T) ∧
           S homeomorphic T"
proof (cases "rel_interior S = {} ∨ rel_interior T = {}")
  case True
    then show ?thesis
      by (metis Diff_empty affeq ‹convex S› ‹convex T› aff_dim_empty homeomorphic_empty rel_interior_eq_empty aff_dim_empty)
next
  case False
  then obtain a b where a: "a ∈ rel_interior S" and b: "b ∈ rel_interior T" by auto
  have starS: "⋀x. x ∈ S ⟹ open_segment a x ⊆ rel_interior S"
    using rel_interior_closure_convex_segment
          a ‹convex S› closure_subset subsetCE by blast
  have starT: "⋀x. x ∈ T ⟹ open_segment b x ⊆ rel_interior T"
    using rel_interior_closure_convex_segment
          b ‹convex T› closure_subset subsetCE by blast
  let ?aS = "op+ (-a) ` S" and ?bT = "op+ (-b) ` T"
  have 0: "0 ∈ affine hull ?aS" "0 ∈ affine hull ?bT"
    by (metis a b subsetD hull_inc image_eqI left_minus rel_interior_subset)+
  have subs: "subspace (span ?aS)" "subspace (span ?bT)"
    by (rule subspace_span)+
  moreover
  have "dim (span (op + (- a) ` S)) = dim (span (op + (- b) ` T))"
    by (metis 0 aff_dim_translation_eq aff_dim_zero affeq dim_span nat_int)
  ultimately obtain f g where "linear f" "linear g"
                and fim: "f ` span ?aS = span ?bT"
                and gim: "g ` span ?bT = span ?aS"
                and fno: "⋀x. x ∈ span ?aS ⟹ norm(f x) = norm x"
                and gno: "⋀x. x ∈ span ?bT ⟹ norm(g x) = norm x"
                and gf: "⋀x. x ∈ span ?aS ⟹ g(f x) = x"
                and fg: "⋀x. x ∈ span ?bT ⟹ f(g x) = x"
    by (rule isometries_subspaces) blast
  have [simp]: "continuous_on A f" for A
    using ‹linear f› linear_conv_bounded_linear linear_continuous_on by blast
  have [simp]: "continuous_on B g" for B
    using ‹linear g› linear_conv_bounded_linear linear_continuous_on by blast
  have eqspanS: "affine hull ?aS = span ?aS"
    by (metis a affine_hull_span_0 subsetD hull_inc image_eqI left_minus rel_interior_subset)
  have eqspanT: "affine hull ?bT = span ?bT"
    by (metis b affine_hull_span_0 subsetD hull_inc image_eqI left_minus rel_interior_subset)
  have "S homeomorphic cball a 1 ∩ affine hull S"
    by (rule starlike_compact_projective2 [OF ‹compact S› a starS])
  also have "... homeomorphic op+ (-a) ` (cball a 1 ∩ affine hull S)"
    by (metis homeomorphic_translation)
  also have "... = cball 0 1 ∩ op+ (-a) ` (affine hull S)"
    by (auto simp: dist_norm)
  also have "... = cball 0 1 ∩ span ?aS"
    using eqspanS affine_hull_translation by blast
  also have "... homeomorphic cball 0 1 ∩ span ?bT"
    proof (rule homeomorphicI [where f=f and g=g])
      show fim1: "f ` (cball 0 1 ∩ span ?aS) = cball 0 1 ∩ span ?bT"
        apply (rule subset_antisym)
         using fim fno apply (force simp:, clarify)
        by (metis IntI fg gim gno image_eqI mem_cball_0)
      show "g ` (cball 0 1 ∩ span ?bT) = cball 0 1 ∩ span ?aS"
        apply (rule subset_antisym)
         using gim gno apply (force simp:, clarify)
        by (metis IntI fim1 gf image_eqI)
    qed (auto simp: fg gf)
  also have "... = cball 0 1 ∩ op+ (-b) ` (affine hull T)"
    using eqspanT affine_hull_translation by blast
  also have "... = op+ (-b) ` (cball b 1 ∩ affine hull T)"
    by (auto simp: dist_norm)
  also have "... homeomorphic (cball b 1 ∩ affine hull T)"
    by (metis homeomorphic_translation homeomorphic_sym)
  also have "... homeomorphic T"
    by (metis starlike_compact_projective2 [OF ‹compact T› b starT] homeomorphic_sym)
  finally have 1: "S homeomorphic T" .

  have "S - rel_interior S homeomorphic sphere a 1 ∩ affine hull S"
    by (rule starlike_compact_projective1 [OF ‹compact S› a starS])
  also have "... homeomorphic op+ (-a) ` (sphere a 1 ∩ affine hull S)"
    by (metis homeomorphic_translation)
  also have "... = sphere 0 1 ∩ op+ (-a) ` (affine hull S)"
    by (auto simp: dist_norm)
  also have "... = sphere 0 1 ∩ span ?aS"
    using eqspanS affine_hull_translation by blast
  also have "... homeomorphic sphere 0 1 ∩ span ?bT"
    proof (rule homeomorphicI [where f=f and g=g])
      show fim1: "f ` (sphere 0 1 ∩ span ?aS) = sphere 0 1 ∩ span ?bT"
        apply (rule subset_antisym)
        using fim fno apply (force simp:, clarify)
        by (metis IntI fg gim gno image_eqI mem_sphere_0)
      show "g ` (sphere 0 1 ∩ span ?bT) = sphere 0 1 ∩ span ?aS"
        apply (rule subset_antisym)
        using gim gno apply (force simp:, clarify)
        by (metis IntI fim1 gf image_eqI)
    qed (auto simp: fg gf)
  also have "... = sphere 0 1 ∩ op+ (-b) ` (affine hull T)"
    using eqspanT affine_hull_translation by blast
  also have "... = op+ (-b) ` (sphere b 1 ∩ affine hull T)"
    by (auto simp: dist_norm)
  also have "... homeomorphic (sphere b 1 ∩ affine hull T)"
    by (metis homeomorphic_translation homeomorphic_sym)
  also have "... homeomorphic T - rel_interior T"
    by (metis starlike_compact_projective1 [OF ‹compact T› b starT] homeomorphic_sym)
  finally have 2: "S - rel_interior S homeomorphic T - rel_interior T" .
  show ?thesis
    using 1 2 by blast
qed

lemma homeomorphic_convex_compact_sets:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "convex S" "compact S" "convex T" "compact T"
      and affeq: "aff_dim S = aff_dim T"
    shows "S homeomorphic T"
using homeomorphic_convex_lemma [OF assms] assms
by (auto simp: rel_frontier_def)

lemma homeomorphic_rel_frontiers_convex_bounded_sets:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "convex S" "bounded S" "convex T" "bounded T"
      and affeq: "aff_dim S = aff_dim T"
    shows  "rel_frontier S homeomorphic rel_frontier T"
using assms homeomorphic_convex_lemma [of "closure S" "closure T"]
by (simp add: rel_frontier_def convex_rel_interior_closure)


subsection‹Homeomorphisms between punctured spheres and affine sets›
text‹Including the famous stereoscopic projection of the 3-D sphere to the complex plane›

text‹The special case with centre 0 and radius 1›
lemma homeomorphic_punctured_affine_sphere_affine_01:
  assumes "b ∈ sphere 0 1" "affine T" "0 ∈ T" "b ∈ T" "affine p"
      and affT: "aff_dim T = aff_dim p + 1"
    shows "(sphere 0 1 ∩ T) - {b} homeomorphic p"
proof -
  have [simp]: "norm b = 1" "b∙b = 1"
    using assms by (auto simp: norm_eq_1)
  have [simp]: "T ∩ {v. b∙v = 0} ≠ {}"
    using ‹0 ∈ T› by auto
  have [simp]: "¬ T ⊆ {v. b∙v = 0}"
    using ‹norm b = 1› ‹b ∈ T› by auto
  define f where "f ≡ λx. 2 *R b + (2 / (1 - b∙x)) *R (x - b)"
  define g where "g ≡ λy. b + (4 / (norm y ^ 2 + 4)) *R (y - 2 *R b)"
  have [simp]: "⋀x. ⟦x ∈ T; b∙x = 0⟧ ⟹ f (g x) = x"
    unfolding f_def g_def by (simp add: algebra_simps divide_simps add_nonneg_eq_0_iff)
  have no: "⋀x. ⟦norm x = 1; b∙x ≠ 1⟧ ⟹ (norm (f x))2 = 4 * (1 + b∙x) / (1 - b∙x)"
    apply (simp add: dot_square_norm [symmetric])
    apply (simp add: f_def vector_add_divide_simps divide_simps norm_eq_1)
    apply (simp add: algebra_simps inner_commute)
    done
  have [simp]: "⋀u::real. 8 + u * (u * 8) = u * 16 ⟷ u=1"
    by algebra
  have [simp]: "⋀x. ⟦norm x = 1; b ∙ x ≠ 1⟧ ⟹ g (f x) = x"
    unfolding g_def no by (auto simp: f_def divide_simps)
  have [simp]: "⋀x. ⟦x ∈ T; b ∙ x = 0⟧ ⟹ norm (g x) = 1"
    unfolding g_def
    apply (rule power2_eq_imp_eq)
    apply (simp_all add: dot_square_norm [symmetric] divide_simps vector_add_divide_simps)
    apply (simp add: algebra_simps inner_commute)
    done
  have [simp]: "⋀x. ⟦x ∈ T; b ∙ x = 0⟧ ⟹ b ∙ g x ≠ 1"
    unfolding g_def
    apply (simp_all add: dot_square_norm [symmetric] divide_simps vector_add_divide_simps add_nonneg_eq_0_iff)
    apply (auto simp: algebra_simps)
    done
  have "subspace T"
    by (simp add: assms subspace_affine)
  have [simp]: "⋀x. ⟦x ∈ T; b ∙ x = 0⟧ ⟹ g x ∈ T"
    unfolding g_def
    by (blast intro: ‹subspace T› ‹b ∈ T› subspace_add subspace_mul subspace_diff)
  have "f ` {x. norm x = 1 ∧ b∙x ≠ 1} ⊆ {x. b∙x = 0}"
    unfolding f_def using ‹norm b = 1› norm_eq_1
    by (force simp: field_simps inner_add_right inner_diff_right)
  moreover have "f ` T ⊆ T"
    unfolding f_def using assms
    apply (auto simp: field_simps inner_add_right inner_diff_right)
    by (metis add_0 diff_zero mem_affine_3_minus)
  moreover have "{x. b∙x = 0} ∩ T ⊆ f ` ({x. norm x = 1 ∧ b∙x ≠ 1} ∩ T)"
    apply clarify
    apply (rule_tac x = "g x" in image_eqI, auto)
    done
  ultimately have imf: "f ` ({x. norm x = 1 ∧ b∙x ≠ 1} ∩ T) = {x. b∙x = 0} ∩ T"
    by blast
  have no4: "⋀y. b∙y = 0 ⟹ norm ((y∙y + 4) *R b + 4 *R (y - 2 *R b)) = y∙y + 4"
    apply (rule power2_eq_imp_eq)
    apply (simp_all add: dot_square_norm [symmetric])
    apply (auto simp: power2_eq_square algebra_simps inner_commute)
    done
  have [simp]: "⋀x. ⟦norm x = 1; b ∙ x ≠ 1⟧ ⟹ b ∙ f x = 0"
    by (simp add: f_def algebra_simps divide_simps)
  have [simp]: "⋀x. ⟦x ∈ T; norm x = 1; b ∙ x ≠ 1⟧ ⟹ f x ∈ T"
    unfolding f_def
    by (blast intro: ‹subspace T› ‹b ∈ T› subspace_add subspace_mul subspace_diff)
  have "g ` {x. b∙x = 0} ⊆ {x. norm x = 1 ∧ b∙x ≠ 1}"
    unfolding g_def
    apply (clarsimp simp: no4 vector_add_divide_simps divide_simps add_nonneg_eq_0_iff dot_square_norm [symmetric])
    apply (auto simp: algebra_simps)
    done
  moreover have "g ` T ⊆ T"
    unfolding g_def
    by (blast intro: ‹subspace T› ‹b ∈ T› subspace_add subspace_mul subspace_diff)
  moreover have "{x. norm x = 1 ∧ b∙x ≠ 1} ∩ T ⊆ g ` ({x. b∙x = 0} ∩ T)"
    apply clarify
    apply (rule_tac x = "f x" in image_eqI, auto)
    done
  ultimately have img: "g ` ({x. b∙x = 0} ∩ T) = {x. norm x = 1 ∧ b∙x ≠ 1} ∩ T"
    by blast
  have aff: "affine ({x. b∙x = 0} ∩ T)"
    by (blast intro: affine_hyperplane assms)
  have contf: "continuous_on ({x. norm x = 1 ∧ b∙x ≠ 1} ∩ T) f"
    unfolding f_def by (rule continuous_intros | force)+
  have contg: "continuous_on ({x. b∙x = 0} ∩ T) g"
    unfolding g_def by (rule continuous_intros | force simp: add_nonneg_eq_0_iff)+
  have "(sphere 0 1 ∩ T) - {b} = {x. norm x = 1 ∧ (b∙x ≠ 1)} ∩ T"
    using  ‹norm b = 1› by (auto simp: norm_eq_1) (metis vector_eq  ‹b∙b = 1›)
  also have "... homeomorphic {x. b∙x = 0} ∩ T"
    by (rule homeomorphicI [OF imf img contf contg]) auto
  also have "... homeomorphic p"
    apply (rule homeomorphic_affine_sets [OF aff ‹affine p›])
    apply (simp add: Int_commute aff_dim_affine_Int_hyperplane [OF ‹affine T›] affT)
    done
  finally show ?thesis .
qed

theorem homeomorphic_punctured_affine_sphere_affine:
  fixes a :: "'a :: euclidean_space"
  assumes "0 < r" "b ∈ sphere a r" "affine T" "a ∈ T" "b ∈ T" "affine p"
      and aff: "aff_dim T = aff_dim p + 1"
    shows "((sphere a r ∩ T) - {b}) homeomorphic p"
proof -
  have "a ≠ b" using assms by auto
  then have inj: "inj (λx::'a. x /R norm (a - b))"
    by (simp add: inj_on_def)
  have "((sphere a r ∩ T) - {b}) homeomorphic
        op+ (-a) ` ((sphere a r ∩ T) - {b})"
    by (rule homeomorphic_translation)
  also have "... homeomorphic op *R (inverse r) ` op + (- a) ` (sphere a r ∩ T - {b})"
    by (metis ‹0 < r› homeomorphic_scaling inverse_inverse_eq inverse_zero less_irrefl)
  also have "... = sphere 0 1 ∩ (op *R (inverse r) ` op + (- a) ` T) - {(b - a) /R r}"
    using assms by (auto simp: dist_norm norm_minus_commute divide_simps)
  also have "... homeomorphic p"
    apply (rule homeomorphic_punctured_affine_sphere_affine_01)
    using assms
    apply (auto simp: dist_norm norm_minus_commute affine_scaling affine_translation [symmetric] aff_dim_translation_eq inj)
    done
  finally show ?thesis .
qed

proposition homeomorphic_punctured_sphere_affine_gen:
  fixes a :: "'a :: euclidean_space"
  assumes "convex S" "bounded S" and a: "a ∈ rel_frontier S"
      and "affine T" and affS: "aff_dim S = aff_dim T + 1"
    shows "rel_frontier S - {a} homeomorphic T"
proof -
  have "S ≠ {}" using assms by auto
  obtain U :: "'a set" where "affine U" and affdS: "aff_dim U = aff_dim S"
    using choose_affine_subset [OF affine_UNIV aff_dim_geq]
    by (meson aff_dim_affine_hull affine_affine_hull)
  have "convex U"
    by (simp add: affine_imp_convex ‹affine U›)
  have "U ≠ {}"
    by (metis ‹S ≠ {}› ‹aff_dim U = aff_dim S› aff_dim_empty)
  then obtain z where "z ∈ U"
    by auto
  then have bne: "ball z 1 ∩ U ≠ {}" by force
  have [simp]: "aff_dim(ball z 1 ∩ U) = aff_dim U"
    using aff_dim_convex_Int_open [OF ‹convex U› open_ball] bne
    by (fastforce simp add: Int_commute)
  have "rel_frontier S homeomorphic rel_frontier (ball z 1 ∩ U)"
    apply (rule homeomorphic_rel_frontiers_convex_bounded_sets)
    apply (auto simp: ‹affine U› affine_imp_convex convex_Int affdS assms)
    done
  also have "... = sphere z 1 ∩ U"
    using convex_affine_rel_frontier_Int [of "ball z 1" U]
    by (simp add: ‹affine U› bne)
  finally obtain h k where him: "h ` rel_frontier S = sphere z 1 ∩ U"
                    and kim: "k ` (sphere z 1 ∩ U) = rel_frontier S"
                    and hcon: "continuous_on (rel_frontier S) h"
                    and kcon: "continuous_on (sphere z 1 ∩ U) k"
                    and kh:  "⋀x. x ∈ rel_frontier S ⟹ k(h(x)) = x"
                    and hk:  "⋀y. y ∈ sphere z 1 ∩ U ⟹ h(k(y)) = y"
    unfolding homeomorphic_def homeomorphism_def by auto
  have "rel_frontier S - {a} homeomorphic (sphere z 1 ∩ U) - {h a}"
  proof (rule homeomorphicI [where f=h and g=k])
    show h: "h ` (rel_frontier S - {a}) = sphere z 1 ∩ U - {h a}"
      using him a kh by auto metis
    show "k ` (sphere z 1 ∩ U - {h a}) = rel_frontier S - {a}"
      by (force simp: h [symmetric] image_comp o_def kh)
  qed (auto intro: continuous_on_subset hcon kcon simp: kh hk)
  also have "... homeomorphic T"
    apply (rule homeomorphic_punctured_affine_sphere_affine)
    using a him
    by (auto simp: affS affdS ‹affine T›  ‹affine U› ‹z ∈ U›)
  finally show ?thesis .
qed


lemma homeomorphic_punctured_sphere_affine:
  fixes a :: "'a :: euclidean_space"
  assumes "0 < r" and b: "b ∈ sphere a r"
      and "affine T" and affS: "aff_dim T + 1 = DIM('a)"
    shows "(sphere a r - {b}) homeomorphic T"
using homeomorphic_punctured_sphere_affine_gen [of "cball a r" b T]
  assms aff_dim_cball by force

corollary homeomorphic_punctured_sphere_hyperplane:
  fixes a :: "'a :: euclidean_space"
  assumes "0 < r" and b: "b ∈ sphere a r"
      and "c ≠ 0"
    shows "(sphere a r - {b}) homeomorphic {x::'a. c ∙ x = d}"
apply (rule homeomorphic_punctured_sphere_affine)
using assms
apply (auto simp: affine_hyperplane of_nat_diff)
done


text‹ When dealing with AR, ANR and ANR later, it's useful to know that every set
  is homeomorphic to a closed subset of a convex set, and
  if the set is locally compact we can take the convex set to be the universe.›

proposition homeomorphic_closedin_convex:
  fixes S :: "'m::euclidean_space set"
  assumes "aff_dim S < DIM('n)"
  obtains U and T :: "'n::euclidean_space set"
     where "convex U" "U ≠ {}" "closedin (subtopology euclidean U) T"
           "S homeomorphic T"
proof (cases "S = {}")
  case True then show ?thesis
    by (rule_tac U=UNIV and T="{}" in that) auto
next
  case False
  then obtain a where "a ∈ S" by auto
  obtain i::'n where i: "i ∈ Basis" "i ≠ 0"
    using SOME_Basis Basis_zero by force
  have "0 ∈ affine hull (op + (- a) ` S)"
    by (simp add: ‹a ∈ S› hull_inc)
  then have "dim (op + (- a) ` S) = aff_dim (op + (- a) ` S)"
    by (simp add: aff_dim_zero)
  also have "... < DIM('n)"
    by (simp add: aff_dim_translation_eq assms)
  finally have dd: "dim (op + (- a) ` S) < DIM('n)"
    by linarith
  obtain T where "subspace T" and Tsub: "T ⊆ {x. i ∙ x = 0}"
             and dimT: "dim T = dim (op + (- a) ` S)"
    apply (rule choose_subspace_of_subspace [of "dim (op + (- a) ` S)" "{x::'n. i ∙ x = 0}"])
     apply (simp add: dim_hyperplane [OF ‹i ≠ 0›])
     apply (metis DIM_positive Suc_pred dd not_le not_less_eq_eq)
    apply (metis span_eq subspace_hyperplane)
    done
  have "subspace (span (op + (- a) ` S))"
    using subspace_span by blast
  then obtain h k where "linear h" "linear k"
               and heq: "h ` span (op + (- a) ` S) = T"
               and keq:"k ` T = span (op + (- a) ` S)"
               and hinv [simp]:  "⋀x. x ∈ span (op + (- a) ` S) ⟹ k(h x) = x"
               and kinv [simp]:  "⋀x. x ∈ T ⟹ h(k x) = x"
    apply (rule isometries_subspaces [OF _ ‹subspace T›])
    apply (auto simp: dimT)
    done
  have hcont: "continuous_on A h" and kcont: "continuous_on B k" for A B
    using ‹linear h› ‹linear k› linear_continuous_on linear_conv_bounded_linear by blast+
  have ihhhh[simp]: "⋀x. x ∈ S ⟹ i ∙ h (x - a) = 0"
    using Tsub [THEN subsetD] heq span_inc by fastforce
  have "sphere 0 1 - {i} homeomorphic {x. i ∙ x = 0}"
    apply (rule homeomorphic_punctured_sphere_affine)
    using i
    apply (auto simp: affine_hyperplane)
    by (metis DIM_positive Suc_eq_plus1 add.left_neutral diff_add_cancel not_le not_less_eq_eq of_nat_1 of_nat_diff)
  then obtain f g where fg: "homeomorphism (sphere 0 1 - {i}) {x. i ∙ x = 0} f g"
    by (force simp: homeomorphic_def)
  have "h ` op + (- a) ` S ⊆ T"
    using heq span_clauses(1) span_linear_image by blast
  then have "g ` h ` op + (- a) ` S ⊆ g ` {x. i ∙ x = 0}"
    using Tsub by (simp add: image_mono)
  also have "... ⊆ sphere 0 1 - {i}"
    by (simp add: fg [unfolded homeomorphism_def])
  finally have gh_sub_sph: "(g ∘ h) ` op + (- a) ` S ⊆ sphere 0 1 - {i}"
    by (metis image_comp)
  then have gh_sub_cb: "(g ∘ h) ` op + (- a) ` S ⊆ cball 0 1"
    by (metis Diff_subset order_trans sphere_cball)
  have [simp]: "⋀u. u ∈ S ⟹ norm (g (h (u - a))) = 1"
    using gh_sub_sph [THEN subsetD] by (auto simp: o_def)
  have ghcont: "continuous_on (op + (- a) ` S) (λx. g (h x))"
    apply (rule continuous_on_compose2 [OF homeomorphism_cont2 [OF fg] hcont], force)
    done
  have kfcont: "continuous_on ((g ∘ h ∘ op + (- a)) ` S) (λx. k (f x))"
    apply (rule continuous_on_compose2 [OF kcont])
    using homeomorphism_cont1 [OF fg] gh_sub_sph apply (force intro: continuous_on_subset, blast)
    done
  have "S homeomorphic op + (- a) ` S"
    by (simp add: homeomorphic_translation)
  also have Shom: "… homeomorphic (g ∘ h) ` op + (- a) ` S"
    apply (simp add: homeomorphic_def homeomorphism_def)
    apply (rule_tac x="g ∘ h" in exI)
    apply (rule_tac x="k ∘ f" in exI)
    apply (auto simp: ghcont kfcont span_clauses(1) homeomorphism_apply2 [OF fg] image_comp)
    apply (force simp: o_def homeomorphism_apply2 [OF fg] span_clauses(1))
    done
  finally have Shom: "S homeomorphic (g ∘ h) ` op + (- a) ` S" .
  show ?thesis
    apply (rule_tac U = "ball 0 1 ∪ image (g o h) (op + (- a) ` S)"
                and T = "image (g o h) (op + (- a) ` S)"
                    in that)
    apply (rule convex_intermediate_ball [of 0 1], force)
    using gh_sub_cb apply force
    apply force
    apply (simp add: closedin_closed)
    apply (rule_tac x="sphere 0 1" in exI)
    apply (auto simp: Shom)
    done
qed

subsection‹Locally compact sets in an open set›

text‹ Locally compact sets are closed in an open set and are homeomorphic
  to an absolutely closed set if we have one more dimension to play with.›

lemma locally_compact_open_Int_closure:
  fixes S :: "'a :: metric_space set"
  assumes "locally compact S"
  obtains T where "open T" "S = T ∩ closure S"
proof -
  have "∀x∈S. ∃T v u. u = S ∩ T ∧ x ∈ u ∧ u ⊆ v ∧ v ⊆ S ∧ open T ∧ compact v"
    by (metis assms locally_compact openin_open)
  then obtain t v where
        tv: "⋀x. x ∈ S
             ⟹ v x ⊆ S ∧ open (t x) ∧ compact (v x) ∧ (∃u. x ∈ u ∧ u ⊆ v x ∧ u = S ∩ t x)"
    by metis
  then have o: "open (UNION S t)"
    by blast
  have "S = ⋃ (v ` S)"
    using tv by blast
  also have "... = UNION S t ∩ closure S"
  proof
    show "UNION S v ⊆ UNION S t ∩ closure S"
      apply safe
       apply (metis Int_iff subsetD UN_iff tv)
      apply (simp add: closure_def rev_subsetD tv)
      done
    have "t x ∩ closure S ⊆ v x" if "x ∈ S" for x
    proof -
      have "t x ∩ closure S ⊆ closure (t x ∩ S)"
        by (simp add: open_Int_closure_subset that tv)
      also have "... ⊆ v x"
        by (metis Int_commute closure_minimal compact_imp_closed that tv)
      finally show ?thesis .
    qed
    then show "UNION S t ∩ closure S ⊆ UNION S v"
      by blast
  qed
  finally have e: "S = UNION S t ∩ closure S" .
  show ?thesis
    by (rule that [OF o e])
qed


lemma locally_compact_closedin_open:
    fixes S :: "'a :: metric_space set"
    assumes "locally compact S"
    obtains T where "open T" "closedin (subtopology euclidean T) S"
  by (metis locally_compact_open_Int_closure [OF assms] closed_closure closedin_closed_Int)


lemma locally_compact_homeomorphism_projection_closed:
  assumes "locally compact S"
  obtains T and f :: "'a ⇒ 'a :: euclidean_space × 'b :: euclidean_space"
    where "closed T" "homeomorphism S T f fst"
proof (cases "closed S")
  case True
    then show ?thesis
      apply (rule_tac T = "S × {0}" and f = "λx. (x, 0)" in that)
      apply (auto simp: closed_Times homeomorphism_def continuous_intros)
      done
next
  case False
    obtain U where "open U" and US: "U ∩ closure S = S"
      by (metis locally_compact_open_Int_closure [OF assms])
    with False have Ucomp: "-U ≠ {}"
      using closure_eq by auto
    have [simp]: "closure (- U) = -U"
      by (simp add: ‹open U› closed_Compl)
    define f :: "'a ⇒ 'a × 'b" where "f ≡ λx. (x, One /R setdist {x} (- U))"
    have "continuous_on U (λx. (x, One /R setdist {x} (- U)))"
      apply (intro continuous_intros continuous_on_setdist)
      by (simp add: Ucomp setdist_eq_0_sing_1)
    then have homU: "homeomorphism U (f`U) f fst"
      by (auto simp: f_def homeomorphism_def image_iff continuous_intros)
    have cloS: "closedin (subtopology euclidean U) S"
      by (metis US closed_closure closedin_closed_Int)
    have cont: "isCont ((λx. setdist {x} (- U)) o fst) z" for z :: "'a × 'b"
      by (rule isCont_o continuous_intros continuous_at_setdist)+
    have setdist1D: "setdist {a} (- U) *R b = One ⟹ setdist {a} (- U) ≠ 0" for a::'a and b::'b
      by force
    have *: "r *R b = One ⟹ b = (1 / r) *R One" for r and b::'b
      by (metis One_non_0 nonzero_divide_eq_eq real_vector.scale_eq_0_iff real_vector.scale_scale scaleR_one)
    have "f ` U = {z. (setdist {fst z} (- U) *R snd z) ∈ {One}}"
      apply (auto simp: f_def setdist_eq_0_sing_1 field_simps Ucomp)
      apply (rule_tac x=a in image_eqI)
      apply (auto simp: * setdist_eq_0_sing_1 dest: setdist1D)
      done
    then have clfU: "closed (f ` U)"
      apply (rule ssubst)
      apply (rule continuous_closed_preimage_univ)
      apply (auto intro: continuous_intros cont [unfolded o_def])
      done
    have "closed (f ` S)"
       apply (rule closedin_closed_trans [OF _ clfU])
       apply (rule homeomorphism_imp_closed_map [OF homU cloS])
       done
    then show ?thesis
      apply (rule that)
      apply (rule homeomorphism_of_subsets [OF homU])
      using US apply auto
      done
qed

lemma locally_compact_closed_Int_open:
  fixes S :: "'a :: euclidean_space set"
  shows
    "locally compact S ⟷ (∃U u. closed U ∧ open u ∧ S = U ∩ u)"
by (metis closed_closure closed_imp_locally_compact inf_commute locally_compact_Int locally_compact_open_Int_closure open_imp_locally_compact)


lemma lowerdim_embeddings:
  assumes  "DIM('a) < DIM('b)"
  obtains f :: "'a::euclidean_space*real ⇒ 'b::euclidean_space" 
      and g :: "'b ⇒ 'a*real"
      and j :: 'b
  where "linear f" "linear g" "⋀z. g (f z) = z" "j ∈ Basis" "⋀x. f(x,0) ∙ j = 0"
proof -
  let ?B = "Basis :: ('a*real) set"
  have b01: "(0,1) ∈ ?B"
    by (simp add: Basis_prod_def)
  have "DIM('a * real) ≤ DIM('b)"
    by (simp add: Suc_leI assms)
  then obtain basf :: "'a*real ⇒ 'b" where sbf: "basf ` ?B ⊆ Basis" and injbf: "inj_on basf Basis"
    by (metis finite_Basis card_le_inj)
  define basg:: "'b ⇒ 'a * real" where
    "basg ≡ λi. if i ∈ basf ` Basis then inv_into Basis basf i else (0,1)"
  have bgf[simp]: "basg (basf i) = i" if "i ∈ Basis" for i
    using inv_into_f_f injbf that by (force simp: basg_def)
  have sbg: "basg ` Basis ⊆ ?B" 
    by (force simp: basg_def injbf b01)
  define f :: "'a*real ⇒ 'b" where "f ≡ λu. ∑j∈Basis. (u ∙ basg j) *R j"
  define g :: "'b ⇒ 'a*real" where "g ≡ λz. (∑i∈Basis. (z ∙ basf i) *R i)" 
  show ?thesis
  proof
    show "linear f"
      unfolding f_def
      by (intro linear_compose_sum linearI ballI) (auto simp: algebra_simps)
    show "linear g"
      unfolding g_def
      by (intro linear_compose_sum linearI ballI) (auto simp: algebra_simps)
    have *: "(∑a ∈ Basis. a ∙ basf b * (x ∙ basg a)) = x ∙ b" if "b ∈ Basis" for x b
      using sbf that by auto
    show gf: "g (f x) = x" for x
      apply (rule euclidean_eqI)
      apply (simp add: f_def g_def inner_sum_left scaleR_sum_left algebra_simps)
      apply (simp add: Groups_Big.sum_distrib_left [symmetric] *)
      done
    show "basf(0,1) ∈ Basis"
      using b01 sbf by auto
    then show "f(x,0) ∙ basf(0,1) = 0" for x
      apply (simp add: f_def inner_sum_left)
      apply (rule comm_monoid_add_class.sum.neutral)
      using b01 inner_not_same_Basis by fastforce
  qed
qed

proposition locally_compact_homeomorphic_closed:
  fixes S :: "'a::euclidean_space set"
  assumes "locally compact S" and dimlt: "DIM('a) < DIM('b)"
  obtains T :: "'b::euclidean_space set" where "closed T" "S homeomorphic T"
proof -
  obtain U:: "('a*real)set" and h
    where "closed U" and homU: "homeomorphism S U h fst"
    using locally_compact_homeomorphism_projection_closed assms by metis
  obtain f :: "'a*real ⇒ 'b" and g :: "'b ⇒ 'a*real"
    where "linear f" "linear g" and gf [simp]: "⋀z. g (f z) = z"
    using lowerdim_embeddings [OF dimlt] by metis 
  then have "inj f"
    by (metis injI)
  have gfU: "g ` f ` U = U"
    by (simp add: image_comp o_def)
  have "S homeomorphic U"
    using homU homeomorphic_def by blast
  also have "... homeomorphic f ` U"
    apply (rule homeomorphicI [OF refl gfU])
       apply (meson ‹inj f› ‹linear f› homeomorphism_cont2 linear_homeomorphism_image)
    using ‹linear g› linear_continuous_on linear_conv_bounded_linear apply blast
    apply (auto simp: o_def)
    done
  finally show ?thesis
    apply (rule_tac T = "f ` U" in that)
    apply (rule closed_injective_linear_image [OF ‹closed U› ‹linear f› ‹inj f›], assumption)
    done
qed


lemma homeomorphic_convex_compact_lemma:
  fixes S :: "'a::euclidean_space set"
  assumes "convex S"
    and "compact S"
    and "cball 0 1 ⊆ S"
  shows "S homeomorphic (cball (0::'a) 1)"
proof (rule starlike_compact_projective_special[OF assms(2-3)])
  fix x u
  assume "x ∈ S" and "0 ≤ u" and "u < (1::real)"
  have "open (ball (u *R x) (1 - u))"
    by (rule open_ball)
  moreover have "u *R x ∈ ball (u *R x) (1 - u)"
    unfolding centre_in_ball using ‹u < 1› by simp
  moreover have "ball (u *R x) (1 - u) ⊆ S"
  proof
    fix y
    assume "y ∈ ball (u *R x) (1 - u)"
    then have "dist (u *R x) y < 1 - u"
      unfolding mem_ball .
    with ‹u < 1› have "inverse (1 - u) *R (y - u *R x) ∈ cball 0 1"
      by (simp add: dist_norm inverse_eq_divide norm_minus_commute)
    with assms(3) have "inverse (1 - u) *R (y - u *R x) ∈ S" ..
    with assms(1) have "(1 - u) *R ((y - u *R x) /R (1 - u)) + u *R x ∈ S"
      using ‹x ∈ S› ‹0 ≤ u› ‹u < 1› [THEN less_imp_le] by (rule convexD_alt)
    then show "y ∈ S" using ‹u < 1›
      by simp
  qed
  ultimately have "u *R x ∈ interior S" ..
  then show "u *R x ∈ S - frontier S"
    using frontier_def and interior_subset by auto
qed

proposition homeomorphic_convex_compact_cball:
  fixes e :: real
    and S :: "'a::euclidean_space set"
  assumes "convex S"
    and "compact S"
    and "interior S ≠ {}"
    and "e > 0"
  shows "S homeomorphic (cball (b::'a) e)"
proof -
  obtain a where "a ∈ interior S"
    using assms(3) by auto
  then obtain d where "d > 0" and d: "cball a d ⊆ S"
    unfolding mem_interior_cball by auto
  let ?d = "inverse d" and ?n = "0::'a"
  have "cball ?n 1 ⊆ (λx. inverse d *R (x - a)) ` S"
    apply rule
    apply (rule_tac x="d *R x + a" in image_eqI)
    defer
    apply (rule d[unfolded subset_eq, rule_format])
    using ‹d > 0›
    unfolding mem_cball dist_norm
    apply (auto simp add: mult_right_le_one_le)
    done
  then have "(λx. inverse d *R (x - a)) ` S homeomorphic cball ?n 1"
    using homeomorphic_convex_compact_lemma[of "(λx. ?d *R -a + ?d *R x) ` S",
      OF convex_affinity compact_affinity]
    using assms(1,2)
    by (auto simp add: scaleR_right_diff_distrib)
  then show ?thesis
    apply (rule_tac homeomorphic_trans[OF _ homeomorphic_balls(2)[of 1 _ ?n]])
    apply (rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" S "?d *R -a"]])
    using ‹d>0› ‹e>0›
    apply (auto simp add: scaleR_right_diff_distrib)
    done
qed

corollary homeomorphic_convex_compact:
  fixes S :: "'a::euclidean_space set"
    and T :: "'a set"
  assumes "convex S" "compact S" "interior S ≠ {}"
    and "convex T" "compact T" "interior T ≠ {}"
  shows "S homeomorphic T"
  using assms
  by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)

subsection‹Covering spaces and lifting results for them›

definition covering_space
           :: "'a::topological_space set ⇒ ('a ⇒ 'b) ⇒ 'b::topological_space set ⇒ bool"
  where
  "covering_space c p S ≡
       continuous_on c p ∧ p ` c = S ∧
       (∀x ∈ S. ∃T. x ∈ T ∧ openin (subtopology euclidean S) T ∧
                    (∃v. ⋃v = {x. x ∈ c ∧ p x ∈ T} ∧
                        (∀u ∈ v. openin (subtopology euclidean c) u) ∧
                        pairwise disjnt v ∧
                        (∀u ∈ v. ∃q. homeomorphism u T p q)))"

lemma covering_space_imp_continuous: "covering_space c p S ⟹ continuous_on c p"
  by (simp add: covering_space_def)

lemma covering_space_imp_surjective: "covering_space c p S ⟹ p ` c = S"
  by (simp add: covering_space_def)

lemma homeomorphism_imp_covering_space: "homeomorphism S T f g ⟹ covering_space S f T"
  apply (simp add: homeomorphism_def covering_space_def, clarify)
  apply (rule_tac x=T in exI, simp)
  apply (rule_tac x="{S}" in exI, auto)
  done

lemma covering_space_local_homeomorphism:
  assumes "covering_space c p S" "x ∈ c"
  obtains T u q where "x ∈ T" "openin (subtopology euclidean c) T"
                      "p x ∈ u" "openin (subtopology euclidean S) u"
                      "homeomorphism T u p q"
using assms
apply (simp add: covering_space_def, clarify)
apply (drule_tac x="p x" in bspec, force)
by (metis (no_types, lifting) Union_iff mem_Collect_eq)


lemma covering_space_local_homeomorphism_alt:
  assumes p: "covering_space c p S" and "y ∈ S"
  obtains x T u q where "p x = y"
                        "x ∈ T" "openin (subtopology euclidean c) T"
                        "y ∈ u" "openin (subtopology euclidean S) u"
                          "homeomorphism T u p q"
proof -
  obtain x where "p x = y" "x ∈ c"
    using assms covering_space_imp_surjective by blast
  show ?thesis
    apply (rule covering_space_local_homeomorphism [OF p ‹x ∈ c›])
    using that ‹p x = y› by blast
qed

proposition covering_space_open_map:
  fixes S :: "'a :: metric_space set" and T :: "'b :: metric_space set"
  assumes p: "covering_space c p S" and T: "openin (subtopology euclidean c) T"
    shows "openin (subtopology euclidean S) (p ` T)"
proof -
  have pce: "p ` c = S"
   and covs:
       "⋀x. x ∈ S ⟹
            ∃X VS. x ∈ X ∧ openin (subtopology euclidean S) X ∧
                  ⋃VS = {x. x ∈ c ∧ p x ∈ X} ∧
                  (∀u ∈ VS. openin (subtopology euclidean c) u) ∧
                  pairwise disjnt VS ∧
                  (∀u ∈ VS. ∃q. homeomorphism u X p q)"
    using p by (auto simp: covering_space_def)
  have "T ⊆ c"  by (metis openin_euclidean_subtopology_iff T)
  have "∃X. openin (subtopology euclidean S) X ∧ y ∈ X ∧ X ⊆ p ` T"
          if "y ∈ p ` T" for y
  proof -
    have "y ∈ S" using ‹T ⊆ c› pce that by blast
    obtain U VS where "y ∈ U" and U: "openin (subtopology euclidean S) U"
                  and VS: "⋃VS = {x. x ∈ c ∧ p x ∈ U}"
                  and openVS: "∀V ∈ VS. openin (subtopology euclidean c) V"
                  and homVS: "⋀V. V ∈ VS ⟹ ∃q. homeomorphism V U p q"
      using covs [OF ‹y ∈ S›] by auto
    obtain x where "x ∈ c" "p x ∈ U" "x ∈ T" "p x = y"
      apply simp
      using T [unfolded openin_euclidean_subtopology_iff] ‹y ∈ U› ‹y ∈ p ` T› by blast
    with VS obtain V where "x ∈ V" "V ∈ VS" by auto
    then obtain q where q: "homeomorphism V U p q" using homVS by blast
    then have ptV: "p ` (T ∩ V) = U ∩ {z. q z ∈ (T ∩ V)}"
      using VS ‹V ∈ VS› by (auto simp: homeomorphism_def)
    have ocv: "openin (subtopology euclidean c) V"
      by (simp add: ‹V ∈ VS› openVS)
    have "openin (subtopology euclidean U) {z ∈ U. q z ∈ T ∩ V}"
      apply (rule continuous_on_open [THEN iffD1, rule_format])
       using homeomorphism_def q apply blast
      using openin_subtopology_Int_subset [of c] q T unfolding homeomorphism_def
      by (metis inf.absorb_iff2 Int_commute ocv openin_euclidean_subtopology_iff)
    then have os: "openin (subtopology euclidean S) (U ∩ {z. q z ∈ T ∩ V})"
      using openin_trans [of U] by (simp add: Collect_conj_eq U)
    show ?thesis
      apply (rule_tac x = "p ` (T ∩ V)" in exI)
      apply (rule conjI)
      apply (simp only: ptV os)
      using ‹p x = y› ‹x ∈ V› ‹x ∈ T› apply blast
      done
  qed
  with openin_subopen show ?thesis by blast
qed

lemma covering_space_lift_unique_gen:
  fixes f :: "'a::topological_space ⇒ 'b::topological_space"
  fixes g1 :: "'a ⇒ 'c::real_normed_vector"
  assumes cov: "covering_space c p S"
      and eq: "g1 a = g2 a"
      and f: "continuous_on T f"  "f ` T ⊆ S"
      and g1: "continuous_on T g1"  "g1 ` T ⊆ c"
      and fg1: "⋀x. x ∈ T ⟹ f x = p(g1 x)"
      and g2: "continuous_on T g2"  "g2 ` T ⊆ c"
      and fg2: "⋀x. x ∈ T ⟹ f x = p(g2 x)"
      and u_compt: "U ∈ components T" and "a ∈ U" "x ∈ U"
    shows "g1 x = g2 x"
proof -
  have "U ⊆ T" by (rule in_components_subset [OF u_compt])
  define G12 where "G12 ≡ {x ∈ U. g1 x - g2 x = 0}"
  have "connected U" by (rule in_components_connected [OF u_compt])
  have contu: "continuous_on U g1" "continuous_on U g2"
       using ‹U ⊆ T› continuous_on_subset g1 g2 by blast+
  have o12: "openin (subtopology euclidean U) G12"
  unfolding G12_def
  proof (subst openin_subopen, clarify)
    fix z
    assume z: "z ∈ U" "g1 z - g2 z = 0"
    obtain v w q where "g1 z ∈ v" and ocv: "openin (subtopology euclidean c) v"
                   and "p (g1 z) ∈ w" and osw: "openin (subtopology euclidean S) w"
                   and hom: "homeomorphism v w p q"
      apply (rule_tac x = "g1 z" in covering_space_local_homeomorphism [OF cov])
       using ‹U ⊆ T› ‹z ∈ U› g1(2) apply blast+
      done
    have "g2 z ∈ v" using ‹g1 z ∈ v› z by auto
    have gg: "{x ∈ U. g x ∈ v} = {x ∈ U. g x ∈ (v ∩ g ` U)}" for g
      by auto
    have "openin (subtopology euclidean (g1 ` U)) (v ∩ g1 ` U)"
      using ocv ‹U ⊆ T› g1 by (fastforce simp add: openin_open)
    then have 1: "openin (subtopology euclidean U) {x ∈ U. g1 x ∈ v}"
      unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
    have "openin (subtopology euclidean (g2 ` U)) (v ∩ g2 ` U)"
      using ocv ‹U ⊆ T› g2 by (fastforce simp add: openin_open)
    then have 2: "openin (subtopology euclidean U) {x ∈ U. g2 x ∈ v}"
      unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
    show "∃T. openin (subtopology euclidean U) T ∧
              z ∈ T ∧ T ⊆ {z ∈ U. g1 z - g2 z = 0}"
      using z
      apply (rule_tac x = "{x. x ∈ U ∧ g1 x ∈ v} ∩ {x. x ∈ U ∧ g2 x ∈ v}" in exI)
      apply (intro conjI)
      apply (rule openin_Int [OF 1 2])
      using ‹g1 z ∈ v›  ‹g2 z ∈ v›  apply (force simp:, clarify)
      apply (metis ‹U ⊆ T› subsetD eq_iff_diff_eq_0 fg1 fg2 hom homeomorphism_def)
      done
  qed
  have c12: "closedin (subtopology euclidean U) G12"
    unfolding G12_def
    by (intro continuous_intros continuous_closedin_preimage_constant contu)
  have "G12 = {} ∨ G12 = U"
    by (intro connected_clopen [THEN iffD1, rule_format] ‹connected U› conjI o12 c12)
  with eq ‹a ∈ U› have "⋀x. x ∈ U ⟹ g1 x - g2 x = 0" by (auto simp: G12_def)
  then show ?thesis
    using ‹x ∈ U› by force
qed

proposition covering_space_lift_unique:
  fixes f :: "'a::topological_space ⇒ 'b::topological_space"
  fixes g1 :: "'a ⇒ 'c::real_normed_vector"
  assumes "covering_space c p S"
          "g1 a = g2 a"
          "continuous_on T f"  "f ` T ⊆ S"
          "continuous_on T g1"  "g1 ` T ⊆ c"  "⋀x. x ∈ T ⟹ f x = p(g1 x)"
          "continuous_on T g2"  "g2 ` T ⊆ c"  "⋀x. x ∈ T ⟹ f x = p(g2 x)"
          "connected T"  "a ∈ T"   "x ∈ T"
   shows "g1 x = g2 x"
using covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv by blast

lemma covering_space_locally:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
  assumes loc: "locally φ C" and cov: "covering_space C p S"
      and pim: "⋀T. ⟦T ⊆ C; φ T⟧ ⟹ ψ(p ` T)"
    shows "locally ψ S"
proof -
  have "locally ψ (p ` C)"
    apply (rule locally_open_map_image [OF loc])
    using cov covering_space_imp_continuous apply blast
    using cov covering_space_imp_surjective covering_space_open_map apply blast
    by (simp add: pim)
  then show ?thesis
    using covering_space_imp_surjective [OF cov] by metis
qed


proposition covering_space_locally_eq:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
  assumes cov: "covering_space C p S"
      and pim: "⋀T. ⟦T ⊆ C; φ T⟧ ⟹ ψ(p ` T)"
      and qim: "⋀q U. ⟦U ⊆ S; continuous_on U q; ψ U⟧ ⟹ φ(q ` U)"
    shows "locally ψ S ⟷ locally φ C"
         (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  show ?rhs
  proof (rule locallyI)
    fix V x
    assume V: "openin (subtopology euclidean C) V" and "x ∈ V"
    have "p x ∈ p ` C"
      by (metis IntE V ‹x ∈ V› imageI openin_open)
    then obtain T 𝒱 where "p x ∈ T"
                      and opeT: "openin (subtopology euclidean S) T"
                      and veq: "⋃𝒱 = {x ∈ C. p x ∈ T}"
                      and ope: "∀U∈𝒱. openin (subtopology euclidean C) U"
                      and hom: "∀U∈𝒱. ∃q. homeomorphism U T p q"
      using cov unfolding covering_space_def by (blast intro: that)
    have "x ∈ ⋃𝒱"
      using V veq ‹p x ∈ T› ‹x ∈ V› openin_imp_subset by fastforce
    then obtain U where "x ∈ U" "U ∈ 𝒱"
      by blast
    then obtain q where opeU: "openin (subtopology euclidean C) U" and q: "homeomorphism U T p q"
      using ope hom by blast
    with V have "openin (subtopology euclidean C) (U ∩ V)"
      by blast
    then have UV: "openin (subtopology euclidean S) (p ` (U ∩ V))"
      using cov covering_space_open_map by blast
    obtain W W' where opeW: "openin (subtopology euclidean S) W" and "ψ W'" "p x ∈ W" "W ⊆ W'" and W'sub: "W' ⊆ p ` (U ∩ V)"
      using locallyE [OF L UV] ‹x ∈ U› ‹x ∈ V› by blast
    then have "W ⊆ T"
      by (metis Int_lower1 q homeomorphism_image1 image_Int_subset order_trans)
    show "∃U Z. openin (subtopology euclidean C) U ∧
                 φ Z ∧ x ∈ U ∧ U ⊆ Z ∧ Z ⊆ V"
    proof (intro exI conjI)
      have "openin (subtopology euclidean T) W"
        by (meson opeW opeT openin_imp_subset openin_subset_trans ‹W ⊆ T›)
      then have "openin (subtopology euclidean U) (q ` W)"
        by (meson homeomorphism_imp_open_map homeomorphism_symD q)
      then show "openin (subtopology euclidean C) (q ` W)"
        using opeU openin_trans by blast
      show "φ (q ` W')"
        by (metis (mono_tags, lifting) Int_subset_iff UV W'sub ‹ψ W'› continuous_on_subset dual_order.trans homeomorphism_def image_Int_subset openin_imp_subset q qim)
      show "x ∈ q ` W"
        by (metis ‹p x ∈ W› ‹x ∈ U› homeomorphism_def imageI q)
      show "q ` W ⊆ q ` W'"
        using ‹W ⊆ W'› by blast
      have "W' ⊆ p ` V"
        using W'sub by blast
      then show "q ` W' ⊆ V"
        using W'sub homeomorphism_apply1 [OF q] by auto
      qed
  qed
next
  assume ?rhs
  then show ?lhs
    using cov covering_space_locally pim by blast
qed

lemma covering_space_locally_compact_eq:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
  assumes "covering_space C p S"
  shows "locally compact S ⟷ locally compact C"
  apply (rule covering_space_locally_eq [OF assms])
   apply (meson assms compact_continuous_image continuous_on_subset covering_space_imp_continuous)
  using compact_continuous_image by blast

lemma covering_space_locally_connected_eq:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
  assumes "covering_space C p S"
    shows "locally connected S ⟷ locally connected C"
  apply (rule covering_space_locally_eq [OF assms])
   apply (meson connected_continuous_image assms continuous_on_subset covering_space_imp_continuous)
  using connected_continuous_image by blast

lemma covering_space_locally_path_connected_eq:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
  assumes "covering_space C p S"
    shows "locally path_connected S ⟷ locally path_connected C"
  apply (rule covering_space_locally_eq [OF assms])
   apply (meson path_connected_continuous_image assms continuous_on_subset covering_space_imp_continuous)
  using path_connected_continuous_image by blast


lemma covering_space_locally_compact:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
  assumes "locally compact C" "covering_space C p S"
  shows "locally compact S"
  using assms covering_space_locally_compact_eq by blast


lemma covering_space_locally_connected:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
  assumes "locally connected C" "covering_space C p S"
  shows "locally connected S"
  using assms covering_space_locally_connected_eq by blast

lemma covering_space_locally_path_connected:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
  assumes "locally path_connected C" "covering_space C p S"
  shows "locally path_connected S"
  using assms covering_space_locally_path_connected_eq by blast

proposition covering_space_lift_homotopy:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
    and h :: "real × 'c::real_normed_vector ⇒ 'b"
  assumes cov: "covering_space C p S"
      and conth: "continuous_on ({0..1} × U) h"
      and him: "h ` ({0..1} × U) ⊆ S"
      and heq: "⋀y. y ∈ U ⟹ h (0,y) = p(f y)"
      and contf: "continuous_on U f" and fim: "f ` U ⊆ C"
    obtains k where "continuous_on ({0..1} × U) k"
                    "k ` ({0..1} × U) ⊆ C"
                    "⋀y. y ∈ U ⟹ k(0, y) = f y"
                    "⋀z. z ∈ {0..1} × U ⟹ h z = p(k z)"
proof -
  have "∃V k. openin (subtopology euclidean U) V ∧ y ∈ V ∧
              continuous_on ({0..1} × V) k ∧ k ` ({0..1} × V) ⊆ C ∧
              (∀z ∈ V. k(0, z) = f z) ∧ (∀z ∈ {0..1} × V. h z = p(k z))"
        if "y ∈ U" for y
  proof -
    obtain UU where UU: "⋀s. s ∈ S ⟹ s ∈ (UU s) ∧ openin (subtopology euclidean S) (UU s) ∧
                                        (∃𝒱. ⋃𝒱 = {x. x ∈ C ∧ p x ∈ (UU s)} ∧
                                            (∀U ∈ 𝒱. openin (subtopology euclidean C) U) ∧
                                            pairwise disjnt 𝒱 ∧
                                            (∀U ∈ 𝒱. ∃q. homeomorphism U (UU s) p q))"
      using cov unfolding covering_space_def by (metis (mono_tags))
    then have ope: "⋀s. s ∈ S ⟹ s ∈ (UU s) ∧ openin (subtopology euclidean S) (UU s)"
      by blast
    have "∃k n i. open k ∧ open n ∧
                  t ∈ k ∧ y ∈ n ∧ i ∈ S ∧ h ` (({0..1} ∩ k) × (U ∩ n)) ⊆ UU i" if "t ∈ {0..1}" for t
    proof -
      have hinS: "h (t, y) ∈ S"
        using ‹y ∈ U› him that by blast
      then have "(t,y) ∈ {z ∈ {0..1} × U. h z ∈ UU (h (t, y))}"
        using ‹y ∈ U› ‹t ∈ {0..1}›  by (auto simp: ope)
      moreover have ope_01U: "openin (subtopology euclidean ({0..1} × U)) {z. z ∈ ({0..1} × U) ∧ h z ∈ UU(h(t, y))}"
        using hinS ope continuous_on_open_gen [OF him] conth by blast
      ultimately obtain V W where opeV: "open V" and "t ∈ {0..1} ∩ V" "t ∈ {0..1} ∩ V"
                              and opeW: "open W" and "y ∈ U" "y ∈ W"
                              and VW: "({0..1} ∩ V) × (U ∩ W)  ⊆ {z. z ∈ ({0..1} × U) ∧ h z ∈ UU(h(t, y))}"
        by (rule Times_in_interior_subtopology) (auto simp: openin_open)
      then show ?thesis
        using hinS by blast
    qed
    then obtain K NN X where
              K: "⋀t. t ∈ {0..1} ⟹ open (K t)"
          and NN: "⋀t. t ∈ {0..1} ⟹ open (NN t)"
          and inUS: "⋀t. t ∈ {0..1} ⟹ t ∈ K t ∧ y ∈ NN t ∧ X t ∈ S"
          and him: "⋀t. t ∈ {0..1} ⟹ h ` (({0..1} ∩ K t) × (U ∩ NN t)) ⊆ UU (X t)"
    by (metis (mono_tags))
    obtain 𝒯 where "𝒯 ⊆ ((λi. K i × NN i)) ` {0..1}" "finite 𝒯" "{0::real..1} × {y} ⊆ ⋃𝒯"
    proof (rule compactE)
      show "compact ({0::real..1} × {y})"
        by (simp add: compact_Times)
      show "{0..1} × {y} ⊆ (⋃i∈{0..1}. K i × NN i)"
        using K inUS by auto
      show "⋀B. B ∈ (λi. K i × NN i) ` {0..1} ⟹ open B"
        using K NN by (auto simp: open_Times)
    qed blast
    then obtain tk where "tk ⊆ {0..1}" "finite tk"
                     and tk: "{0::real..1} × {y} ⊆ (⋃i ∈ tk. K i × NN i)"
      by (metis (no_types, lifting) finite_subset_image)
    then have "tk ≠ {}"
      by auto
    define n where "n = INTER tk NN"
    have "y ∈ n" "open n"
      using inUS NN ‹tk ⊆ {0..1}› ‹finite tk›
      by (auto simp: n_def open_INT subset_iff)
    obtain δ where "0 < δ" and δ: "⋀T. ⟦T ⊆ {0..1}; diameter T < δ⟧ ⟹ ∃B∈K ` tk. T ⊆ B"
    proof (rule Lebesgue_number_lemma [of "{0..1}" "K ` tk"])
      show "K ` tk ≠ {}"
        using ‹tk ≠ {}› by auto
      show "{0..1} ⊆ UNION tk K"
        using tk by auto
      show "⋀B. B ∈ K ` tk ⟹ open B"
        using ‹tk ⊆ {0..1}› K by auto
    qed auto
    obtain N::nat where N: "N > 1 / δ"
      using reals_Archimedean2 by blast
    then have "N > 0"
      using ‹0 < δ› order.asym by force
    have *: "∃V k. openin (subtopology euclidean U) V ∧ y ∈ V ∧
                   continuous_on ({0..of_nat n / N} × V) k ∧
                   k ` ({0..of_nat n / N} × V) ⊆ C ∧
                   (∀z∈V. k (0, z) = f z) ∧
                   (∀z∈{0..of_nat n / N} × V. h z = p (k z))" if "n ≤ N" for n
      using that
    proof (induction n)
      case 0
      show ?case
        apply (rule_tac x=U in exI)
        apply (rule_tac x="f ∘ snd" in exI)
        apply (intro conjI ‹y ∈ U› continuous_intros continuous_on_subset [OF contf])
        using fim  apply (auto simp: heq)
        done
    next
      case (Suc n)
      then obtain V k where opeUV: "openin (subtopology euclidean U) V"
                        and "y ∈ V"
                        and contk: "continuous_on ({0..real n / real N} × V) k"
                        and kim: "k ` ({0..real n / real N} × V) ⊆ C"
                        and keq: "⋀z. z ∈ V ⟹ k (0, z) = f z"
                        and heq: "⋀z. z ∈ {0..real n / real N} × V ⟹ h z = p (k z)"
        using Suc_leD by auto
      have "n ≤ N"
        using Suc.prems by auto
      obtain t where "t ∈ tk" and t: "{real n / real N .. (1 + real n) / real N} ⊆ K t"
      proof (rule bexE [OF δ])
        show "{real n / real N .. (1 + real n) / real N} ⊆ {0..1}"
          using Suc.prems by (auto simp: divide_simps algebra_simps)
        show diameter_less: "diameter {real n / real N .. (1 + real n) / real N} < δ"
          using ‹0 < δ› N by (auto simp: divide_simps algebra_simps)
      qed blast
      have t01: "t ∈ {0..1}"
        using ‹t ∈ tk› ‹tk ⊆ {0..1}› by blast
      obtain 𝒱 where "⋃𝒱 = {x. x ∈ C ∧ p x ∈ (UU (X t))}"
                 and opeC: "⋀U. U ∈ 𝒱 ⟹ openin (subtopology euclidean C) U"
                 and "pairwise disjnt 𝒱"
                 and homuu: "⋀U. U ∈ 𝒱 ⟹ ∃q. homeomorphism U (UU (X t)) p q"
        using inUS [OF t01] UU by meson
      have n_div_N_in: "real n / real N ∈ {real n / real N .. (1 + real n) / real N}"
        using N by (auto simp: divide_simps algebra_simps)
      with t have nN_in_kkt: "real n / real N ∈ K t"
        by blast
      have "k (real n / real N, y) ∈ {x. x ∈ C ∧ p x ∈ (UU (X t))}"
      proof (simp, rule conjI)
        show "k (real n / real N, y) ∈ C"
          using ‹y ∈ V› kim keq by force
        have "p (k (real n / real N, y)) = h (real n / real N, y)"
          by (simp add: ‹y ∈ V› heq)
        also have "... ∈ h ` (({0..1} ∩ K t) × (U ∩ NN t))"
          apply (rule imageI)
           using ‹y ∈ V› t01 ‹n ≤ N›
          apply (simp add: nN_in_kkt ‹y ∈ U› inUS divide_simps)
          done
        also have "... ⊆ UU (X t)"
          using him t01 by blast
        finally show "p (k (real n / real N, y)) ∈ UU (X t)" .
      qed
      then have "k (real n / real N, y) ∈ ⋃𝒱"
        using ‹⋃𝒱 = {x ∈ C. p x ∈ UU (X t)}› by blast
      then obtain W where W: "k (real n / real N, y) ∈ W" and "W ∈ 𝒱"
        by blast
      then obtain p' where opeC': "openin (subtopology euclidean C) W"
                       and hom': "homeomorphism W (UU (X t)) p p'"
        using homuu opeC by blast
      then have "W ⊆ C"
        using openin_imp_subset by blast
      define W' where "W' = UU(X t)"
      have opeVW: "openin (subtopology euclidean V) {z ∈ V. (k ∘ Pair (real n / real N)) z ∈ W}"
        apply (rule continuous_openin_preimage [OF _ _ opeC'])
         apply (intro continuous_intros continuous_on_subset [OF contk])
        using kim apply (auto simp: ‹y ∈ V› W)
        done
      obtain N' where opeUN': "openin (subtopology euclidean U) N'"
                  and "y ∈ N'" and kimw: "k ` ({(real n / real N)} × N') ⊆ W"
        apply (rule_tac N' = "{z ∈ V. (k ∘ Pair ((real n / real N))) z ∈ W}" in that)
        apply (fastforce simp:  ‹y ∈ V› W intro!: openin_trans [OF opeVW opeUV])+
        done
      obtain Q Q' where opeUQ: "openin (subtopology euclidean U) Q"
                    and cloUQ': "closedin (subtopology euclidean U) Q'"
                    and "y ∈ Q" "Q ⊆ Q'"
                    and Q': "Q' ⊆ (U ∩ NN(t)) ∩ N' ∩ V"
      proof -
        obtain VO VX where "open VO" "open VX" and VO: "V = U ∩ VO" and VX: "N' = U ∩ VX"
          using opeUV opeUN' by (auto simp: openin_open)
        then have "open (NN(t) ∩ VO ∩ VX)"
          using NN t01 by blast
        then obtain e where "e > 0" and e: "cball y e ⊆ NN(t) ∩ VO ∩ VX"
          by (metis Int_iff ‹N' = U ∩ VX› ‹V = U ∩ VO› ‹y ∈ N'› ‹y ∈ V› inUS open_contains_cball t01)
        show ?thesis
        proof
          show "openin (subtopology euclidean U) (U ∩ ball y e)"
            by blast
          show "closedin (subtopology euclidean U) (U ∩ cball y e)"
            using e by (auto simp: closedin_closed)
        qed (use ‹y ∈ U› ‹e > 0› VO VX e in auto)
      qed
      then have "y ∈ Q'" "Q ⊆ (U ∩ NN(t)) ∩ N' ∩ V"
        by blast+
      have neq: "{0..real n / real N} ∪ {real n / real N..(1 + real n) / real N} = {0..(1 + real n) / real N}"
        apply (auto simp: divide_simps)
        by (metis mult_zero_left of_nat_0_le_iff of_nat_0_less_iff order_trans real_mult_le_cancel_iff1)
      then have neqQ': "{0..real n / real N} × Q' ∪ {real n / real N..(1 + real n) / real N} × Q' = {0..(1 + real n) / real N} × Q'"
        by blast
      have cont: "continuous_on ({0..(1 + real n) / real N} × Q')
        (λx. if x ∈ {0..real n / real N} × Q' then k x else (p' ∘ h) x)"
        unfolding neqQ' [symmetric]
      proof (rule continuous_on_cases_local, simp_all add: neqQ' del: comp_apply)
        show "closedin (subtopology euclidean ({0..(1 + real n) / real N} × Q'))
                       ({0..real n / real N} × Q')"
          apply (simp add: closedin_closed)
          apply (rule_tac x="{0 .. real n / real N} × UNIV" in exI)
          using n_div_N_in apply (auto simp: closed_Times)
          done
        show "closedin (subtopology euclidean ({0..(1 + real n) / real N} × Q'))
                       ({real n / real N..(1 + real n) / real N} × Q')"
          apply (simp add: closedin_closed)
          apply (rule_tac x="{real n / real N .. (1 + real n) / real N} × UNIV" in exI)
          apply (auto simp: closed_Times)
          by (meson divide_nonneg_nonneg of_nat_0_le_iff order_trans)
        show "continuous_on ({0..real n / real N} × Q') k"
          apply (rule continuous_on_subset [OF contk])
          using Q' by auto
        have "continuous_on ({real n / real N..(1 + real n) / real N} × Q') h"
        proof (rule continuous_on_subset [OF conth])
          show "{real n / real N..(1 + real n) / real N} × Q' ⊆ {0..1} × U"
            using ‹N > 0›
            apply auto
              apply (meson divide_nonneg_nonneg of_nat_0_le_iff order_trans)
            using Suc.prems order_trans apply fastforce
            apply (metis IntE  cloUQ' closedin_closed)
            done
        qed
        moreover have "continuous_on (h ` ({real n / real N..(1 + real n) / real N} × Q')) p'"
        proof (rule continuous_on_subset [OF homeomorphism_cont2 [OF hom']])
          have "h ` ({real n / real N..(1 + real n) / real N} × Q') ⊆ h ` (({0..1} ∩ K t) × (U ∩ NN t))"
            apply (rule image_mono)
            using ‹0 < δ› ‹N > 0› Suc.prems apply auto
              apply (meson divide_nonneg_nonneg of_nat_0_le_iff order_trans)
            using Suc.prems order_trans apply fastforce
            using t Q' apply auto
            done
          with him show "h ` ({real n / real N..(1 + real n) / real N} × Q') ⊆ UU (X t)"
            using t01 by blast
        qed
        ultimately show "continuous_on ({real n / real N..(1 + real n) / real N} × Q') (p' ∘ h)"
          by (rule continuous_on_compose)
        have "k (real n / real N, b) = p' (h (real n / real N, b))" if "b ∈ Q'" for b
        proof -
          have "k (real n / real N, b) ∈ W"
            using that Q' kimw  by force
          then have "k (real n / real N, b) = p' (p (k (real n / real N, b)))"
            by (simp add:  homeomorphism_apply1 [OF hom'])
          then show ?thesis
            using Q' that by (force simp: heq)
        qed
        then show "⋀x. x ∈ {real n / real N..(1 + real n) / real N} × Q' ∧
                  x ∈ {0..real n / real N} × Q' ⟹ k x = (p' ∘ h) x"
          by auto
      qed
      have h_in_UU: "h (x, y) ∈ UU (X t)" if "y ∈ Q" "¬ x ≤ real n / real N" "0 ≤ x" "x ≤ (1 + real n) / real N" for x y
      proof -
        have "x ≤ 1"
          using Suc.prems that order_trans by force
        moreover have "x ∈ K t"
          by (meson atLeastAtMost_iff le_less not_le subset_eq t that)
        moreover have "y ∈ U"
          using ‹y ∈ Q› opeUQ openin_imp_subset by blast
        moreover have "y ∈ NN t"
          using Q' ‹Q ⊆ Q'› ‹y ∈ Q› by auto
        ultimately have "(x, y) ∈ (({0..1} ∩ K t) × (U ∩ NN t))"
          using that by auto
        then have "h (x, y) ∈ h ` (({0..1} ∩ K t) × (U ∩ NN t))"
          by blast
        also have "... ⊆ UU (X t)"
          by (metis him t01)
        finally show ?thesis .
      qed
      let ?k = "(λx. if x ∈ {0..real n / real N} × Q' then k x else (p' ∘ h) x)"
      show ?case
      proof (intro exI conjI)
        show "continuous_on ({0..real (Suc n) / real N} × Q) ?k"
          apply (rule continuous_on_subset [OF cont])
          using ‹Q ⊆ Q'› by auto
        have "⋀a b. ⟦a ≤ real n / real N; b ∈ Q'; 0 ≤ a⟧ ⟹ k (a, b) ∈ C"
          using kim Q' by force
        moreover have "⋀a b. ⟦b ∈ Q; 0 ≤ a; a ≤ (1 + real n) / real N; ¬ a ≤ real n / real N⟧ ⟹ p' (h (a, b)) ∈ C"
          apply (rule ‹W ⊆ C› [THEN subsetD])
          using homeomorphism_image2 [OF hom', symmetric]  h_in_UU  Q' ‹Q ⊆ Q'› ‹W ⊆ C›
          apply auto
          done
        ultimately show "?k ` ({0..real (Suc n) / real N} × Q) ⊆ C"
          using Q' ‹Q ⊆ Q'› by force
        show "∀z∈Q. ?k (0, z) = f z"
          using Q' keq  ‹Q ⊆ Q'› by auto
        show "∀z ∈ {0..real (Suc n) / real N} × Q. h z = p(?k z)"
          using ‹Q ⊆ U ∩ NN t ∩ N' ∩ V› heq apply clarsimp
          using h_in_UU Q' ‹Q ⊆ Q'› apply (auto simp: homeomorphism_apply2 [OF hom', symmetric])
          done
        qed (auto simp: ‹y ∈ Q› opeUQ)
    qed
    show ?thesis
      using*[OF order_refl] N ‹0 < δ› by (simp add: split: if_split_asm)
  qed
  then obtain V fs where opeV: "⋀y. y ∈ U ⟹ openin (subtopology euclidean U) (V y)"
          and V: "⋀y. y ∈ U ⟹ y ∈ V y"
          and contfs: "⋀y. y ∈ U ⟹ continuous_on ({0..1} × V y) (fs y)"
          and *: "⋀y. y ∈ U ⟹ (fs y) ` ({0..1} × V y) ⊆ C ∧
                            (∀z ∈ V y. fs y (0, z) = f z) ∧
                            (∀z ∈ {0..1} × V y. h z = p(fs y z))"
    by (metis (mono_tags))
  then have VU: "⋀y. y ∈ U ⟹ V y ⊆ U"
    by (meson openin_imp_subset)
  obtain k where contk: "continuous_on ({0..1} × U) k"
             and k: "⋀x i. ⟦i ∈ U; x ∈ {0..1} × U ∩ {0..1} × V i⟧ ⟹ k x = fs i x"
  proof (rule pasting_lemma_exists)
    show "{0..1} × U ⊆ (⋃i∈U. {0..1} × V i)"
      apply auto
      using V by blast
    show "⋀i. i ∈ U ⟹ openin (subtopology euclidean ({0..1} × U)) ({0..1} × V i)"
      by (simp add: opeV openin_Times)
    show "⋀i. i ∈ U ⟹ continuous_on ({0..1} × V i) (fs i)"
      using contfs by blast
    show "fs i x = fs j x"  if "i ∈ U" "j ∈ U" and x: "x ∈ {0..1} × U ∩ {0..1} × V i ∩ {0..1} × V j"
         for i j x
    proof -
      obtain u y where "x = (u, y)" "y ∈ V i" "y ∈ V j" "0 ≤ u" "u ≤ 1"
        using x by auto
      show ?thesis
      proof (rule covering_space_lift_unique [OF cov, of _ "(0,y)" _ "{0..1} × {y}" h])
        show "fs i (0, y) = fs j (0, y)"
          using*V by (simp add: ‹y ∈ V i› ‹y ∈ V j› that)
        show conth_y: "continuous_on ({0..1} × {y}) h"
          apply (rule continuous_on_subset [OF conth])
          using VU ‹y ∈ V j› that by auto
        show "h ` ({0..1} × {y}) ⊆ S"
          using ‹y ∈ V i› assms(3) VU that by fastforce
        show "continuous_on ({0..1} × {y}) (fs i)"
          using continuous_on_subset [OF contfs] ‹i ∈ U›
          by (simp add: ‹y ∈ V i› subset_iff)
        show "fs i ` ({0..1} × {y}) ⊆ C"
          using "*" ‹y ∈ V i› ‹i ∈ U› by fastforce
        show "⋀x. x ∈ {0..1} × {y} ⟹ h x = p (fs i x)"
          using "*" ‹y ∈ V i› ‹i ∈ U› by blast
        show "continuous_on ({0..1} × {y}) (fs j)"
          using continuous_on_subset [OF contfs] ‹j ∈ U›
          by (simp add: ‹y ∈ V j› subset_iff)
        show "fs j ` ({0..1} × {y}) ⊆ C"
          using "*" ‹y ∈ V j› ‹j ∈ U› by fastforce
        show "⋀x. x ∈ {0..1} × {y} ⟹ h x = p (fs j x)"
          using "*" ‹y ∈ V j› ‹j ∈ U› by blast
        show "connected ({0..1::real} × {y})"
          using connected_Icc connected_Times connected_sing by blast
        show "(0, y) ∈ {0..1::real} × {y}"
          by force
        show "x ∈ {0..1} × {y}"
          using ‹x = (u, y)› x by blast
      qed
    qed
  qed blast
  show ?thesis
  proof
    show "k ` ({0..1} × U) ⊆ C"
      using V*k VU by fastforce
    show "⋀y. y ∈ U ⟹ k (0, y) = f y"
      by (simp add: V*k)
    show "⋀z. z ∈ {0..1} × U ⟹ h z = p (k z)"
      using V*k by auto
  qed (auto simp: contk)
qed

corollary covering_space_lift_homotopy_alt:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
    and h :: "'c::real_normed_vector × real ⇒ 'b"
  assumes cov: "covering_space C p S"
      and conth: "continuous_on (U × {0..1}) h"
      and him: "h ` (U × {0..1}) ⊆ S"
      and heq: "⋀y. y ∈ U ⟹ h (y,0) = p(f y)"
      and contf: "continuous_on U f" and fim: "f ` U ⊆ C"
  obtains k where "continuous_on (U × {0..1}) k"
                  "k ` (U × {0..1}) ⊆ C"
                  "⋀y. y ∈ U ⟹ k(y, 0) = f y"
                  "⋀z. z ∈ U × {0..1} ⟹ h z = p(k z)"
proof -
  have "continuous_on ({0..1} × U) (h ∘ (λz. (snd z, fst z)))"
    by (intro continuous_intros continuous_on_subset [OF conth]) auto
  then obtain k where contk: "continuous_on ({0..1} × U) k"
                  and kim:  "k ` ({0..1} × U) ⊆ C"
                  and k0: "⋀y. y ∈ U ⟹ k(0, y) = f y"
                  and heqp: "⋀z. z ∈ {0..1} × U ⟹ (h ∘ (λz. Pair (snd z) (fst z))) z = p(k z)"
    apply (rule covering_space_lift_homotopy [OF cov _ _ _ contf fim])
    using him  by (auto simp: contf heq)
  show ?thesis
    apply (rule_tac k="k ∘ (λz. Pair (snd z) (fst z))" in that)
       apply (intro continuous_intros continuous_on_subset [OF contk])
    using kim heqp apply (auto simp: k0)
    done
qed

corollary covering_space_lift_homotopic_function:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector" and g:: "'c::real_normed_vector ⇒ 'a"
  assumes cov: "covering_space C p S"
      and contg: "continuous_on U g"
      and gim: "g ` U ⊆ C"
      and pgeq: "⋀y. y ∈ U ⟹ p(g y) = f y"
      and hom: "homotopic_with (λx. True) U S f f'"
    obtains g' where "continuous_on U g'" "image g' U ⊆ C" "⋀y. y ∈ U ⟹ p(g' y) = f' y"
proof -
  obtain h where conth: "continuous_on ({0..1::real} × U) h"
             and him: "h ` ({0..1} × U) ⊆ S"
             and h0:  "⋀x. h(0, x) = f x"
             and h1: "⋀x. h(1, x) = f' x"
    using hom by (auto simp: homotopic_with_def)
  have "⋀y. y ∈ U ⟹ h (0, y) = p (g y)"
    by (simp add: h0 pgeq)
  then obtain k where contk: "continuous_on ({0..1} × U) k"
                  and kim: "k ` ({0..1} × U) ⊆ C"
                  and k0: "⋀y. y ∈ U ⟹ k(0, y) = g y"
                  and heq: "⋀z. z ∈ {0..1} × U ⟹ h z = p(k z)"
    using covering_space_lift_homotopy [OF cov conth him _ contg gim] by metis
  show ?thesis
  proof
    show "continuous_on U (k ∘ Pair 1)"
      by (meson contk atLeastAtMost_iff continuous_on_o_Pair order_refl zero_le_one)
    show "(k ∘ Pair 1) ` U ⊆ C"
      using kim by auto
    show "⋀y. y ∈ U ⟹ p ((k ∘ Pair 1) y) = f' y"
      by (auto simp: h1 heq [symmetric])
  qed
qed

corollary covering_space_lift_inessential_function:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector" and U :: "'c::real_normed_vector set"
  assumes cov: "covering_space C p S"
      and hom: "homotopic_with (λx. True) U S f (λx. a)"
  obtains g where "continuous_on U g" "g ` U ⊆ C" "⋀y. y ∈ U ⟹ p(g y) = f y"
proof (cases "U = {}")
  case True
  then show ?thesis
    using that continuous_on_empty by blast
next
  case False
  then obtain b where b: "b ∈ C" "p b = a"
    using covering_space_imp_surjective [OF cov] homotopic_with_imp_subset2 [OF hom]
    by auto
  then have gim: "(λy. b) ` U ⊆ C"
    by blast
  show ?thesis
    apply (rule covering_space_lift_homotopic_function
                  [OF cov continuous_on_const gim _ homotopic_with_symD [OF hom]])
    using b that apply auto
    done
qed

subsection‹ Lifting of general functions to covering space›

proposition covering_space_lift_path_strong:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
    and f :: "'c::real_normed_vector ⇒ 'b"
  assumes cov: "covering_space C p S" and "a ∈ C"
      and "path g" and pag: "path_image g ⊆ S" and pas: "pathstart g = p a"
    obtains h where "path h" "path_image h ⊆ C" "pathstart h = a"
                and "⋀t. t ∈ {0..1} ⟹ p(h t) = g t"
proof -
  obtain k:: "real × 'c ⇒ 'a"
    where contk: "continuous_on ({0..1} × {undefined}) k"
      and kim: "k ` ({0..1} × {undefined}) ⊆ C"
      and k0:  "k (0, undefined) = a"
      and pk: "⋀z. z ∈ {0..1} × {undefined} ⟹ p(k z) = (g ∘ fst) z"
  proof (rule covering_space_lift_homotopy [OF cov, of "{undefined}" "g ∘ fst"])
    show "continuous_on ({0..1::real} × {undefined::'c}) (g ∘ fst)"
      apply (intro continuous_intros)
      using ‹path g› by (simp add: path_def)
    show "(g ∘ fst) ` ({0..1} × {undefined}) ⊆ S"
      using pag by (auto simp: path_image_def)
    show "(g ∘ fst) (0, y) = p a" if "y ∈ {undefined}" for y::'c
      by (metis comp_def fst_conv pas pathstart_def)
  qed (use assms in auto)
  show ?thesis
  proof
    show "path (k ∘ (λt. Pair t undefined))"
      unfolding path_def
      by (intro continuous_on_compose continuous_intros continuous_on_subset [OF contk]) auto
    show "path_image (k ∘ (λt. (t, undefined))) ⊆ C"
      using kim by (auto simp: path_image_def)
    show "pathstart (k ∘ (λt. (t, undefined))) = a"
      by (auto simp: pathstart_def k0)
    show "⋀t. t ∈ {0..1} ⟹ p ((k ∘ (λt. (t, undefined))) t) = g t"
      by (auto simp: pk)
  qed
qed

corollary covering_space_lift_path:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
  assumes cov: "covering_space C p S" and "path g" and pig: "path_image g ⊆ S"
  obtains h where "path h" "path_image h ⊆ C" "⋀t. t ∈ {0..1} ⟹ p(h t) = g t"
proof -
  obtain a where "a ∈ C" "pathstart g = p a"
    by (metis pig cov covering_space_imp_surjective imageE pathstart_in_path_image subsetCE)
  show ?thesis
    using covering_space_lift_path_strong [OF cov ‹a ∈ C› ‹path g› pig]
    by (metis ‹pathstart g = p a› that)
qed

  
proposition covering_space_lift_homotopic_paths:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
  assumes cov: "covering_space C p S"
      and "path g1" and pig1: "path_image g1 ⊆ S"
      and "path g2" and pig2: "path_image g2 ⊆ S"
      and hom: "homotopic_paths S g1 g2"
      and "path h1" and pih1: "path_image h1 ⊆ C" and ph1: "⋀t. t ∈ {0..1} ⟹ p(h1 t) = g1 t"
      and "path h2" and pih2: "path_image h2 ⊆ C" and ph2: "⋀t. t ∈ {0..1} ⟹ p(h2 t) = g2 t"
      and h1h2: "pathstart h1 = pathstart h2"
    shows "homotopic_paths C h1 h2"
proof -
  obtain h :: "real × real ⇒ 'b"
     where conth: "continuous_on ({0..1} × {0..1}) h"
       and him: "h ` ({0..1} × {0..1}) ⊆ S"
       and h0: "⋀x. h (0, x) = g1 x" and h1: "⋀x. h (1, x) = g2 x"
       and heq0: "⋀t. t ∈ {0..1} ⟹ h (t, 0) = g1 0"
       and heq1: "⋀t. t ∈ {0..1} ⟹ h (t, 1) = g1 1"
    using hom by (auto simp: homotopic_paths_def homotopic_with_def pathstart_def pathfinish_def)
  obtain k where contk: "continuous_on ({0..1} × {0..1}) k"
             and kim: "k ` ({0..1} × {0..1}) ⊆ C"
             and kh2: "⋀y. y ∈ {0..1} ⟹ k (y, 0) = h2 0"
             and hpk: "⋀z. z ∈ {0..1} × {0..1} ⟹ h z = p (k z)"
    apply (rule covering_space_lift_homotopy_alt [OF cov conth him, of "λx. h2 0"])
    using h1h2 ph1 ph2 apply (force simp: heq0 pathstart_def pathfinish_def)
    using path_image_def pih2 continuous_on_const by fastforce+
  have contg1: "continuous_on {0..1} g1" and contg2: "continuous_on {0..1} g2"
    using ‹path g1› ‹path g2› path_def by blast+
  have g1im: "g1 ` {0..1} ⊆ S" and g2im: "g2 ` {0..1} ⊆ S"
    using path_image_def pig1 pig2 by auto
  have conth1: "continuous_on {0..1} h1" and conth2: "continuous_on {0..1} h2"
    using ‹path h1› ‹path h2› path_def by blast+
  have h1im: "h1 ` {0..1} ⊆ C" and h2im: "h2 ` {0..1} ⊆ C"
    using path_image_def pih1 pih2 by auto
  show ?thesis
    unfolding homotopic_paths pathstart_def pathfinish_def
  proof (intro exI conjI ballI)
    show keqh1: "k(0, x) = h1 x" if "x ∈ {0..1}" for x
    proof (rule covering_space_lift_unique [OF cov _ contg1 g1im])
      show "k (0,0) = h1 0"
        by (metis atLeastAtMost_iff h1h2 kh2 order_refl pathstart_def zero_le_one)
      show "continuous_on {0..1} (λa. k (0, a))"
        by (intro continuous_intros continuous_on_compose2 [OF contk]) auto
      show "⋀x. x ∈ {0..1} ⟹ g1 x = p (k (0, x))"
        by (metis atLeastAtMost_iff h0 hpk zero_le_one mem_Sigma_iff order_refl)
    qed (use conth1 h1im kim that in ‹auto simp: ph1›)
    show "k(1, x) = h2 x" if "x ∈ {0..1}" for x
    proof (rule covering_space_lift_unique [OF cov _ contg2 g2im])
      show "k (1,0) = h2 0"
        by (metis atLeastAtMost_iff kh2 order_refl zero_le_one)
      show "continuous_on {0..1} (λa. k (1, a))"
        by (intro continuous_intros continuous_on_compose2 [OF contk]) auto
      show "⋀x. x ∈ {0..1} ⟹ g2 x = p (k (1, x))"
        by (metis atLeastAtMost_iff h1 hpk mem_Sigma_iff order_refl zero_le_one)
    qed (use conth2 h2im kim that in ‹auto simp: ph2›)
    show "⋀t. t ∈ {0..1} ⟹ (k ∘ Pair t) 0 = h1 0"
      by (metis comp_apply h1h2 kh2 pathstart_def)
    show "(k ∘ Pair t) 1 = h1 1" if "t ∈ {0..1}" for t
    proof (rule covering_space_lift_unique
           [OF cov, of "λa. (k ∘ Pair a) 1" 0 "λa. h1 1" "{0..1}"  "λx. g1 1"])
      show "(k ∘ Pair 0) 1 = h1 1"
        using keqh1 by auto
      show "continuous_on {0..1} (λa. (k ∘ Pair a) 1)"
        apply simp
        by (intro continuous_intros continuous_on_compose2 [OF contk]) auto
      show "⋀x. x ∈ {0..1} ⟹ g1 1 = p ((k ∘ Pair x) 1)"
        using heq1 hpk by auto
    qed (use contk kim g1im h1im that in ‹auto simp: ph1 continuous_on_const›)
  qed (use contk kim in auto)
qed


corollary covering_space_monodromy:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
  assumes cov: "covering_space C p S"
      and "path g1" and pig1: "path_image g1 ⊆ S"
      and "path g2" and pig2: "path_image g2 ⊆ S"
      and hom: "homotopic_paths S g1 g2"
      and "path h1" and pih1: "path_image h1 ⊆ C" and ph1: "⋀t. t ∈ {0..1} ⟹ p(h1 t) = g1 t"
      and "path h2" and pih2: "path_image h2 ⊆ C" and ph2: "⋀t. t ∈ {0..1} ⟹ p(h2 t) = g2 t"
      and h1h2: "pathstart h1 = pathstart h2"
    shows "pathfinish h1 = pathfinish h2"
  using covering_space_lift_homotopic_paths [OF assms] homotopic_paths_imp_pathfinish by blast


corollary covering_space_lift_homotopic_path:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
  assumes cov: "covering_space C p S"
      and hom: "homotopic_paths S f f'"
      and "path g" and pig: "path_image g ⊆ C"
      and a: "pathstart g = a" and b: "pathfinish g = b"
      and pgeq: "⋀t. t ∈ {0..1} ⟹ p(g t) = f t"
  obtains g' where "path g'" "path_image g' ⊆ C"
                   "pathstart g' = a" "pathfinish g' = b" "⋀t. t ∈ {0..1} ⟹ p(g' t) = f' t"
proof (rule covering_space_lift_path_strong [OF cov, of a f'])
  show "a ∈ C"
    using a pig by auto
  show "path f'" "path_image f' ⊆ S"
    using hom homotopic_paths_imp_path homotopic_paths_imp_subset by blast+
  show "pathstart f' = p a"
    by (metis a atLeastAtMost_iff hom homotopic_paths_imp_pathstart order_refl pathstart_def pgeq zero_le_one)
qed (metis (mono_tags, lifting) assms cov covering_space_monodromy hom homotopic_paths_imp_path homotopic_paths_imp_subset pgeq pig)


proposition covering_space_lift_general:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
    and f :: "'c::real_normed_vector ⇒ 'b"
  assumes cov: "covering_space C p S" and "a ∈ C" "z ∈ U"
      and U: "path_connected U" "locally path_connected U"
      and contf: "continuous_on U f" and fim: "f ` U ⊆ S"
      and feq: "f z = p a"
      and hom: "⋀r. ⟦path r; path_image r ⊆ U; pathstart r = z; pathfinish r = z⟧
                     ⟹ ∃q. path q ∧ path_image q ⊆ C ∧
                             pathstart q = a ∧ pathfinish q = a ∧
                             homotopic_paths S (f ∘ r) (p ∘ q)"
  obtains g where "continuous_on U g" "g ` U ⊆ C" "g z = a" "⋀y. y ∈ U ⟹ p(g y) = f y"
proof -
  have *: "∃g h. path g ∧ path_image g ⊆ U ∧
                 pathstart g = z ∧ pathfinish g = y ∧
                 path h ∧ path_image h ⊆ C ∧ pathstart h = a ∧
                 (∀t ∈ {0..1}. p(h t) = f(g t))"
          if "y ∈ U" for y
  proof -
    obtain g where "path g" "path_image g ⊆ U" and pastg: "pathstart g = z"
               and pafig: "pathfinish g = y"
      using U ‹z ∈ U› ‹y ∈ U› by (force simp: path_connected_def)
    obtain h where "path h" "path_image h ⊆ C" "pathstart h = a"
               and "⋀t. t ∈ {0..1} ⟹ p(h t) = (f ∘ g) t"
    proof (rule covering_space_lift_path_strong [OF cov ‹a ∈ C›])
      show "path (f ∘ g)"
        using ‹path g› ‹path_image g ⊆ U› contf continuous_on_subset path_continuous_image by blast
      show "path_image (f ∘ g) ⊆ S"
        by (metis ‹path_image g ⊆ U› fim image_mono path_image_compose subset_trans)
      show "pathstart (f ∘ g) = p a"
        by (simp add: feq pastg pathstart_compose)
    qed auto
    then show ?thesis
      by (metis ‹path g› ‹path_image g ⊆ U› comp_apply pafig pastg)
  qed
  have "∃l. ∀g h. path g ∧ path_image g ⊆ U ∧ pathstart g = z ∧ pathfinish g = y ∧
                  path h ∧ path_image h ⊆ C ∧ pathstart h = a ∧
                  (∀t ∈ {0..1}. p(h t) = f(g t))  ⟶ pathfinish h = l" for y
  proof -
    have "pathfinish h = pathfinish h'"
         if g: "path g" "path_image g ⊆ U" "pathstart g = z" "pathfinish g = y"
            and h: "path h" "path_image h ⊆ C" "pathstart h = a"
            and phg: "⋀t. t ∈ {0..1} ⟹ p(h t) = f(g t)"
            and g': "path g'" "path_image g' ⊆ U" "pathstart g' = z" "pathfinish g' = y"
            and h': "path h'" "path_image h' ⊆ C" "pathstart h' = a"
            and phg': "⋀t. t ∈ {0..1} ⟹ p(h' t) = f(g' t)"
         for g h g' h'
    proof -
      obtain q where "path q" and piq: "path_image q ⊆ C" and pastq: "pathstart q = a" and pafiq: "pathfinish q = a"
                 and homS: "homotopic_paths S (f ∘ g +++ reversepath g') (p ∘ q)"
        using g g' hom [of "g +++ reversepath g'"] by (auto simp:  subset_path_image_join)
              have papq: "path (p ∘ q)"
                using homS homotopic_paths_imp_path by blast
              have pipq: "path_image (p ∘ q) ⊆ S"
                using homS homotopic_paths_imp_subset by blast
      obtain q' where "path q'" "path_image q' ⊆ C"
                and "pathstart q' = pathstart q" "pathfinish q' = pathfinish q"
                and pq'_eq: "⋀t. t ∈ {0..1} ⟹ p (q' t) = (f ∘ g +++ reversepath g') t"
        using covering_space_lift_homotopic_path [OF cov homotopic_paths_sym [OF homS] ‹path q› piq refl refl]
        by auto
      have "q' t = (h ∘ op *R 2) t" if "0 ≤ t" "t ≤ 1/2" for t
      proof (rule covering_space_lift_unique [OF cov, of q' 0 "h ∘ op *R 2" "{0..1/2}" "f ∘ g ∘ op *R 2" t])
        show "q' 0 = (h ∘ op *R 2) 0"
          by (metis ‹pathstart q' = pathstart q› comp_def g h pastq pathstart_def pth_4(2))
        show "continuous_on {0..1/2} (f ∘ g ∘ op *R 2)"
          apply (intro continuous_intros continuous_on_compose continuous_on_path [OF ‹path g›] continuous_on_subset [OF contf])
          using g(2) path_image_def by fastforce+
        show "(f ∘ g ∘ op *R 2) ` {0..1/2} ⊆ S"
          using g(2) path_image_def fim by fastforce
        show "(h ∘ op *R 2) ` {0..1/2} ⊆ C"
          using h path_image_def by fastforce
        show "q' ` {0..1/2} ⊆ C"
          using ‹path_image q' ⊆ C› path_image_def by fastforce
        show "⋀x. x ∈ {0..1/2} ⟹ (f ∘ g ∘ op *R 2) x = p (q' x)"
          by (auto simp: joinpaths_def pq'_eq)
        show "⋀x. x ∈ {0..1/2} ⟹ (f ∘ g ∘ op *R 2) x = p ((h ∘ op *R 2) x)"
          by (simp add: phg)
        show "continuous_on {0..1/2} q'"
          by (simp add: continuous_on_path ‹path q'›)
        show "continuous_on {0..1/2} (h ∘ op *R 2)"
          apply (intro continuous_intros continuous_on_compose continuous_on_path [OF ‹path h›], force)
          done
      qed (use that in auto)
      moreover have "q' t = (reversepath h' ∘ (λt. 2 *R t - 1)) t" if "1/2 < t" "t ≤ 1" for t
      proof (rule covering_space_lift_unique [OF cov, of q' 1 "reversepath h' ∘ (λt. 2 *R t - 1)" "{1/2<..1}" "f ∘ reversepath g' ∘ (λt. 2 *R t - 1)" t])
        show "q' 1 = (reversepath h' ∘ (λt. 2 *R t - 1)) 1"
          using h' ‹pathfinish q' = pathfinish q› pafiq
          by (simp add: pathstart_def pathfinish_def reversepath_def)
        show "continuous_on {1/2<..1} (f ∘ reversepath g' ∘ (λt. 2 *R t - 1))"
          apply (intro continuous_intros continuous_on_compose continuous_on_path ‹path g'› continuous_on_subset [OF contf])
          using g' apply simp_all
          by (auto simp: path_image_def reversepath_def)
        show "(f ∘ reversepath g' ∘ (λt. 2 *R t - 1)) ` {1/2<..1} ⊆ S"
          using g'(2) path_image_def fim by (auto simp: image_subset_iff path_image_def reversepath_def)
        show "q' ` {1/2<..1} ⊆ C"
          using ‹path_image q' ⊆ C› path_image_def by fastforce
        show "(reversepath h' ∘ (λt. 2 *R t - 1)) ` {1/2<..1} ⊆ C"
          using h' by (simp add: path_image_def reversepath_def subset_eq)
        show "⋀x. x ∈ {1/2<..1} ⟹ (f ∘ reversepath g' ∘ (λt. 2 *R t - 1)) x = p (q' x)"
          by (auto simp: joinpaths_def pq'_eq)
        show "⋀x. x ∈ {1/2<..1} ⟹
                  (f ∘ reversepath g' ∘ (λt. 2 *R t - 1)) x = p ((reversepath h' ∘ (λt. 2 *R t - 1)) x)"
          by (simp add: phg' reversepath_def)
        show "continuous_on {1/2<..1} q'"
          by (auto intro: continuous_on_path [OF ‹path q'›])
        show "continuous_on {1/2<..1} (reversepath h' ∘ (λt. 2 *R t - 1))"
          apply (intro continuous_intros continuous_on_compose continuous_on_path ‹path h'›)
          using h' apply auto
          done
      qed (use that in auto)
      ultimately have "q' t = (h +++ reversepath h') t" if "0 ≤ t" "t ≤ 1" for t
        using that by (simp add: joinpaths_def)
      then have "path(h +++ reversepath h')"
        by (auto intro: path_eq [OF ‹path q'›])
      then show ?thesis
        by (auto simp: ‹path h› ‹path h'›)
    qed
    then show ?thesis by metis
  qed
  then obtain l :: "'c ⇒ 'a"
          where l: "⋀y g h. ⟦path g; path_image g ⊆ U; pathstart g = z; pathfinish g = y;
                             path h; path_image h ⊆ C; pathstart h = a;
                             ⋀t. t ∈ {0..1} ⟹ p(h t) = f(g t)⟧ ⟹ pathfinish h = l y"
    by metis
  show ?thesis
  proof
    show pleq: "p (l y) = f y" if "y ∈ U" for y
      using*[OF ‹y ∈ U›]  by (metis l atLeastAtMost_iff order_refl pathfinish_def zero_le_one)
    show "l z = a"
      using l [of "linepath z z" z "linepath a a"] by (auto simp: assms)
    show LC: "l ` U ⊆ C"
      by (clarify dest!: *) (metis (full_types) l pathfinish_in_path_image subsetCE)
    have "∃T. openin (subtopology euclidean U) T ∧ y ∈ T ∧ T ⊆ {x ∈ U. l x ∈ X}"
         if X: "openin (subtopology euclidean C) X" and "y ∈ U" "l y ∈ X" for X y
    proof -
      have "X ⊆ C"
        using X openin_euclidean_subtopology_iff by blast
      have "f y ∈ S"
        using fim ‹y ∈ U› by blast
      then obtain W 𝒱
              where WV: "f y ∈ W ∧ openin (subtopology euclidean S) W ∧
                         (⋃𝒱 = {x. x ∈ C ∧ p x ∈ W} ∧
                          (∀U ∈ 𝒱. openin (subtopology euclidean C) U) ∧
                          pairwise disjnt 𝒱 ∧
                          (∀U ∈ 𝒱. ∃q. homeomorphism U W p q))"
        using cov by (force simp: covering_space_def)
      then have "l y ∈ ⋃𝒱"
        using ‹X ⊆ C› pleq that by auto
      then obtain W' where "l y ∈ W'" and "W' ∈ 𝒱"
        by blast
      with WV obtain p' where opeCW': "openin (subtopology euclidean C) W'"
                          and homUW': "homeomorphism W' W p p'"
        by blast
      then have contp': "continuous_on W p'" and p'im: "p' ` W ⊆ W'"
        using homUW' homeomorphism_image2 homeomorphism_cont2 by fastforce+
      obtain V where "y ∈ V" "y ∈ U" and fimW: "f ` V ⊆ W" "V ⊆ U"
                 and "path_connected V" and opeUV: "openin (subtopology euclidean U) V"
      proof -
        have "openin (subtopology euclidean U) {c ∈ U. f c ∈ W}"
          using WV contf continuous_on_open_gen fim by auto
        then show ?thesis
          using U WV
          apply (auto simp: locally_path_connected)
          apply (drule_tac x="{x. x ∈ U ∧ f x ∈ W}" in spec)
          apply (drule_tac x=y in spec)
          apply (auto simp: ‹y ∈ U› intro: that)
          done
      qed
      have "W' ⊆ C" "W ⊆ S"
        using opeCW' WV openin_imp_subset by auto
      have p'im: "p' ` W ⊆ W'"
        using homUW' homeomorphism_image2 by fastforce
      show ?thesis
      proof (intro exI conjI)
        have "openin (subtopology euclidean S) {x ∈ W. p' x ∈ W' ∩ X}"
        proof (rule openin_trans)
          show "openin (subtopology euclidean W) {x ∈ W. p' x ∈ W' ∩ X}"
            apply (rule continuous_openin_preimage [OF contp' p'im])
            using X ‹W' ⊆ C› apply (auto simp: openin_open)
            done
          show "openin (subtopology euclidean S) W"
            using WV by blast
        qed
        then show "openin (subtopology euclidean U) (V ∩ {x. x ∈ U ∧ f x ∈ {x. x ∈ W ∧ p' x ∈ W' ∩ X}})"
          by (intro openin_Int opeUV continuous_openin_preimage [OF contf fim])
        have "p' (f y) ∈ X"
          using ‹l y ∈ W'› homeomorphism_apply1 [OF homUW'] pleq ‹y ∈ U› ‹l y ∈ X› by fastforce
        then show "y ∈ V ∩ {x ∈ U. f x ∈ {x ∈ W. p' x ∈ W' ∩ X}}"
          using ‹y ∈ U› ‹y ∈ V› WV p'im by auto
        show "V ∩ {x ∈ U. f x ∈ {x ∈ W. p' x ∈ W' ∩ X}} ⊆ {x ∈ U. l x ∈ X}"
        proof clarsimp
          fix y'
          assume y': "y' ∈ V" "y' ∈ U" "f y' ∈ W" "p' (f y') ∈ W'" "p' (f y') ∈ X"
          then obtain γ where "path γ" "path_image γ ⊆ V" "pathstart γ = y" "pathfinish γ = y'"
            by (meson ‹path_connected V› ‹y ∈ V› path_connected_def)
          obtain pp qq where "path pp" "path_image pp ⊆ U"
                             "pathstart pp = z" "pathfinish pp = y"
                             "path qq" "path_image qq ⊆ C" "pathstart qq = a"
                         and pqqeq: "⋀t. t ∈ {0..1} ⟹ p(qq t) = f(pp t)"
            using*[OF ‹y ∈ U›] by blast
          have finW: "⋀x. ⟦0 ≤ x; x ≤ 1⟧ ⟹ f (γ x) ∈ W"
            using ‹path_image γ ⊆ V› by (auto simp: image_subset_iff path_image_def fimW [THEN subsetD])
          have "pathfinish (qq +++ (p' ∘ f ∘ γ)) = l y'"
          proof (rule l [of "pp +++ γ" y' "qq +++ (p' ∘ f ∘ γ)" ])
            show "path (pp +++ γ)"
              by (simp add: ‹path γ› ‹path pp› ‹pathfinish pp = y› ‹pathstart γ = y›)
            show "path_image (pp +++ γ) ⊆ U"
              using ‹V ⊆ U› ‹path_image γ ⊆ V› ‹path_image pp ⊆ U› not_in_path_image_join by blast
            show "pathstart (pp +++ γ) = z"
              by (simp add: ‹pathstart pp = z›)
            show "pathfinish (pp +++ γ) = y'"
              by (simp add: ‹pathfinish γ = y'›)
            have paqq: "pathfinish qq = pathstart (p' ∘ f ∘ γ)"
              apply (simp add: ‹pathstart γ = y› pathstart_compose)
              apply (metis (mono_tags, lifting) ‹l y ∈ W'› ‹path pp› ‹path qq› ‹path_image pp ⊆ U› ‹path_image qq ⊆ C›
                           ‹pathfinish pp = y› ‹pathstart pp = z› ‹pathstart qq = a›
                           homeomorphism_apply1 [OF homUW'] l pleq pqqeq ‹y ∈ U›)
              done
            have "continuous_on (path_image γ) (p' ∘ f)"
            proof (rule continuous_on_compose)
              show "continuous_on (path_image γ) f"
                using ‹path_image γ ⊆ V› ‹V ⊆ U› contf continuous_on_subset by blast
              show "continuous_on (f ` path_image γ) p'"
                apply (rule continuous_on_subset [OF contp'])
                apply (auto simp: path_image_def pathfinish_def pathstart_def finW)
                done
            qed
            then show "path (qq +++ (p' ∘ f ∘ γ))"
              using ‹path γ› ‹path qq› paqq path_continuous_image path_join_imp by blast
            show "path_image (qq +++ (p' ∘ f ∘ γ)) ⊆ C"
              apply (rule subset_path_image_join)
               apply (simp add: ‹path_image qq ⊆ C›)
              by (metis ‹W' ⊆ C› ‹path_image γ ⊆ V› dual_order.trans fimW(1) image_comp image_mono p'im path_image_compose)
            show "pathstart (qq +++ (p' ∘ f ∘ γ)) = a"
              by (simp add: ‹pathstart qq = a›)
            show "p ((qq +++ (p' ∘ f ∘ γ)) ξ) = f ((pp +++ γ) ξ)" if ξ: "ξ ∈ {0..1}" for ξ
            proof (simp add: joinpaths_def, safe)
              show "p (qq (2*ξ)) = f (pp (2*ξ))" if "ξ*2 ≤ 1"
                using ‹ξ ∈ {0..1}› pqqeq that by auto
              show "p (p' (f (γ (2*ξ - 1)))) = f (γ (2*ξ - 1))" if "¬ ξ*2 ≤ 1"
                apply (rule homeomorphism_apply2 [OF homUW' finW])
                using that ξ by auto
            qed
          qed
          with ‹pathfinish γ = y'›  ‹p' (f y') ∈ X› show "l y' ∈ X"
            unfolding pathfinish_join by (simp add: pathfinish_def)
        qed
      qed
    qed
    then show "continuous_on U l"
      using openin_subopen continuous_on_open_gen [OF LC]
      by (metis (no_types, lifting) mem_Collect_eq)
  qed
qed


corollary covering_space_lift_stronger:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
    and f :: "'c::real_normed_vector ⇒ 'b"
  assumes cov: "covering_space C p S" "a ∈ C" "z ∈ U"
      and U: "path_connected U" "locally path_connected U"
      and contf: "continuous_on U f" and fim: "f ` U ⊆ S"
      and feq: "f z = p a"
      and hom: "⋀r. ⟦path r; path_image r ⊆ U; pathstart r = z; pathfinish r = z⟧
                     ⟹ ∃b. homotopic_paths S (f ∘ r) (linepath b b)"
  obtains g where "continuous_on U g" "g ` U ⊆ C" "g z = a" "⋀y. y ∈ U ⟹ p(g y) = f y"
proof (rule covering_space_lift_general [OF cov U contf fim feq])
  fix r
  assume "path r" "path_image r ⊆ U" "pathstart r = z" "pathfinish r = z"
  then obtain b where b: "homotopic_paths S (f ∘ r) (linepath b b)"
    using hom by blast
  then have "f (pathstart r) = b"
    by (metis homotopic_paths_imp_pathstart pathstart_compose pathstart_linepath)
  then have "homotopic_paths S (f ∘ r) (linepath (f z) (f z))"
    by (simp add: b ‹pathstart r = z›)
  then have "homotopic_paths S (f ∘ r) (p ∘ linepath a a)"
    by (simp add: o_def feq linepath_def)
  then show "∃q. path q ∧
                  path_image q ⊆ C ∧
                  pathstart q = a ∧ pathfinish q = a ∧ homotopic_paths S (f ∘ r) (p ∘ q)"
    by (force simp: ‹a ∈ C›)
qed auto

corollary covering_space_lift_strong:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
    and f :: "'c::real_normed_vector ⇒ 'b"
  assumes cov: "covering_space C p S" "a ∈ C" "z ∈ U"
      and scU: "simply_connected U" and lpcU: "locally path_connected U"
      and contf: "continuous_on U f" and fim: "f ` U ⊆ S"
      and feq: "f z = p a"
  obtains g where "continuous_on U g" "g ` U ⊆ C" "g z = a" "⋀y. y ∈ U ⟹ p(g y) = f y"
proof (rule covering_space_lift_stronger [OF cov _ lpcU contf fim feq])
  show "path_connected U"
    using scU simply_connected_eq_contractible_loop_some by blast
  fix r
  assume r: "path r" "path_image r ⊆ U" "pathstart r = z" "pathfinish r = z"
  have "linepath (f z) (f z) = f ∘ linepath z z"
    by (simp add: o_def linepath_def)
  then have "homotopic_paths S (f ∘ r) (linepath (f z) (f z))"
    by (metis r contf fim homotopic_paths_continuous_image scU simply_connected_eq_contractible_path)
  then show "∃b. homotopic_paths S (f ∘ r) (linepath b b)"
    by blast
qed blast

corollary covering_space_lift:
  fixes p :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
    and f :: "'c::real_normed_vector ⇒ 'b"
  assumes cov: "covering_space C p S"
      and U: "simply_connected U"  "locally path_connected U"
      and contf: "continuous_on U f" and fim: "f ` U ⊆ S"
    obtains g where "continuous_on U g" "g ` U ⊆ C" "⋀y. y ∈ U ⟹ p(g y) = f y"
proof (cases "U = {}")
  case True
  with that show ?thesis by auto
next
  case False
  then obtain z where "z ∈ U" by blast
  then obtain a where "a ∈ C" "f z = p a"
    by (metis cov covering_space_imp_surjective fim image_iff image_subset_iff)
  then show ?thesis
    by (metis that covering_space_lift_strong [OF cov _ ‹z ∈ U› U contf fim])
qed

end