src/HOL/Analysis/Homeomorphism.thy
 author nipkow Sat Dec 29 15:43:53 2018 +0100 (6 months ago) changeset 69529 4ab9657b3257 parent 69508 2a4c8a2a3f8e child 69620 19d8a59481db permissions -rw-r--r--
capitalize proper names in lemma names
```     1 (*  Title:      HOL/Analysis/Homeomorphism.thy
```
```     2     Author: LC Paulson (ported from HOL Light)
```
```     3 *)
```
```     4
```
```     5 section%important \<open>Homeomorphism Theorems\<close>
```
```     6
```
```     7 theory Homeomorphism
```
```     8 imports Path_Connected
```
```     9 begin
```
```    10
```
```    11 lemma%unimportant homeomorphic_spheres':
```
```    12   fixes a ::"'a::euclidean_space" and b ::"'b::euclidean_space"
```
```    13   assumes "0 < \<delta>" and dimeq: "DIM('a) = DIM('b)"
```
```    14   shows "(sphere a \<delta>) homeomorphic (sphere b \<delta>)"
```
```    15 proof -
```
```    16   obtain f :: "'a\<Rightarrow>'b" and g where "linear f" "linear g"
```
```    17      and fg: "\<And>x. norm(f x) = norm x" "\<And>y. norm(g y) = norm y" "\<And>x. g(f x) = x" "\<And>y. f(g y) = y"
```
```    18     by (blast intro: isomorphisms_UNIV_UNIV [OF dimeq])
```
```    19   then have "continuous_on UNIV f" "continuous_on UNIV g"
```
```    20     using linear_continuous_on linear_linear by blast+
```
```    21   then show ?thesis
```
```    22     unfolding homeomorphic_minimal
```
```    23     apply(rule_tac x="\<lambda>x. b + f(x - a)" in exI)
```
```    24     apply(rule_tac x="\<lambda>x. a + g(x - b)" in exI)
```
```    25     using assms
```
```    26     apply (force intro: continuous_intros
```
```    27                   continuous_on_compose2 [of _ f] continuous_on_compose2 [of _ g] simp: dist_commute dist_norm fg)
```
```    28     done
```
```    29 qed
```
```    30
```
```    31 lemma%unimportant homeomorphic_spheres_gen:
```
```    32     fixes a :: "'a::euclidean_space" and b :: "'b::euclidean_space"
```
```    33   assumes "0 < r" "0 < s" "DIM('a::euclidean_space) = DIM('b::euclidean_space)"
```
```    34   shows "(sphere a r homeomorphic sphere b s)"
```
```    35   apply (rule homeomorphic_trans [OF homeomorphic_spheres homeomorphic_spheres'])
```
```    36   using assms  apply auto
```
```    37   done
```
```    38
```
```    39 subsection%important \<open>Homeomorphism of all convex compact sets with nonempty interior\<close>
```
```    40
```
```    41 proposition%important ray_to_rel_frontier:
```
```    42   fixes a :: "'a::real_inner"
```
```    43   assumes "bounded S"
```
```    44       and a: "a \<in> rel_interior S"
```
```    45       and aff: "(a + l) \<in> affine hull S"
```
```    46       and "l \<noteq> 0"
```
```    47   obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> rel_frontier S"
```
```    48            "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> rel_interior S"
```
```    49 proof%unimportant -
```
```    50   have aaff: "a \<in> affine hull S"
```
```    51     by (meson a hull_subset rel_interior_subset rev_subsetD)
```
```    52   let ?D = "{d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}"
```
```    53   obtain B where "B > 0" and B: "S \<subseteq> ball a B"
```
```    54     using bounded_subset_ballD [OF \<open>bounded S\<close>] by blast
```
```    55   have "a + (B / norm l) *\<^sub>R l \<notin> ball a B"
```
```    56     by (simp add: dist_norm \<open>l \<noteq> 0\<close>)
```
```    57   with B have "a + (B / norm l) *\<^sub>R l \<notin> rel_interior S"
```
```    58     using rel_interior_subset subsetCE by blast
```
```    59   with \<open>B > 0\<close> \<open>l \<noteq> 0\<close> have nonMT: "?D \<noteq> {}"
```
```    60     using divide_pos_pos zero_less_norm_iff by fastforce
```
```    61   have bdd: "bdd_below ?D"
```
```    62     by (metis (no_types, lifting) bdd_belowI le_less mem_Collect_eq)
```
```    63   have relin_Ex: "\<And>x. x \<in> rel_interior S \<Longrightarrow>
```
```    64                     \<exists>e>0. \<forall>x'\<in>affine hull S. dist x' x < e \<longrightarrow> x' \<in> rel_interior S"
```
```    65     using openin_rel_interior [of S] by (simp add: openin_euclidean_subtopology_iff)
```
```    66   define d where "d = Inf ?D"
```
```    67   obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "\<And>\<eta>. \<lbrakk>0 \<le> \<eta>; \<eta> < \<epsilon>\<rbrakk> \<Longrightarrow> (a + \<eta> *\<^sub>R l) \<in> rel_interior S"
```
```    68   proof -
```
```    69     obtain e where "e>0"
```
```    70             and e: "\<And>x'. x' \<in> affine hull S \<Longrightarrow> dist x' a < e \<Longrightarrow> x' \<in> rel_interior S"
```
```    71       using relin_Ex a by blast
```
```    72     show thesis
```
```    73     proof (rule_tac \<epsilon> = "e / norm l" in that)
```
```    74       show "0 < e / norm l" by (simp add: \<open>0 < e\<close> \<open>l \<noteq> 0\<close>)
```
```    75     next
```
```    76       show "a + \<eta> *\<^sub>R l \<in> rel_interior S" if "0 \<le> \<eta>" "\<eta> < e / norm l" for \<eta>
```
```    77       proof (rule e)
```
```    78         show "a + \<eta> *\<^sub>R l \<in> affine hull S"
```
```    79           by (metis (no_types) add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff)
```
```    80         show "dist (a + \<eta> *\<^sub>R l) a < e"
```
```    81           using that by (simp add: \<open>l \<noteq> 0\<close> dist_norm pos_less_divide_eq)
```
```    82       qed
```
```    83     qed
```
```    84   qed
```
```    85   have inint: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> a + e *\<^sub>R l \<in> rel_interior S"
```
```    86     unfolding d_def using cInf_lower [OF _ bdd]
```
```    87     by (metis (no_types, lifting) a add.right_neutral le_less mem_Collect_eq not_less real_vector.scale_zero_left)
```
```    88   have "\<epsilon> \<le> d"
```
```    89     unfolding d_def
```
```    90     apply (rule cInf_greatest [OF nonMT])
```
```    91     using \<epsilon> dual_order.strict_implies_order le_less_linear by blast
```
```    92   with \<open>0 < \<epsilon>\<close> have "0 < d" by simp
```
```    93   have "a + d *\<^sub>R l \<notin> rel_interior S"
```
```    94   proof
```
```    95     assume adl: "a + d *\<^sub>R l \<in> rel_interior S"
```
```    96     obtain e where "e > 0"
```
```    97              and e: "\<And>x'. x' \<in> affine hull S \<Longrightarrow> dist x' (a + d *\<^sub>R l) < e \<Longrightarrow> x' \<in> rel_interior S"
```
```    98       using relin_Ex adl by blast
```
```    99     have "d + e / norm l \<le> Inf {d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}"
```
```   100     proof (rule cInf_greatest [OF nonMT], clarsimp)
```
```   101       fix x::real
```
```   102       assume "0 < x" and nonrel: "a + x *\<^sub>R l \<notin> rel_interior S"
```
```   103       show "d + e / norm l \<le> x"
```
```   104       proof (cases "x < d")
```
```   105         case True with inint nonrel \<open>0 < x\<close>
```
```   106           show ?thesis by auto
```
```   107       next
```
```   108         case False
```
```   109           then have dle: "x < d + e / norm l \<Longrightarrow> dist (a + x *\<^sub>R l) (a + d *\<^sub>R l) < e"
```
```   110             by (simp add: field_simps \<open>l \<noteq> 0\<close>)
```
```   111           have ain: "a + x *\<^sub>R l \<in> affine hull S"
```
```   112             by (metis add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff)
```
```   113           show ?thesis
```
```   114             using e [OF ain] nonrel dle by force
```
```   115       qed
```
```   116     qed
```
```   117     then show False
```
```   118       using \<open>0 < e\<close> \<open>l \<noteq> 0\<close> by (simp add: d_def [symmetric] divide_simps)
```
```   119   qed
```
```   120   moreover have "a + d *\<^sub>R l \<in> closure S"
```
```   121   proof (clarsimp simp: closure_approachable)
```
```   122     fix \<eta>::real assume "0 < \<eta>"
```
```   123     have 1: "a + (d - min d (\<eta> / 2 / norm l)) *\<^sub>R l \<in> S"
```
```   124       apply (rule subsetD [OF rel_interior_subset inint])
```
```   125       using \<open>l \<noteq> 0\<close> \<open>0 < d\<close> \<open>0 < \<eta>\<close> by auto
```
```   126     have "norm l * min d (\<eta> / (norm l * 2)) \<le> norm l * (\<eta> / (norm l * 2))"
```
```   127       by (metis min_def mult_left_mono norm_ge_zero order_refl)
```
```   128     also have "... < \<eta>"
```
```   129       using \<open>l \<noteq> 0\<close> \<open>0 < \<eta>\<close> by (simp add: divide_simps)
```
```   130     finally have 2: "norm l * min d (\<eta> / (norm l * 2)) < \<eta>" .
```
```   131     show "\<exists>y\<in>S. dist y (a + d *\<^sub>R l) < \<eta>"
```
```   132       apply (rule_tac x="a + (d - min d (\<eta> / 2 / norm l)) *\<^sub>R l" in bexI)
```
```   133       using 1 2 \<open>0 < d\<close> \<open>0 < \<eta>\<close> apply (auto simp: algebra_simps)
```
```   134       done
```
```   135   qed
```
```   136   ultimately have infront: "a + d *\<^sub>R l \<in> rel_frontier S"
```
```   137     by (simp add: rel_frontier_def)
```
```   138   show ?thesis
```
```   139     by (rule that [OF \<open>0 < d\<close> infront inint])
```
```   140 qed
```
```   141
```
```   142 corollary%important ray_to_frontier:
```
```   143   fixes a :: "'a::euclidean_space"
```
```   144   assumes "bounded S"
```
```   145       and a: "a \<in> interior S"
```
```   146       and "l \<noteq> 0"
```
```   147   obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> frontier S"
```
```   148            "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> interior S"
```
```   149 proof%unimportant -
```
```   150   have "interior S = rel_interior S"
```
```   151     using a rel_interior_nonempty_interior by auto
```
```   152   then have "a \<in> rel_interior S"
```
```   153     using a by simp
```
```   154   then show ?thesis
```
```   155     apply (rule ray_to_rel_frontier [OF \<open>bounded S\<close> _ _ \<open>l \<noteq> 0\<close>])
```
```   156      using a affine_hull_nonempty_interior apply blast
```
```   157     by (simp add: \<open>interior S = rel_interior S\<close> frontier_def rel_frontier_def that)
```
```   158 qed
```
```   159
```
```   160
```
```   161 lemma%unimportant segment_to_rel_frontier_aux:
```
```   162   fixes x :: "'a::euclidean_space"
```
```   163   assumes "convex S" "bounded S" and x: "x \<in> rel_interior S" and y: "y \<in> S" and xy: "x \<noteq> y"
```
```   164   obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z"
```
```   165                    "open_segment x z \<subseteq> rel_interior S"
```
```   166 proof -
```
```   167   have "x + (y - x) \<in> affine hull S"
```
```   168     using hull_inc [OF y] by auto
```
```   169   then obtain d where "0 < d" and df: "(x + d *\<^sub>R (y-x)) \<in> rel_frontier S"
```
```   170                   and di: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (x + e *\<^sub>R (y-x)) \<in> rel_interior S"
```
```   171     by (rule ray_to_rel_frontier [OF \<open>bounded S\<close> x]) (use xy in auto)
```
```   172   show ?thesis
```
```   173   proof
```
```   174     show "x + d *\<^sub>R (y - x) \<in> rel_frontier S"
```
```   175       by (simp add: df)
```
```   176   next
```
```   177     have "open_segment x y \<subseteq> rel_interior S"
```
```   178       using rel_interior_closure_convex_segment [OF \<open>convex S\<close> x] closure_subset y by blast
```
```   179     moreover have "x + d *\<^sub>R (y - x) \<in> open_segment x y" if "d < 1"
```
```   180       using xy
```
```   181       apply (auto simp: in_segment)
```
```   182       apply (rule_tac x="d" in exI)
```
```   183       using \<open>0 < d\<close> that apply (auto simp: divide_simps algebra_simps)
```
```   184       done
```
```   185     ultimately have "1 \<le> d"
```
```   186       using df rel_frontier_def by fastforce
```
```   187     moreover have "x = (1 / d) *\<^sub>R x + ((d - 1) / d) *\<^sub>R x"
```
```   188       by (metis \<open>0 < d\<close> add.commute add_divide_distrib diff_add_cancel divide_self_if less_irrefl scaleR_add_left scaleR_one)
```
```   189     ultimately show "y \<in> closed_segment x (x + d *\<^sub>R (y - x))"
```
```   190       apply (auto simp: in_segment)
```
```   191       apply (rule_tac x="1/d" in exI)
```
```   192       apply (auto simp: divide_simps algebra_simps)
```
```   193       done
```
```   194   next
```
```   195     show "open_segment x (x + d *\<^sub>R (y - x)) \<subseteq> rel_interior S"
```
```   196       apply (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> x])
```
```   197       using df rel_frontier_def by auto
```
```   198   qed
```
```   199 qed
```
```   200
```
```   201 lemma%unimportant segment_to_rel_frontier:
```
```   202   fixes x :: "'a::euclidean_space"
```
```   203   assumes S: "convex S" "bounded S" and x: "x \<in> rel_interior S"
```
```   204       and y: "y \<in> S" and xy: "\<not>(x = y \<and> S = {x})"
```
```   205   obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z"
```
```   206                   "open_segment x z \<subseteq> rel_interior S"
```
```   207 proof (cases "x=y")
```
```   208   case True
```
```   209   with xy have "S \<noteq> {x}"
```
```   210     by blast
```
```   211   with True show ?thesis
```
```   212     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)
```
```   213 next
```
```   214   case False
```
```   215   then show ?thesis
```
```   216     using segment_to_rel_frontier_aux [OF S x y] that by blast
```
```   217 qed
```
```   218
```
```   219 proposition%important rel_frontier_not_sing:
```
```   220   fixes a :: "'a::euclidean_space"
```
```   221   assumes "bounded S"
```
```   222     shows "rel_frontier S \<noteq> {a}"
```
```   223 proof%unimportant (cases "S = {}")
```
```   224   case True  then show ?thesis  by simp
```
```   225 next
```
```   226   case False
```
```   227   then obtain z where "z \<in> S"
```
```   228     by blast
```
```   229   then show ?thesis
```
```   230   proof (cases "S = {z}")
```
```   231     case True then show ?thesis  by simp
```
```   232   next
```
```   233     case False
```
```   234     then obtain w where "w \<in> S" "w \<noteq> z"
```
```   235       using \<open>z \<in> S\<close> by blast
```
```   236     show ?thesis
```
```   237     proof
```
```   238       assume "rel_frontier S = {a}"
```
```   239       then consider "w \<notin> rel_frontier S" | "z \<notin> rel_frontier S"
```
```   240         using \<open>w \<noteq> z\<close> by auto
```
```   241       then show False
```
```   242       proof cases
```
```   243         case 1
```
```   244         then have w: "w \<in> rel_interior S"
```
```   245           using \<open>w \<in> S\<close> closure_subset rel_frontier_def by fastforce
```
```   246         have "w + (w - z) \<in> affine hull S"
```
```   247           by (metis \<open>w \<in> S\<close> \<open>z \<in> S\<close> affine_affine_hull hull_inc mem_affine_3_minus scaleR_one)
```
```   248         then obtain e where "0 < e" "(w + e *\<^sub>R (w - z)) \<in> rel_frontier S"
```
```   249           using \<open>w \<noteq> z\<close>  \<open>z \<in> S\<close> by (metis assms ray_to_rel_frontier right_minus_eq w)
```
```   250         moreover obtain d where "0 < d" "(w + d *\<^sub>R (z - w)) \<in> rel_frontier S"
```
```   251           using ray_to_rel_frontier [OF \<open>bounded S\<close> w, of "1 *\<^sub>R (z - w)"]  \<open>w \<noteq> z\<close>  \<open>z \<in> S\<close>
```
```   252           by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one)
```
```   253         ultimately have "d *\<^sub>R (z - w) = e *\<^sub>R (w - z)"
```
```   254           using \<open>rel_frontier S = {a}\<close> by force
```
```   255         moreover have "e \<noteq> -d "
```
```   256           using \<open>0 < e\<close> \<open>0 < d\<close> by force
```
```   257         ultimately show False
```
```   258           by (metis (no_types, lifting) \<open>w \<noteq> z\<close> eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus)
```
```   259       next
```
```   260         case 2
```
```   261         then have z: "z \<in> rel_interior S"
```
```   262           using \<open>z \<in> S\<close> closure_subset rel_frontier_def by fastforce
```
```   263         have "z + (z - w) \<in> affine hull S"
```
```   264           by (metis \<open>z \<in> S\<close> \<open>w \<in> S\<close> affine_affine_hull hull_inc mem_affine_3_minus scaleR_one)
```
```   265         then obtain e where "0 < e" "(z + e *\<^sub>R (z - w)) \<in> rel_frontier S"
```
```   266           using \<open>w \<noteq> z\<close>  \<open>w \<in> S\<close> by (metis assms ray_to_rel_frontier right_minus_eq z)
```
```   267         moreover obtain d where "0 < d" "(z + d *\<^sub>R (w - z)) \<in> rel_frontier S"
```
```   268           using ray_to_rel_frontier [OF \<open>bounded S\<close> z, of "1 *\<^sub>R (w - z)"]  \<open>w \<noteq> z\<close>  \<open>w \<in> S\<close>
```
```   269           by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one)
```
```   270         ultimately have "d *\<^sub>R (w - z) = e *\<^sub>R (z - w)"
```
```   271           using \<open>rel_frontier S = {a}\<close> by force
```
```   272         moreover have "e \<noteq> -d "
```
```   273           using \<open>0 < e\<close> \<open>0 < d\<close> by force
```
```   274         ultimately show False
```
```   275           by (metis (no_types, lifting) \<open>w \<noteq> z\<close> eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus)
```
```   276       qed
```
```   277     qed
```
```   278   qed
```
```   279 qed
```
```   280
```
```   281 proposition%important
```
```   282   fixes S :: "'a::euclidean_space set"
```
```   283   assumes "compact S" and 0: "0 \<in> rel_interior S"
```
```   284       and star: "\<And>x. x \<in> S \<Longrightarrow> open_segment 0 x \<subseteq> rel_interior S"
```
```   285     shows starlike_compact_projective1_0:
```
```   286             "S - rel_interior S homeomorphic sphere 0 1 \<inter> affine hull S"
```
```   287             (is "?SMINUS homeomorphic ?SPHER")
```
```   288       and starlike_compact_projective2_0:
```
```   289             "S homeomorphic cball 0 1 \<inter> affine hull S"
```
```   290             (is "S homeomorphic ?CBALL")
```
```   291 proof%unimportant -
```
```   292   have starI: "(u *\<^sub>R x) \<in> rel_interior S" if "x \<in> S" "0 \<le> u" "u < 1" for x u
```
```   293   proof (cases "x=0 \<or> u=0")
```
```   294     case True with 0 show ?thesis by force
```
```   295   next
```
```   296     case False with that show ?thesis
```
```   297       by (auto simp: in_segment intro: star [THEN subsetD])
```
```   298   qed
```
```   299   have "0 \<in> S"  using assms rel_interior_subset by auto
```
```   300   define proj where "proj \<equiv> \<lambda>x::'a. x /\<^sub>R norm x"
```
```   301   have eqI: "x = y" if "proj x = proj y" "norm x = norm y" for x y
```
```   302     using that  by (force simp: proj_def)
```
```   303   then have iff_eq: "\<And>x y. (proj x = proj y \<and> norm x = norm y) \<longleftrightarrow> x = y"
```
```   304     by blast
```
```   305   have projI: "x \<in> affine hull S \<Longrightarrow> proj x \<in> affine hull S" for x
```
```   306     by (metis \<open>0 \<in> S\<close> affine_hull_span_0 hull_inc span_mul proj_def)
```
```   307   have nproj1 [simp]: "x \<noteq> 0 \<Longrightarrow> norm(proj x) = 1" for x
```
```   308     by (simp add: proj_def)
```
```   309   have proj0_iff [simp]: "proj x = 0 \<longleftrightarrow> x = 0" for x
```
```   310     by (simp add: proj_def)
```
```   311   have cont_proj: "continuous_on (UNIV - {0}) proj"
```
```   312     unfolding proj_def by (rule continuous_intros | force)+
```
```   313   have proj_spherI: "\<And>x. \<lbrakk>x \<in> affine hull S; x \<noteq> 0\<rbrakk> \<Longrightarrow> proj x \<in> ?SPHER"
```
```   314     by (simp add: projI)
```
```   315   have "bounded S" "closed S"
```
```   316     using \<open>compact S\<close> compact_eq_bounded_closed by blast+
```
```   317   have inj_on_proj: "inj_on proj (S - rel_interior S)"
```
```   318   proof
```
```   319     fix x y
```
```   320     assume x: "x \<in> S - rel_interior S"
```
```   321        and y: "y \<in> S - rel_interior S" and eq: "proj x = proj y"
```
```   322     then have xynot: "x \<noteq> 0" "y \<noteq> 0" "x \<in> S" "y \<in> S" "x \<notin> rel_interior S" "y \<notin> rel_interior S"
```
```   323       using 0 by auto
```
```   324     consider "norm x = norm y" | "norm x < norm y" | "norm x > norm y" by linarith
```
```   325     then show "x = y"
```
```   326     proof cases
```
```   327       assume "norm x = norm y"
```
```   328         with iff_eq eq show "x = y" by blast
```
```   329     next
```
```   330       assume *: "norm x < norm y"
```
```   331       have "x /\<^sub>R norm x = norm x *\<^sub>R (x /\<^sub>R norm x) /\<^sub>R norm (norm x *\<^sub>R (x /\<^sub>R norm x))"
```
```   332         by force
```
```   333       then have "proj ((norm x / norm y) *\<^sub>R y) = proj x"
```
```   334         by (metis (no_types) divide_inverse local.proj_def eq scaleR_scaleR)
```
```   335       then have [simp]: "(norm x / norm y) *\<^sub>R y = x"
```
```   336         by (rule eqI) (simp add: \<open>y \<noteq> 0\<close>)
```
```   337       have no: "0 \<le> norm x / norm y" "norm x / norm y < 1"
```
```   338         using * by (auto simp: divide_simps)
```
```   339       then show "x = y"
```
```   340         using starI [OF \<open>y \<in> S\<close> no] xynot by auto
```
```   341     next
```
```   342       assume *: "norm x > norm y"
```
```   343       have "y /\<^sub>R norm y = norm y *\<^sub>R (y /\<^sub>R norm y) /\<^sub>R norm (norm y *\<^sub>R (y /\<^sub>R norm y))"
```
```   344         by force
```
```   345       then have "proj ((norm y / norm x) *\<^sub>R x) = proj y"
```
```   346         by (metis (no_types) divide_inverse local.proj_def eq scaleR_scaleR)
```
```   347       then have [simp]: "(norm y / norm x) *\<^sub>R x = y"
```
```   348         by (rule eqI) (simp add: \<open>x \<noteq> 0\<close>)
```
```   349       have no: "0 \<le> norm y / norm x" "norm y / norm x < 1"
```
```   350         using * by (auto simp: divide_simps)
```
```   351       then show "x = y"
```
```   352         using starI [OF \<open>x \<in> S\<close> no] xynot by auto
```
```   353     qed
```
```   354   qed
```
```   355   have "\<exists>surf. homeomorphism (S - rel_interior S) ?SPHER proj surf"
```
```   356   proof (rule homeomorphism_compact)
```
```   357     show "compact (S - rel_interior S)"
```
```   358        using \<open>compact S\<close> compact_rel_boundary by blast
```
```   359     show "continuous_on (S - rel_interior S) proj"
```
```   360       using 0 by (blast intro: continuous_on_subset [OF cont_proj])
```
```   361     show "proj ` (S - rel_interior S) = ?SPHER"
```
```   362     proof
```
```   363       show "proj ` (S - rel_interior S) \<subseteq> ?SPHER"
```
```   364         using 0 by (force simp: hull_inc projI intro: nproj1)
```
```   365       show "?SPHER \<subseteq> proj ` (S - rel_interior S)"
```
```   366       proof (clarsimp simp: proj_def)
```
```   367         fix x
```
```   368         assume "x \<in> affine hull S" and nox: "norm x = 1"
```
```   369         then have "x \<noteq> 0" by auto
```
```   370         obtain d where "0 < d" and dx: "(d *\<^sub>R x) \<in> rel_frontier S"
```
```   371                    and ri: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (e *\<^sub>R x) \<in> rel_interior S"
```
```   372           using ray_to_rel_frontier [OF \<open>bounded S\<close> 0] \<open>x \<in> affine hull S\<close> \<open>x \<noteq> 0\<close> by auto
```
```   373         show "x \<in> (\<lambda>x. x /\<^sub>R norm x) ` (S - rel_interior S)"
```
```   374           apply (rule_tac x="d *\<^sub>R x" in image_eqI)
```
```   375           using \<open>0 < d\<close>
```
```   376           using dx \<open>closed S\<close> apply (auto simp: rel_frontier_def divide_simps nox)
```
```   377           done
```
```   378       qed
```
```   379     qed
```
```   380   qed (rule inj_on_proj)
```
```   381   then obtain surf where surf: "homeomorphism (S - rel_interior S) ?SPHER proj surf"
```
```   382     by blast
```
```   383   then have cont_surf: "continuous_on (proj ` (S - rel_interior S)) surf"
```
```   384     by (auto simp: homeomorphism_def)
```
```   385   have surf_nz: "\<And>x. x \<in> ?SPHER \<Longrightarrow> surf x \<noteq> 0"
```
```   386     by (metis "0" DiffE homeomorphism_def imageI surf)
```
```   387   have cont_nosp: "continuous_on (?SPHER) (\<lambda>x. norm x *\<^sub>R ((surf o proj) x))"
```
```   388     apply (rule continuous_intros)+
```
```   389     apply (rule continuous_on_subset [OF cont_proj], force)
```
```   390     apply (rule continuous_on_subset [OF cont_surf])
```
```   391     apply (force simp: homeomorphism_image1 [OF surf] dest: proj_spherI)
```
```   392     done
```
```   393   have surfpS: "\<And>x. \<lbrakk>norm x = 1; x \<in> affine hull S\<rbrakk> \<Longrightarrow> surf (proj x) \<in> S"
```
```   394     by (metis (full_types) DiffE \<open>0 \<in> S\<close> homeomorphism_def image_eqI norm_zero proj_spherI real_vector.scale_zero_left scaleR_one surf)
```
```   395   have *: "\<exists>y. norm y = 1 \<and> y \<in> affine hull S \<and> x = surf (proj y)"
```
```   396           if "x \<in> S" "x \<notin> rel_interior S" for x
```
```   397   proof -
```
```   398     have "proj x \<in> ?SPHER"
```
```   399       by (metis (full_types) "0" hull_inc proj_spherI that)
```
```   400     moreover have "surf (proj x) = x"
```
```   401       by (metis Diff_iff homeomorphism_def surf that)
```
```   402     ultimately show ?thesis
```
```   403       by (metis \<open>\<And>x. x \<in> ?SPHER \<Longrightarrow> surf x \<noteq> 0\<close> hull_inc inverse_1 local.proj_def norm_sgn projI scaleR_one sgn_div_norm that(1))
```
```   404   qed
```
```   405   have surfp_notin: "\<And>x. \<lbrakk>norm x = 1; x \<in> affine hull S\<rbrakk> \<Longrightarrow> surf (proj x) \<notin> rel_interior S"
```
```   406     by (metis (full_types) DiffE one_neq_zero homeomorphism_def image_eqI norm_zero proj_spherI surf)
```
```   407   have no_sp_im: "(\<lambda>x. norm x *\<^sub>R surf (proj x)) ` (?SPHER) = S - rel_interior S"
```
```   408     by (auto simp: surfpS image_def Bex_def surfp_notin *)
```
```   409   have inj_spher: "inj_on (\<lambda>x. norm x *\<^sub>R surf (proj x)) ?SPHER"
```
```   410   proof
```
```   411     fix x y
```
```   412     assume xy: "x \<in> ?SPHER" "y \<in> ?SPHER"
```
```   413        and eq: " norm x *\<^sub>R surf (proj x) = norm y *\<^sub>R surf (proj y)"
```
```   414     then have "norm x = 1" "norm y = 1" "x \<in> affine hull S" "y \<in> affine hull S"
```
```   415       using 0 by auto
```
```   416     with eq show "x = y"
```
```   417       by (simp add: proj_def) (metis surf xy homeomorphism_def)
```
```   418   qed
```
```   419   have co01: "compact ?SPHER"
```
```   420     by (simp add: closed_affine_hull compact_Int_closed)
```
```   421   show "?SMINUS homeomorphic ?SPHER"
```
```   422     apply (subst homeomorphic_sym)
```
```   423     apply (rule homeomorphic_compact [OF co01 cont_nosp [unfolded o_def] no_sp_im inj_spher])
```
```   424     done
```
```   425   have proj_scaleR: "\<And>a x. 0 < a \<Longrightarrow> proj (a *\<^sub>R x) = proj x"
```
```   426     by (simp add: proj_def)
```
```   427   have cont_sp0: "continuous_on (affine hull S - {0}) (surf o proj)"
```
```   428     apply (rule continuous_on_compose [OF continuous_on_subset [OF cont_proj]], force)
```
```   429     apply (rule continuous_on_subset [OF cont_surf])
```
```   430     using homeomorphism_image1 proj_spherI surf by fastforce
```
```   431   obtain B where "B>0" and B: "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B"
```
```   432     by (metis compact_imp_bounded \<open>compact S\<close> bounded_pos_less less_eq_real_def)
```
```   433   have cont_nosp: "continuous (at x within ?CBALL) (\<lambda>x. norm x *\<^sub>R surf (proj x))"
```
```   434          if "norm x \<le> 1" "x \<in> affine hull S" for x
```
```   435   proof (cases "x=0")
```
```   436     case True
```
```   437     show ?thesis using True
```
```   438       apply (simp add: continuous_within)
```
```   439       apply (rule lim_null_scaleR_bounded [where B=B])
```
```   440       apply (simp_all add: tendsto_norm_zero eventually_at)
```
```   441       apply (rule_tac x=B in exI)
```
```   442       using B surfpS proj_def projI apply (auto simp: \<open>B > 0\<close>)
```
```   443       done
```
```   444   next
```
```   445     case False
```
```   446     then have "\<forall>\<^sub>F x in at x. (x \<in> affine hull S - {0}) = (x \<in> affine hull S)"
```
```   447       apply (simp add: eventually_at)
```
```   448       apply (rule_tac x="norm x" in exI)
```
```   449       apply (auto simp: False)
```
```   450       done
```
```   451     with cont_sp0 have *: "continuous (at x within affine hull S) (\<lambda>x. surf (proj x))"
```
```   452       apply (simp add: continuous_on_eq_continuous_within)
```
```   453       apply (drule_tac x=x in bspec, force simp: False that)
```
```   454       apply (simp add: continuous_within Lim_transform_within_set)
```
```   455       done
```
```   456     show ?thesis
```
```   457       apply (rule continuous_within_subset [where s = "affine hull S", OF _ Int_lower2])
```
```   458       apply (rule continuous_intros *)+
```
```   459       done
```
```   460   qed
```
```   461   have cont_nosp2: "continuous_on ?CBALL (\<lambda>x. norm x *\<^sub>R ((surf o proj) x))"
```
```   462     by (simp add: continuous_on_eq_continuous_within cont_nosp)
```
```   463   have "norm y *\<^sub>R surf (proj y) \<in> S"  if "y \<in> cball 0 1" and yaff: "y \<in> affine hull S" for y
```
```   464   proof (cases "y=0")
```
```   465     case True then show ?thesis
```
```   466       by (simp add: \<open>0 \<in> S\<close>)
```
```   467   next
```
```   468     case False
```
```   469     then have "norm y *\<^sub>R surf (proj y) = norm y *\<^sub>R surf (proj (y /\<^sub>R norm y))"
```
```   470       by (simp add: proj_def)
```
```   471     have "norm y \<le> 1" using that by simp
```
```   472     have "surf (proj (y /\<^sub>R norm y)) \<in> S"
```
```   473       apply (rule surfpS)
```
```   474       using proj_def projI yaff
```
```   475       by (auto simp: False)
```
```   476     then have "surf (proj y) \<in> S"
```
```   477       by (simp add: False proj_def)
```
```   478     then show "norm y *\<^sub>R surf (proj y) \<in> S"
```
```   479       by (metis dual_order.antisym le_less_linear norm_ge_zero rel_interior_subset scaleR_one
```
```   480                 starI subset_eq \<open>norm y \<le> 1\<close>)
```
```   481   qed
```
```   482   moreover have "x \<in> (\<lambda>x. norm x *\<^sub>R surf (proj x)) ` (?CBALL)" if "x \<in> S" for x
```
```   483   proof (cases "x=0")
```
```   484     case True with that hull_inc  show ?thesis by fastforce
```
```   485   next
```
```   486     case False
```
```   487     then have psp: "proj (surf (proj x)) = proj x"
```
```   488       by (metis homeomorphism_def hull_inc proj_spherI surf that)
```
```   489     have nxx: "norm x *\<^sub>R proj x = x"
```
```   490       by (simp add: False local.proj_def)
```
```   491     have affineI: "(1 / norm (surf (proj x))) *\<^sub>R x \<in> affine hull S"
```
```   492       by (metis \<open>0 \<in> S\<close> affine_hull_span_0 hull_inc span_clauses(4) that)
```
```   493     have sproj_nz: "surf (proj x) \<noteq> 0"
```
```   494       by (metis False proj0_iff psp)
```
```   495     then have "proj x = proj (proj x)"
```
```   496       by (metis False nxx proj_scaleR zero_less_norm_iff)
```
```   497     moreover have scaleproj: "\<And>a r. r *\<^sub>R proj a = (r / norm a) *\<^sub>R a"
```
```   498       by (simp add: divide_inverse local.proj_def)
```
```   499     ultimately have "(norm (surf (proj x)) / norm x) *\<^sub>R x \<notin> rel_interior S"
```
```   500       by (metis (no_types) sproj_nz divide_self_if hull_inc norm_eq_zero nproj1 projI psp scaleR_one surfp_notin that)
```
```   501     then have "(norm (surf (proj x)) / norm x) \<ge> 1"
```
```   502       using starI [OF that] by (meson starI [OF that] le_less_linear norm_ge_zero zero_le_divide_iff)
```
```   503     then have nole: "norm x \<le> norm (surf (proj x))"
```
```   504       by (simp add: le_divide_eq_1)
```
```   505     show ?thesis
```
```   506       apply (rule_tac x="inverse(norm(surf (proj x))) *\<^sub>R x" in image_eqI)
```
```   507       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)
```
```   508       apply (auto simp: divide_simps nole affineI)
```
```   509       done
```
```   510   qed
```
```   511   ultimately have im_cball: "(\<lambda>x. norm x *\<^sub>R surf (proj x)) ` ?CBALL = S"
```
```   512     by blast
```
```   513   have inj_cball: "inj_on (\<lambda>x. norm x *\<^sub>R surf (proj x)) ?CBALL"
```
```   514   proof
```
```   515     fix x y
```
```   516     assume "x \<in> ?CBALL" "y \<in> ?CBALL"
```
```   517        and eq: "norm x *\<^sub>R surf (proj x) = norm y *\<^sub>R surf (proj y)"
```
```   518     then have x: "x \<in> affine hull S" and y: "y \<in> affine hull S"
```
```   519       using 0 by auto
```
```   520     show "x = y"
```
```   521     proof (cases "x=0 \<or> y=0")
```
```   522       case True then show "x = y" using eq proj_spherI surf_nz x y by force
```
```   523     next
```
```   524       case False
```
```   525       with x y have speq: "surf (proj x) = surf (proj y)"
```
```   526         by (metis eq homeomorphism_apply2 proj_scaleR proj_spherI surf zero_less_norm_iff)
```
```   527       then have "norm x = norm y"
```
```   528         by (metis \<open>x \<in> affine hull S\<close> \<open>y \<in> affine hull S\<close> eq proj_spherI real_vector.scale_cancel_right surf_nz)
```
```   529       moreover have "proj x = proj y"
```
```   530         by (metis (no_types) False speq homeomorphism_apply2 proj_spherI surf x y)
```
```   531       ultimately show "x = y"
```
```   532         using eq eqI by blast
```
```   533     qed
```
```   534   qed
```
```   535   have co01: "compact ?CBALL"
```
```   536     by (simp add: closed_affine_hull compact_Int_closed)
```
```   537   show "S homeomorphic ?CBALL"
```
```   538     apply (subst homeomorphic_sym)
```
```   539     apply (rule homeomorphic_compact [OF co01 cont_nosp2 [unfolded o_def] im_cball inj_cball])
```
```   540     done
```
```   541 qed
```
```   542
```
```   543 corollary%important
```
```   544   fixes S :: "'a::euclidean_space set"
```
```   545   assumes "compact S" and a: "a \<in> rel_interior S"
```
```   546       and star: "\<And>x. x \<in> S \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
```
```   547     shows starlike_compact_projective1:
```
```   548             "S - rel_interior S homeomorphic sphere a 1 \<inter> affine hull S"
```
```   549       and starlike_compact_projective2:
```
```   550             "S homeomorphic cball a 1 \<inter> affine hull S"
```
```   551 proof%unimportant -
```
```   552   have 1: "compact ((+) (-a) ` S)" by (meson assms compact_translation)
```
```   553   have 2: "0 \<in> rel_interior ((+) (-a) ` S)"
```
```   554     by (simp add: a rel_interior_translation)
```
```   555   have 3: "open_segment 0 x \<subseteq> rel_interior ((+) (-a) ` S)" if "x \<in> ((+) (-a) ` S)" for x
```
```   556   proof -
```
```   557     have "x+a \<in> S" using that by auto
```
```   558     then have "open_segment a (x+a) \<subseteq> rel_interior S" by (metis star)
```
```   559     then show ?thesis using open_segment_translation
```
```   560       using rel_interior_translation by fastforce
```
```   561   qed
```
```   562   have "S - rel_interior S homeomorphic ((+) (-a) ` S) - rel_interior ((+) (-a) ` S)"
```
```   563     by (metis rel_interior_translation translation_diff homeomorphic_translation)
```
```   564   also have "... homeomorphic sphere 0 1 \<inter> affine hull ((+) (-a) ` S)"
```
```   565     by (rule starlike_compact_projective1_0 [OF 1 2 3])
```
```   566   also have "... = (+) (-a) ` (sphere a 1 \<inter> affine hull S)"
```
```   567     by (metis affine_hull_translation left_minus sphere_translation translation_Int)
```
```   568   also have "... homeomorphic sphere a 1 \<inter> affine hull S"
```
```   569     using homeomorphic_translation homeomorphic_sym by blast
```
```   570   finally show "S - rel_interior S homeomorphic sphere a 1 \<inter> affine hull S" .
```
```   571
```
```   572   have "S homeomorphic ((+) (-a) ` S)"
```
```   573     by (metis homeomorphic_translation)
```
```   574   also have "... homeomorphic cball 0 1 \<inter> affine hull ((+) (-a) ` S)"
```
```   575     by (rule starlike_compact_projective2_0 [OF 1 2 3])
```
```   576   also have "... = (+) (-a) ` (cball a 1 \<inter> affine hull S)"
```
```   577     by (metis affine_hull_translation left_minus cball_translation translation_Int)
```
```   578   also have "... homeomorphic cball a 1 \<inter> affine hull S"
```
```   579     using homeomorphic_translation homeomorphic_sym by blast
```
```   580   finally show "S homeomorphic cball a 1 \<inter> affine hull S" .
```
```   581 qed
```
```   582
```
```   583 corollary%important starlike_compact_projective_special:
```
```   584   assumes "compact S"
```
```   585     and cb01: "cball (0::'a::euclidean_space) 1 \<subseteq> S"
```
```   586     and scale: "\<And>x u. \<lbrakk>x \<in> S; 0 \<le> u; u < 1\<rbrakk> \<Longrightarrow> u *\<^sub>R x \<in> S - frontier S"
```
```   587   shows "S homeomorphic (cball (0::'a::euclidean_space) 1)"
```
```   588 proof%unimportant -
```
```   589   have "ball 0 1 \<subseteq> interior S"
```
```   590     using cb01 interior_cball interior_mono by blast
```
```   591   then have 0: "0 \<in> rel_interior S"
```
```   592     by (meson centre_in_ball subsetD interior_subset_rel_interior le_numeral_extra(2) not_le)
```
```   593   have [simp]: "affine hull S = UNIV"
```
```   594     using \<open>ball 0 1 \<subseteq> interior S\<close> by (auto intro!: affine_hull_nonempty_interior)
```
```   595   have star: "open_segment 0 x \<subseteq> rel_interior S" if "x \<in> S" for x
```
```   596   proof
```
```   597     fix p assume "p \<in> open_segment 0 x"
```
```   598     then obtain u where "x \<noteq> 0" and u: "0 \<le> u" "u < 1" and p: "u *\<^sub>R x = p"
```
```   599       by (auto simp: in_segment)
```
```   600     then show "p \<in> rel_interior S"
```
```   601       using scale [OF that u] closure_subset frontier_def interior_subset_rel_interior by fastforce
```
```   602   qed
```
```   603   show ?thesis
```
```   604     using starlike_compact_projective2_0 [OF \<open>compact S\<close> 0 star] by simp
```
```   605 qed
```
```   606
```
```   607 lemma%important homeomorphic_convex_lemma:
```
```   608   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
```
```   609   assumes "convex S" "compact S" "convex T" "compact T"
```
```   610       and affeq: "aff_dim S = aff_dim T"
```
```   611     shows "(S - rel_interior S) homeomorphic (T - rel_interior T) \<and>
```
```   612            S homeomorphic T"
```
```   613 proof%unimportant (cases "rel_interior S = {} \<or> rel_interior T = {}")
```
```   614   case True
```
```   615     then show ?thesis
```
```   616       by (metis Diff_empty affeq \<open>convex S\<close> \<open>convex T\<close> aff_dim_empty homeomorphic_empty rel_interior_eq_empty aff_dim_empty)
```
```   617 next
```
```   618   case False
```
```   619   then obtain a b where a: "a \<in> rel_interior S" and b: "b \<in> rel_interior T" by auto
```
```   620   have starS: "\<And>x. x \<in> S \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
```
```   621     using rel_interior_closure_convex_segment
```
```   622           a \<open>convex S\<close> closure_subset subsetCE by blast
```
```   623   have starT: "\<And>x. x \<in> T \<Longrightarrow> open_segment b x \<subseteq> rel_interior T"
```
```   624     using rel_interior_closure_convex_segment
```
```   625           b \<open>convex T\<close> closure_subset subsetCE by blast
```
```   626   let ?aS = "(+) (-a) ` S" and ?bT = "(+) (-b) ` T"
```
```   627   have 0: "0 \<in> affine hull ?aS" "0 \<in> affine hull ?bT"
```
```   628     by (metis a b subsetD hull_inc image_eqI left_minus rel_interior_subset)+
```
```   629   have subs: "subspace (span ?aS)" "subspace (span ?bT)"
```
```   630     by (rule subspace_span)+
```
```   631   moreover
```
```   632   have "dim (span ((+) (- a) ` S)) = dim (span ((+) (- b) ` T))"
```
```   633     by (metis 0 aff_dim_translation_eq aff_dim_zero affeq dim_span nat_int)
```
```   634   ultimately obtain f g where "linear f" "linear g"
```
```   635                 and fim: "f ` span ?aS = span ?bT"
```
```   636                 and gim: "g ` span ?bT = span ?aS"
```
```   637                 and fno: "\<And>x. x \<in> span ?aS \<Longrightarrow> norm(f x) = norm x"
```
```   638                 and gno: "\<And>x. x \<in> span ?bT \<Longrightarrow> norm(g x) = norm x"
```
```   639                 and gf: "\<And>x. x \<in> span ?aS \<Longrightarrow> g(f x) = x"
```
```   640                 and fg: "\<And>x. x \<in> span ?bT \<Longrightarrow> f(g x) = x"
```
```   641     by (rule isometries_subspaces) blast
```
```   642   have [simp]: "continuous_on A f" for A
```
```   643     using \<open>linear f\<close> linear_conv_bounded_linear linear_continuous_on by blast
```
```   644   have [simp]: "continuous_on B g" for B
```
```   645     using \<open>linear g\<close> linear_conv_bounded_linear linear_continuous_on by blast
```
```   646   have eqspanS: "affine hull ?aS = span ?aS"
```
```   647     by (metis a affine_hull_span_0 subsetD hull_inc image_eqI left_minus rel_interior_subset)
```
```   648   have eqspanT: "affine hull ?bT = span ?bT"
```
```   649     by (metis b affine_hull_span_0 subsetD hull_inc image_eqI left_minus rel_interior_subset)
```
```   650   have "S homeomorphic cball a 1 \<inter> affine hull S"
```
```   651     by (rule starlike_compact_projective2 [OF \<open>compact S\<close> a starS])
```
```   652   also have "... homeomorphic (+) (-a) ` (cball a 1 \<inter> affine hull S)"
```
```   653     by (metis homeomorphic_translation)
```
```   654   also have "... = cball 0 1 \<inter> (+) (-a) ` (affine hull S)"
```
```   655     by (auto simp: dist_norm)
```
```   656   also have "... = cball 0 1 \<inter> span ?aS"
```
```   657     using eqspanS affine_hull_translation by blast
```
```   658   also have "... homeomorphic cball 0 1 \<inter> span ?bT"
```
```   659     proof (rule homeomorphicI [where f=f and g=g])
```
```   660       show fim1: "f ` (cball 0 1 \<inter> span ?aS) = cball 0 1 \<inter> span ?bT"
```
```   661         apply (rule subset_antisym)
```
```   662          using fim fno apply (force simp:, clarify)
```
```   663         by (metis IntI fg gim gno image_eqI mem_cball_0)
```
```   664       show "g ` (cball 0 1 \<inter> span ?bT) = cball 0 1 \<inter> span ?aS"
```
```   665         apply (rule subset_antisym)
```
```   666          using gim gno apply (force simp:, clarify)
```
```   667         by (metis IntI fim1 gf image_eqI)
```
```   668     qed (auto simp: fg gf)
```
```   669   also have "... = cball 0 1 \<inter> (+) (-b) ` (affine hull T)"
```
```   670     using eqspanT affine_hull_translation by blast
```
```   671   also have "... = (+) (-b) ` (cball b 1 \<inter> affine hull T)"
```
```   672     by (auto simp: dist_norm)
```
```   673   also have "... homeomorphic (cball b 1 \<inter> affine hull T)"
```
```   674     by (metis homeomorphic_translation homeomorphic_sym)
```
```   675   also have "... homeomorphic T"
```
```   676     by (metis starlike_compact_projective2 [OF \<open>compact T\<close> b starT] homeomorphic_sym)
```
```   677   finally have 1: "S homeomorphic T" .
```
```   678
```
```   679   have "S - rel_interior S homeomorphic sphere a 1 \<inter> affine hull S"
```
```   680     by (rule starlike_compact_projective1 [OF \<open>compact S\<close> a starS])
```
```   681   also have "... homeomorphic (+) (-a) ` (sphere a 1 \<inter> affine hull S)"
```
```   682     by (metis homeomorphic_translation)
```
```   683   also have "... = sphere 0 1 \<inter> (+) (-a) ` (affine hull S)"
```
```   684     by (auto simp: dist_norm)
```
```   685   also have "... = sphere 0 1 \<inter> span ?aS"
```
```   686     using eqspanS affine_hull_translation by blast
```
```   687   also have "... homeomorphic sphere 0 1 \<inter> span ?bT"
```
```   688     proof (rule homeomorphicI [where f=f and g=g])
```
```   689       show fim1: "f ` (sphere 0 1 \<inter> span ?aS) = sphere 0 1 \<inter> span ?bT"
```
```   690         apply (rule subset_antisym)
```
```   691         using fim fno apply (force simp:, clarify)
```
```   692         by (metis IntI fg gim gno image_eqI mem_sphere_0)
```
```   693       show "g ` (sphere 0 1 \<inter> span ?bT) = sphere 0 1 \<inter> span ?aS"
```
```   694         apply (rule subset_antisym)
```
```   695         using gim gno apply (force simp:, clarify)
```
```   696         by (metis IntI fim1 gf image_eqI)
```
```   697     qed (auto simp: fg gf)
```
```   698   also have "... = sphere 0 1 \<inter> (+) (-b) ` (affine hull T)"
```
```   699     using eqspanT affine_hull_translation by blast
```
```   700   also have "... = (+) (-b) ` (sphere b 1 \<inter> affine hull T)"
```
```   701     by (auto simp: dist_norm)
```
```   702   also have "... homeomorphic (sphere b 1 \<inter> affine hull T)"
```
```   703     by (metis homeomorphic_translation homeomorphic_sym)
```
```   704   also have "... homeomorphic T - rel_interior T"
```
```   705     by (metis starlike_compact_projective1 [OF \<open>compact T\<close> b starT] homeomorphic_sym)
```
```   706   finally have 2: "S - rel_interior S homeomorphic T - rel_interior T" .
```
```   707   show ?thesis
```
```   708     using 1 2 by blast
```
```   709 qed
```
```   710
```
```   711 lemma%unimportant homeomorphic_convex_compact_sets:
```
```   712   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
```
```   713   assumes "convex S" "compact S" "convex T" "compact T"
```
```   714       and affeq: "aff_dim S = aff_dim T"
```
```   715     shows "S homeomorphic T"
```
```   716 using homeomorphic_convex_lemma [OF assms] assms
```
```   717 by (auto simp: rel_frontier_def)
```
```   718
```
```   719 lemma%unimportant homeomorphic_rel_frontiers_convex_bounded_sets:
```
```   720   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
```
```   721   assumes "convex S" "bounded S" "convex T" "bounded T"
```
```   722       and affeq: "aff_dim S = aff_dim T"
```
```   723     shows  "rel_frontier S homeomorphic rel_frontier T"
```
```   724 using assms homeomorphic_convex_lemma [of "closure S" "closure T"]
```
```   725 by (simp add: rel_frontier_def convex_rel_interior_closure)
```
```   726
```
```   727
```
```   728 subsection%important\<open>Homeomorphisms between punctured spheres and affine sets\<close>
```
```   729 text\<open>Including the famous stereoscopic projection of the 3-D sphere to the complex plane\<close>
```
```   730
```
```   731 text\<open>The special case with centre 0 and radius 1\<close>
```
```   732 lemma%unimportant homeomorphic_punctured_affine_sphere_affine_01:
```
```   733   assumes "b \<in> sphere 0 1" "affine T" "0 \<in> T" "b \<in> T" "affine p"
```
```   734       and affT: "aff_dim T = aff_dim p + 1"
```
```   735     shows "(sphere 0 1 \<inter> T) - {b} homeomorphic p"
```
```   736 proof -
```
```   737   have [simp]: "norm b = 1" "b\<bullet>b = 1"
```
```   738     using assms by (auto simp: norm_eq_1)
```
```   739   have [simp]: "T \<inter> {v. b\<bullet>v = 0} \<noteq> {}"
```
```   740     using \<open>0 \<in> T\<close> by auto
```
```   741   have [simp]: "\<not> T \<subseteq> {v. b\<bullet>v = 0}"
```
```   742     using \<open>norm b = 1\<close> \<open>b \<in> T\<close> by auto
```
```   743   define f where "f \<equiv> \<lambda>x. 2 *\<^sub>R b + (2 / (1 - b\<bullet>x)) *\<^sub>R (x - b)"
```
```   744   define g where "g \<equiv> \<lambda>y. b + (4 / (norm y ^ 2 + 4)) *\<^sub>R (y - 2 *\<^sub>R b)"
```
```   745   have [simp]: "\<And>x. \<lbrakk>x \<in> T; b\<bullet>x = 0\<rbrakk> \<Longrightarrow> f (g x) = x"
```
```   746     unfolding f_def g_def by (simp add: algebra_simps divide_simps add_nonneg_eq_0_iff)
```
```   747   have no: "\<And>x. \<lbrakk>norm x = 1; b\<bullet>x \<noteq> 1\<rbrakk> \<Longrightarrow> (norm (f x))\<^sup>2 = 4 * (1 + b\<bullet>x) / (1 - b\<bullet>x)"
```
```   748     apply (simp add: dot_square_norm [symmetric])
```
```   749     apply (simp add: f_def vector_add_divide_simps divide_simps norm_eq_1)
```
```   750     apply (simp add: algebra_simps inner_commute)
```
```   751     done
```
```   752   have [simp]: "\<And>u::real. 8 + u * (u * 8) = u * 16 \<longleftrightarrow> u=1"
```
```   753     by algebra
```
```   754   have [simp]: "\<And>x. \<lbrakk>norm x = 1; b \<bullet> x \<noteq> 1\<rbrakk> \<Longrightarrow> g (f x) = x"
```
```   755     unfolding g_def no by (auto simp: f_def divide_simps)
```
```   756   have [simp]: "\<And>x. \<lbrakk>x \<in> T; b \<bullet> x = 0\<rbrakk> \<Longrightarrow> norm (g x) = 1"
```
```   757     unfolding g_def
```
```   758     apply (rule power2_eq_imp_eq)
```
```   759     apply (simp_all add: dot_square_norm [symmetric] divide_simps vector_add_divide_simps)
```
```   760     apply (simp add: algebra_simps inner_commute)
```
```   761     done
```
```   762   have [simp]: "\<And>x. \<lbrakk>x \<in> T; b \<bullet> x = 0\<rbrakk> \<Longrightarrow> b \<bullet> g x \<noteq> 1"
```
```   763     unfolding g_def
```
```   764     apply (simp_all add: dot_square_norm [symmetric] divide_simps vector_add_divide_simps add_nonneg_eq_0_iff)
```
```   765     apply (auto simp: algebra_simps)
```
```   766     done
```
```   767   have "subspace T"
```
```   768     by (simp add: assms subspace_affine)
```
```   769   have [simp]: "\<And>x. \<lbrakk>x \<in> T; b \<bullet> x = 0\<rbrakk> \<Longrightarrow> g x \<in> T"
```
```   770     unfolding g_def
```
```   771     by (blast intro: \<open>subspace T\<close> \<open>b \<in> T\<close> subspace_add subspace_mul subspace_diff)
```
```   772   have "f ` {x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<subseteq> {x. b\<bullet>x = 0}"
```
```   773     unfolding f_def using \<open>norm b = 1\<close> norm_eq_1
```
```   774     by (force simp: field_simps inner_add_right inner_diff_right)
```
```   775   moreover have "f ` T \<subseteq> T"
```
```   776     unfolding f_def using assms
```
```   777     apply (auto simp: field_simps inner_add_right inner_diff_right)
```
```   778     by (metis add_0 diff_zero mem_affine_3_minus)
```
```   779   moreover have "{x. b\<bullet>x = 0} \<inter> T \<subseteq> f ` ({x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T)"
```
```   780     apply clarify
```
```   781     apply (rule_tac x = "g x" in image_eqI, auto)
```
```   782     done
```
```   783   ultimately have imf: "f ` ({x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T) = {x. b\<bullet>x = 0} \<inter> T"
```
```   784     by blast
```
```   785   have no4: "\<And>y. b\<bullet>y = 0 \<Longrightarrow> norm ((y\<bullet>y + 4) *\<^sub>R b + 4 *\<^sub>R (y - 2 *\<^sub>R b)) = y\<bullet>y + 4"
```
```   786     apply (rule power2_eq_imp_eq)
```
```   787     apply (simp_all add: dot_square_norm [symmetric])
```
```   788     apply (auto simp: power2_eq_square algebra_simps inner_commute)
```
```   789     done
```
```   790   have [simp]: "\<And>x. \<lbrakk>norm x = 1; b \<bullet> x \<noteq> 1\<rbrakk> \<Longrightarrow> b \<bullet> f x = 0"
```
```   791     by (simp add: f_def algebra_simps divide_simps)
```
```   792   have [simp]: "\<And>x. \<lbrakk>x \<in> T; norm x = 1; b \<bullet> x \<noteq> 1\<rbrakk> \<Longrightarrow> f x \<in> T"
```
```   793     unfolding f_def
```
```   794     by (blast intro: \<open>subspace T\<close> \<open>b \<in> T\<close> subspace_add subspace_mul subspace_diff)
```
```   795   have "g ` {x. b\<bullet>x = 0} \<subseteq> {x. norm x = 1 \<and> b\<bullet>x \<noteq> 1}"
```
```   796     unfolding g_def
```
```   797     apply (clarsimp simp: no4 vector_add_divide_simps divide_simps add_nonneg_eq_0_iff dot_square_norm [symmetric])
```
```   798     apply (auto simp: algebra_simps)
```
```   799     done
```
```   800   moreover have "g ` T \<subseteq> T"
```
```   801     unfolding g_def
```
```   802     by (blast intro: \<open>subspace T\<close> \<open>b \<in> T\<close> subspace_add subspace_mul subspace_diff)
```
```   803   moreover have "{x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T \<subseteq> g ` ({x. b\<bullet>x = 0} \<inter> T)"
```
```   804     apply clarify
```
```   805     apply (rule_tac x = "f x" in image_eqI, auto)
```
```   806     done
```
```   807   ultimately have img: "g ` ({x. b\<bullet>x = 0} \<inter> T) = {x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T"
```
```   808     by blast
```
```   809   have aff: "affine ({x. b\<bullet>x = 0} \<inter> T)"
```
```   810     by (blast intro: affine_hyperplane assms)
```
```   811   have contf: "continuous_on ({x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T) f"
```
```   812     unfolding f_def by (rule continuous_intros | force)+
```
```   813   have contg: "continuous_on ({x. b\<bullet>x = 0} \<inter> T) g"
```
```   814     unfolding g_def by (rule continuous_intros | force simp: add_nonneg_eq_0_iff)+
```
```   815   have "(sphere 0 1 \<inter> T) - {b} = {x. norm x = 1 \<and> (b\<bullet>x \<noteq> 1)} \<inter> T"
```
```   816     using  \<open>norm b = 1\<close> by (auto simp: norm_eq_1) (metis vector_eq  \<open>b\<bullet>b = 1\<close>)
```
```   817   also have "... homeomorphic {x. b\<bullet>x = 0} \<inter> T"
```
```   818     by (rule homeomorphicI [OF imf img contf contg]) auto
```
```   819   also have "... homeomorphic p"
```
```   820     apply (rule homeomorphic_affine_sets [OF aff \<open>affine p\<close>])
```
```   821     apply (simp add: Int_commute aff_dim_affine_Int_hyperplane [OF \<open>affine T\<close>] affT)
```
```   822     done
```
```   823   finally show ?thesis .
```
```   824 qed
```
```   825
```
```   826 theorem%important homeomorphic_punctured_affine_sphere_affine:
```
```   827   fixes a :: "'a :: euclidean_space"
```
```   828   assumes "0 < r" "b \<in> sphere a r" "affine T" "a \<in> T" "b \<in> T" "affine p"
```
```   829       and aff: "aff_dim T = aff_dim p + 1"
```
```   830     shows "(sphere a r \<inter> T) - {b} homeomorphic p"
```
```   831 proof%unimportant -
```
```   832   have "a \<noteq> b" using assms by auto
```
```   833   then have inj: "inj (\<lambda>x::'a. x /\<^sub>R norm (a - b))"
```
```   834     by (simp add: inj_on_def)
```
```   835   have "((sphere a r \<inter> T) - {b}) homeomorphic
```
```   836         (+) (-a) ` ((sphere a r \<inter> T) - {b})"
```
```   837     by (rule homeomorphic_translation)
```
```   838   also have "... homeomorphic (*\<^sub>R) (inverse r) ` (+) (- a) ` (sphere a r \<inter> T - {b})"
```
```   839     by (metis \<open>0 < r\<close> homeomorphic_scaling inverse_inverse_eq inverse_zero less_irrefl)
```
```   840   also have "... = sphere 0 1 \<inter> ((*\<^sub>R) (inverse r) ` (+) (- a) ` T) - {(b - a) /\<^sub>R r}"
```
```   841     using assms by (auto simp: dist_norm norm_minus_commute divide_simps)
```
```   842   also have "... homeomorphic p"
```
```   843     apply (rule homeomorphic_punctured_affine_sphere_affine_01)
```
```   844     using assms
```
```   845     apply (auto simp: dist_norm norm_minus_commute affine_scaling affine_translation [symmetric] aff_dim_translation_eq inj)
```
```   846     done
```
```   847   finally show ?thesis .
```
```   848 qed
```
```   849
```
```   850 corollary%important homeomorphic_punctured_sphere_affine:
```
```   851   fixes a :: "'a :: euclidean_space"
```
```   852   assumes "0 < r" and b: "b \<in> sphere a r"
```
```   853       and "affine T" and affS: "aff_dim T + 1 = DIM('a)"
```
```   854     shows "(sphere a r - {b}) homeomorphic T"
```
```   855   using%unimportant homeomorphic_punctured_affine_sphere_affine [of r b a UNIV T] assms by%unimportant auto
```
```   856
```
```   857 corollary%important homeomorphic_punctured_sphere_hyperplane:
```
```   858   fixes a :: "'a :: euclidean_space"
```
```   859   assumes "0 < r" and b: "b \<in> sphere a r"
```
```   860       and "c \<noteq> 0"
```
```   861     shows "(sphere a r - {b}) homeomorphic {x::'a. c \<bullet> x = d}"
```
```   862 apply (rule homeomorphic_punctured_sphere_affine)
```
```   863 using assms
```
```   864 apply (auto simp: affine_hyperplane of_nat_diff)
```
```   865 done
```
```   866
```
```   867 proposition%important homeomorphic_punctured_sphere_affine_gen:
```
```   868   fixes a :: "'a :: euclidean_space"
```
```   869   assumes "convex S" "bounded S" and a: "a \<in> rel_frontier S"
```
```   870       and "affine T" and affS: "aff_dim S = aff_dim T + 1"
```
```   871     shows "rel_frontier S - {a} homeomorphic T"
```
```   872 proof%unimportant -
```
```   873   obtain U :: "'a set" where "affine U" "convex U" and affdS: "aff_dim U = aff_dim S"
```
```   874     using choose_affine_subset [OF affine_UNIV aff_dim_geq]
```
```   875     by (meson aff_dim_affine_hull affine_affine_hull affine_imp_convex)
```
```   876   have "S \<noteq> {}" using assms by auto
```
```   877   then obtain z where "z \<in> U"
```
```   878     by (metis aff_dim_negative_iff equals0I affdS)
```
```   879   then have bne: "ball z 1 \<inter> U \<noteq> {}" by force
```
```   880   then have [simp]: "aff_dim(ball z 1 \<inter> U) = aff_dim U"
```
```   881     using aff_dim_convex_Int_open [OF \<open>convex U\<close> open_ball]
```
```   882     by (fastforce simp add: Int_commute)
```
```   883   have "rel_frontier S homeomorphic rel_frontier (ball z 1 \<inter> U)"
```
```   884     by (rule homeomorphic_rel_frontiers_convex_bounded_sets)
```
```   885        (auto simp: \<open>affine U\<close> affine_imp_convex convex_Int affdS assms)
```
```   886   also have "... = sphere z 1 \<inter> U"
```
```   887     using convex_affine_rel_frontier_Int [of "ball z 1" U]
```
```   888     by (simp add: \<open>affine U\<close> bne)
```
```   889   finally have "rel_frontier S homeomorphic sphere z 1 \<inter> U" .
```
```   890   then obtain h k where him: "h ` rel_frontier S = sphere z 1 \<inter> U"
```
```   891                     and kim: "k ` (sphere z 1 \<inter> U) = rel_frontier S"
```
```   892                     and hcon: "continuous_on (rel_frontier S) h"
```
```   893                     and kcon: "continuous_on (sphere z 1 \<inter> U) k"
```
```   894                     and kh:  "\<And>x. x \<in> rel_frontier S \<Longrightarrow> k(h(x)) = x"
```
```   895                     and hk:  "\<And>y. y \<in> sphere z 1 \<inter> U \<Longrightarrow> h(k(y)) = y"
```
```   896     unfolding homeomorphic_def homeomorphism_def by auto
```
```   897   have "rel_frontier S - {a} homeomorphic (sphere z 1 \<inter> U) - {h a}"
```
```   898   proof (rule homeomorphicI)
```
```   899     show h: "h ` (rel_frontier S - {a}) = sphere z 1 \<inter> U - {h a}"
```
```   900       using him a kh by auto metis
```
```   901     show "k ` (sphere z 1 \<inter> U - {h a}) = rel_frontier S - {a}"
```
```   902       by (force simp: h [symmetric] image_comp o_def kh)
```
```   903   qed (auto intro: continuous_on_subset hcon kcon simp: kh hk)
```
```   904   also have "... homeomorphic T"
```
```   905     by (rule homeomorphic_punctured_affine_sphere_affine)
```
```   906        (use a him in \<open>auto simp: affS affdS \<open>affine T\<close> \<open>affine U\<close> \<open>z \<in> U\<close>\<close>)
```
```   907   finally show ?thesis .
```
```   908 qed
```
```   909
```
```   910
```
```   911 text\<open> When dealing with AR, ANR and ANR later, it's useful to know that every set
```
```   912   is homeomorphic to a closed subset of a convex set, and
```
```   913   if the set is locally compact we can take the convex set to be the universe.\<close>
```
```   914
```
```   915 proposition%important homeomorphic_closedin_convex:
```
```   916   fixes S :: "'m::euclidean_space set"
```
```   917   assumes "aff_dim S < DIM('n)"
```
```   918   obtains U and T :: "'n::euclidean_space set"
```
```   919      where "convex U" "U \<noteq> {}" "closedin (subtopology euclidean U) T"
```
```   920            "S homeomorphic T"
```
```   921 proof%unimportant (cases "S = {}")
```
```   922   case True then show ?thesis
```
```   923     by (rule_tac U=UNIV and T="{}" in that) auto
```
```   924 next
```
```   925   case False
```
```   926   then obtain a where "a \<in> S" by auto
```
```   927   obtain i::'n where i: "i \<in> Basis" "i \<noteq> 0"
```
```   928     using SOME_Basis Basis_zero by force
```
```   929   have "0 \<in> affine hull ((+) (- a) ` S)"
```
```   930     by (simp add: \<open>a \<in> S\<close> hull_inc)
```
```   931   then have "dim ((+) (- a) ` S) = aff_dim ((+) (- a) ` S)"
```
```   932     by (simp add: aff_dim_zero)
```
```   933   also have "... < DIM('n)"
```
```   934     by (simp add: aff_dim_translation_eq assms)
```
```   935   finally have dd: "dim ((+) (- a) ` S) < DIM('n)"
```
```   936     by linarith
```
```   937   obtain T where "subspace T" and Tsub: "T \<subseteq> {x. i \<bullet> x = 0}"
```
```   938              and dimT: "dim T = dim ((+) (- a) ` S)"
```
```   939     apply (rule choose_subspace_of_subspace [of "dim ((+) (- a) ` S)" "{x::'n. i \<bullet> x = 0}"])
```
```   940      apply (simp add: dim_hyperplane [OF \<open>i \<noteq> 0\<close>])
```
```   941      apply (metis DIM_positive Suc_pred dd not_le not_less_eq_eq)
```
```   942     apply (metis span_eq_iff subspace_hyperplane)
```
```   943     done
```
```   944   have "subspace (span ((+) (- a) ` S))"
```
```   945     using subspace_span by blast
```
```   946   then obtain h k where "linear h" "linear k"
```
```   947                and heq: "h ` span ((+) (- a) ` S) = T"
```
```   948                and keq:"k ` T = span ((+) (- a) ` S)"
```
```   949                and hinv [simp]:  "\<And>x. x \<in> span ((+) (- a) ` S) \<Longrightarrow> k(h x) = x"
```
```   950                and kinv [simp]:  "\<And>x. x \<in> T \<Longrightarrow> h(k x) = x"
```
```   951     apply (rule isometries_subspaces [OF _ \<open>subspace T\<close>])
```
```   952     apply (auto simp: dimT)
```
```   953     done
```
```   954   have hcont: "continuous_on A h" and kcont: "continuous_on B k" for A B
```
```   955     using \<open>linear h\<close> \<open>linear k\<close> linear_continuous_on linear_conv_bounded_linear by blast+
```
```   956   have ihhhh[simp]: "\<And>x. x \<in> S \<Longrightarrow> i \<bullet> h (x - a) = 0"
```
```   957     using Tsub [THEN subsetD] heq span_superset by fastforce
```
```   958   have "sphere 0 1 - {i} homeomorphic {x. i \<bullet> x = 0}"
```
```   959     apply (rule homeomorphic_punctured_sphere_affine)
```
```   960     using i
```
```   961     apply (auto simp: affine_hyperplane)
```
```   962     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)
```
```   963   then obtain f g where fg: "homeomorphism (sphere 0 1 - {i}) {x. i \<bullet> x = 0} f g"
```
```   964     by (force simp: homeomorphic_def)
```
```   965   have "h ` (+) (- a) ` S \<subseteq> T"
```
```   966     using heq span_superset span_linear_image by blast
```
```   967   then have "g ` h ` (+) (- a) ` S \<subseteq> g ` {x. i \<bullet> x = 0}"
```
```   968     using Tsub by (simp add: image_mono)
```
```   969   also have "... \<subseteq> sphere 0 1 - {i}"
```
```   970     by (simp add: fg [unfolded homeomorphism_def])
```
```   971   finally have gh_sub_sph: "(g \<circ> h) ` (+) (- a) ` S \<subseteq> sphere 0 1 - {i}"
```
```   972     by (metis image_comp)
```
```   973   then have gh_sub_cb: "(g \<circ> h) ` (+) (- a) ` S \<subseteq> cball 0 1"
```
```   974     by (metis Diff_subset order_trans sphere_cball)
```
```   975   have [simp]: "\<And>u. u \<in> S \<Longrightarrow> norm (g (h (u - a))) = 1"
```
```   976     using gh_sub_sph [THEN subsetD] by (auto simp: o_def)
```
```   977   have ghcont: "continuous_on ((+) (- a) ` S) (\<lambda>x. g (h x))"
```
```   978     apply (rule continuous_on_compose2 [OF homeomorphism_cont2 [OF fg] hcont], force)
```
```   979     done
```
```   980   have kfcont: "continuous_on ((g \<circ> h \<circ> (+) (- a)) ` S) (\<lambda>x. k (f x))"
```
```   981     apply (rule continuous_on_compose2 [OF kcont])
```
```   982     using homeomorphism_cont1 [OF fg] gh_sub_sph apply (force intro: continuous_on_subset, blast)
```
```   983     done
```
```   984   have "S homeomorphic (+) (- a) ` S"
```
```   985     by (simp add: homeomorphic_translation)
```
```   986   also have Shom: "\<dots> homeomorphic (g \<circ> h) ` (+) (- a) ` S"
```
```   987     apply (simp add: homeomorphic_def homeomorphism_def)
```
```   988     apply (rule_tac x="g \<circ> h" in exI)
```
```   989     apply (rule_tac x="k \<circ> f" in exI)
```
```   990     apply (auto simp: ghcont kfcont span_base homeomorphism_apply2 [OF fg] image_comp)
```
```   991     apply (force simp: o_def homeomorphism_apply2 [OF fg] span_base)
```
```   992     done
```
```   993   finally have Shom: "S homeomorphic (g \<circ> h) ` (+) (- a) ` S" .
```
```   994   show ?thesis
```
```   995     apply (rule_tac U = "ball 0 1 \<union> image (g o h) ((+) (- a) ` S)"
```
```   996                 and T = "image (g o h) ((+) (- a) ` S)"
```
```   997                     in that)
```
```   998     apply (rule convex_intermediate_ball [of 0 1], force)
```
```   999     using gh_sub_cb apply force
```
```  1000     apply force
```
```  1001     apply (simp add: closedin_closed)
```
```  1002     apply (rule_tac x="sphere 0 1" in exI)
```
```  1003     apply (auto simp: Shom)
```
```  1004     done
```
```  1005 qed
```
```  1006
```
```  1007 subsection%important\<open>Locally compact sets in an open set\<close>
```
```  1008
```
```  1009 text\<open> Locally compact sets are closed in an open set and are homeomorphic
```
```  1010   to an absolutely closed set if we have one more dimension to play with.\<close>
```
```  1011
```
```  1012 lemma%important locally_compact_open_Int_closure:
```
```  1013   fixes S :: "'a :: metric_space set"
```
```  1014   assumes "locally compact S"
```
```  1015   obtains T where "open T" "S = T \<inter> closure S"
```
```  1016 proof%unimportant -
```
```  1017   have "\<forall>x\<in>S. \<exists>T v u. u = S \<inter> T \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> S \<and> open T \<and> compact v"
```
```  1018     by (metis assms locally_compact openin_open)
```
```  1019   then obtain t v where
```
```  1020         tv: "\<And>x. x \<in> S
```
```  1021              \<Longrightarrow> v x \<subseteq> S \<and> open (t x) \<and> compact (v x) \<and> (\<exists>u. x \<in> u \<and> u \<subseteq> v x \<and> u = S \<inter> t x)"
```
```  1022     by metis
```
```  1023   then have o: "open (\<Union>(t ` S))"
```
```  1024     by blast
```
```  1025   have "S = \<Union> (v ` S)"
```
```  1026     using tv by blast
```
```  1027   also have "... = \<Union>(t ` S) \<inter> closure S"
```
```  1028   proof
```
```  1029     show "\<Union>(v ` S) \<subseteq> \<Union>(t ` S) \<inter> closure S"
```
```  1030       apply safe
```
```  1031        apply (metis Int_iff subsetD UN_iff tv)
```
```  1032       apply (simp add: closure_def rev_subsetD tv)
```
```  1033       done
```
```  1034     have "t x \<inter> closure S \<subseteq> v x" if "x \<in> S" for x
```
```  1035     proof -
```
```  1036       have "t x \<inter> closure S \<subseteq> closure (t x \<inter> S)"
```
```  1037         by (simp add: open_Int_closure_subset that tv)
```
```  1038       also have "... \<subseteq> v x"
```
```  1039         by (metis Int_commute closure_minimal compact_imp_closed that tv)
```
```  1040       finally show ?thesis .
```
```  1041     qed
```
```  1042     then show "\<Union>(t ` S) \<inter> closure S \<subseteq> \<Union>(v ` S)"
```
```  1043       by blast
```
```  1044   qed
```
```  1045   finally have e: "S = \<Union>(t ` S) \<inter> closure S" .
```
```  1046   show ?thesis
```
```  1047     by (rule that [OF o e])
```
```  1048 qed
```
```  1049
```
```  1050
```
```  1051 lemma%unimportant locally_compact_closedin_open:
```
```  1052     fixes S :: "'a :: metric_space set"
```
```  1053     assumes "locally compact S"
```
```  1054     obtains T where "open T" "closedin (subtopology euclidean T) S"
```
```  1055   by (metis locally_compact_open_Int_closure [OF assms] closed_closure closedin_closed_Int)
```
```  1056
```
```  1057
```
```  1058 lemma%unimportant locally_compact_homeomorphism_projection_closed:
```
```  1059   assumes "locally compact S"
```
```  1060   obtains T and f :: "'a \<Rightarrow> 'a :: euclidean_space \<times> 'b :: euclidean_space"
```
```  1061     where "closed T" "homeomorphism S T f fst"
```
```  1062 proof (cases "closed S")
```
```  1063   case True
```
```  1064     then show ?thesis
```
```  1065       apply (rule_tac T = "S \<times> {0}" and f = "\<lambda>x. (x, 0)" in that)
```
```  1066       apply (auto simp: closed_Times homeomorphism_def continuous_intros)
```
```  1067       done
```
```  1068 next
```
```  1069   case False
```
```  1070     obtain U where "open U" and US: "U \<inter> closure S = S"
```
```  1071       by (metis locally_compact_open_Int_closure [OF assms])
```
```  1072     with False have Ucomp: "-U \<noteq> {}"
```
```  1073       using closure_eq by auto
```
```  1074     have [simp]: "closure (- U) = -U"
```
```  1075       by (simp add: \<open>open U\<close> closed_Compl)
```
```  1076     define f :: "'a \<Rightarrow> 'a \<times> 'b" where "f \<equiv> \<lambda>x. (x, One /\<^sub>R setdist {x} (- U))"
```
```  1077     have "continuous_on U (\<lambda>x. (x, One /\<^sub>R setdist {x} (- U)))"
```
```  1078       apply (intro continuous_intros continuous_on_setdist)
```
```  1079       by (simp add: Ucomp setdist_eq_0_sing_1)
```
```  1080     then have homU: "homeomorphism U (f`U) f fst"
```
```  1081       by (auto simp: f_def homeomorphism_def image_iff continuous_intros)
```
```  1082     have cloS: "closedin (subtopology euclidean U) S"
```
```  1083       by (metis US closed_closure closedin_closed_Int)
```
```  1084     have cont: "isCont ((\<lambda>x. setdist {x} (- U)) o fst) z" for z :: "'a \<times> 'b"
```
```  1085       by (rule continuous_at_compose continuous_intros continuous_at_setdist)+
```
```  1086     have setdist1D: "setdist {a} (- U) *\<^sub>R b = One \<Longrightarrow> setdist {a} (- U) \<noteq> 0" for a::'a and b::'b
```
```  1087       by force
```
```  1088     have *: "r *\<^sub>R b = One \<Longrightarrow> b = (1 / r) *\<^sub>R One" for r and b::'b
```
```  1089       by (metis One_non_0 nonzero_divide_eq_eq real_vector.scale_eq_0_iff real_vector.scale_scale scaleR_one)
```
```  1090     have "f ` U = (\<lambda>z. (setdist {fst z} (- U) *\<^sub>R snd z)) -` {One}"
```
```  1091       apply (auto simp: f_def setdist_eq_0_sing_1 field_simps Ucomp)
```
```  1092       apply (rule_tac x=a in image_eqI)
```
```  1093       apply (auto simp: * setdist_eq_0_sing_1 dest: setdist1D)
```
```  1094       done
```
```  1095     then have clfU: "closed (f ` U)"
```
```  1096       apply (rule ssubst)
```
```  1097       apply (rule continuous_closed_vimage)
```
```  1098       apply (auto intro: continuous_intros cont [unfolded o_def])
```
```  1099       done
```
```  1100     have "closed (f ` S)"
```
```  1101        apply (rule closedin_closed_trans [OF _ clfU])
```
```  1102        apply (rule homeomorphism_imp_closed_map [OF homU cloS])
```
```  1103        done
```
```  1104     then show ?thesis
```
```  1105       apply (rule that)
```
```  1106       apply (rule homeomorphism_of_subsets [OF homU])
```
```  1107       using US apply auto
```
```  1108       done
```
```  1109 qed
```
```  1110
```
```  1111 lemma%unimportant locally_compact_closed_Int_open:
```
```  1112   fixes S :: "'a :: euclidean_space set"
```
```  1113   shows
```
```  1114     "locally compact S \<longleftrightarrow> (\<exists>U u. closed U \<and> open u \<and> S = U \<inter> u)"
```
```  1115 by (metis closed_closure closed_imp_locally_compact inf_commute locally_compact_Int locally_compact_open_Int_closure open_imp_locally_compact)
```
```  1116
```
```  1117
```
```  1118 lemma%unimportant lowerdim_embeddings:
```
```  1119   assumes  "DIM('a) < DIM('b)"
```
```  1120   obtains f :: "'a::euclidean_space*real \<Rightarrow> 'b::euclidean_space"
```
```  1121       and g :: "'b \<Rightarrow> 'a*real"
```
```  1122       and j :: 'b
```
```  1123   where "linear f" "linear g" "\<And>z. g (f z) = z" "j \<in> Basis" "\<And>x. f(x,0) \<bullet> j = 0"
```
```  1124 proof -
```
```  1125   let ?B = "Basis :: ('a*real) set"
```
```  1126   have b01: "(0,1) \<in> ?B"
```
```  1127     by (simp add: Basis_prod_def)
```
```  1128   have "DIM('a * real) \<le> DIM('b)"
```
```  1129     by (simp add: Suc_leI assms)
```
```  1130   then obtain basf :: "'a*real \<Rightarrow> 'b" where sbf: "basf ` ?B \<subseteq> Basis" and injbf: "inj_on basf Basis"
```
```  1131     by (metis finite_Basis card_le_inj)
```
```  1132   define basg:: "'b \<Rightarrow> 'a * real" where
```
```  1133     "basg \<equiv> \<lambda>i. if i \<in> basf ` Basis then inv_into Basis basf i else (0,1)"
```
```  1134   have bgf[simp]: "basg (basf i) = i" if "i \<in> Basis" for i
```
```  1135     using inv_into_f_f injbf that by (force simp: basg_def)
```
```  1136   have sbg: "basg ` Basis \<subseteq> ?B"
```
```  1137     by (force simp: basg_def injbf b01)
```
```  1138   define f :: "'a*real \<Rightarrow> 'b" where "f \<equiv> \<lambda>u. \<Sum>j\<in>Basis. (u \<bullet> basg j) *\<^sub>R j"
```
```  1139   define g :: "'b \<Rightarrow> 'a*real" where "g \<equiv> \<lambda>z. (\<Sum>i\<in>Basis. (z \<bullet> basf i) *\<^sub>R i)"
```
```  1140   show ?thesis
```
```  1141   proof
```
```  1142     show "linear f"
```
```  1143       unfolding f_def
```
```  1144       by (intro linear_compose_sum linearI ballI) (auto simp: algebra_simps)
```
```  1145     show "linear g"
```
```  1146       unfolding g_def
```
```  1147       by (intro linear_compose_sum linearI ballI) (auto simp: algebra_simps)
```
```  1148     have *: "(\<Sum>a \<in> Basis. a \<bullet> basf b * (x \<bullet> basg a)) = x \<bullet> b" if "b \<in> Basis" for x b
```
```  1149       using sbf that by auto
```
```  1150     show gf: "g (f x) = x" for x
```
```  1151       apply (rule euclidean_eqI)
```
```  1152       apply (simp add: f_def g_def inner_sum_left scaleR_sum_left algebra_simps)
```
```  1153       apply (simp add: Groups_Big.sum_distrib_left [symmetric] *)
```
```  1154       done
```
```  1155     show "basf(0,1) \<in> Basis"
```
```  1156       using b01 sbf by auto
```
```  1157     then show "f(x,0) \<bullet> basf(0,1) = 0" for x
```
```  1158       apply (simp add: f_def inner_sum_left)
```
```  1159       apply (rule comm_monoid_add_class.sum.neutral)
```
```  1160       using b01 inner_not_same_Basis by fastforce
```
```  1161   qed
```
```  1162 qed
```
```  1163
```
```  1164 proposition%important locally_compact_homeomorphic_closed:
```
```  1165   fixes S :: "'a::euclidean_space set"
```
```  1166   assumes "locally compact S" and dimlt: "DIM('a) < DIM('b)"
```
```  1167   obtains T :: "'b::euclidean_space set" where "closed T" "S homeomorphic T"
```
```  1168 proof%unimportant -
```
```  1169   obtain U:: "('a*real)set" and h
```
```  1170     where "closed U" and homU: "homeomorphism S U h fst"
```
```  1171     using locally_compact_homeomorphism_projection_closed assms by metis
```
```  1172   obtain f :: "'a*real \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'a*real"
```
```  1173     where "linear f" "linear g" and gf [simp]: "\<And>z. g (f z) = z"
```
```  1174     using lowerdim_embeddings [OF dimlt] by metis
```
```  1175   then have "inj f"
```
```  1176     by (metis injI)
```
```  1177   have gfU: "g ` f ` U = U"
```
```  1178     by (simp add: image_comp o_def)
```
```  1179   have "S homeomorphic U"
```
```  1180     using homU homeomorphic_def by blast
```
```  1181   also have "... homeomorphic f ` U"
```
```  1182     apply (rule homeomorphicI [OF refl gfU])
```
```  1183        apply (meson \<open>inj f\<close> \<open>linear f\<close> homeomorphism_cont2 linear_homeomorphism_image)
```
```  1184     using \<open>linear g\<close> linear_continuous_on linear_conv_bounded_linear apply blast
```
```  1185     apply (auto simp: o_def)
```
```  1186     done
```
```  1187   finally show ?thesis
```
```  1188     apply (rule_tac T = "f ` U" in that)
```
```  1189     apply (rule closed_injective_linear_image [OF \<open>closed U\<close> \<open>linear f\<close> \<open>inj f\<close>], assumption)
```
```  1190     done
```
```  1191 qed
```
```  1192
```
```  1193
```
```  1194 lemma%important homeomorphic_convex_compact_lemma:
```
```  1195   fixes S :: "'a::euclidean_space set"
```
```  1196   assumes "convex S"
```
```  1197     and "compact S"
```
```  1198     and "cball 0 1 \<subseteq> S"
```
```  1199   shows "S homeomorphic (cball (0::'a) 1)"
```
```  1200 proof%unimportant (rule starlike_compact_projective_special[OF assms(2-3)])
```
```  1201   fix x u
```
```  1202   assume "x \<in> S" and "0 \<le> u" and "u < (1::real)"
```
```  1203   have "open (ball (u *\<^sub>R x) (1 - u))"
```
```  1204     by (rule open_ball)
```
```  1205   moreover have "u *\<^sub>R x \<in> ball (u *\<^sub>R x) (1 - u)"
```
```  1206     unfolding centre_in_ball using \<open>u < 1\<close> by simp
```
```  1207   moreover have "ball (u *\<^sub>R x) (1 - u) \<subseteq> S"
```
```  1208   proof
```
```  1209     fix y
```
```  1210     assume "y \<in> ball (u *\<^sub>R x) (1 - u)"
```
```  1211     then have "dist (u *\<^sub>R x) y < 1 - u"
```
```  1212       unfolding mem_ball .
```
```  1213     with \<open>u < 1\<close> have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> cball 0 1"
```
```  1214       by (simp add: dist_norm inverse_eq_divide norm_minus_commute)
```
```  1215     with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> S" ..
```
```  1216     with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \<in> S"
```
```  1217       using \<open>x \<in> S\<close> \<open>0 \<le> u\<close> \<open>u < 1\<close> [THEN less_imp_le] by (rule convexD_alt)
```
```  1218     then show "y \<in> S" using \<open>u < 1\<close>
```
```  1219       by simp
```
```  1220   qed
```
```  1221   ultimately have "u *\<^sub>R x \<in> interior S" ..
```
```  1222   then show "u *\<^sub>R x \<in> S - frontier S"
```
```  1223     using frontier_def and interior_subset by auto
```
```  1224 qed
```
```  1225
```
```  1226 proposition%important homeomorphic_convex_compact_cball:
```
```  1227   fixes e :: real
```
```  1228     and S :: "'a::euclidean_space set"
```
```  1229   assumes "convex S"
```
```  1230     and "compact S"
```
```  1231     and "interior S \<noteq> {}"
```
```  1232     and "e > 0"
```
```  1233   shows "S homeomorphic (cball (b::'a) e)"
```
```  1234 proof%unimportant -
```
```  1235   obtain a where "a \<in> interior S"
```
```  1236     using assms(3) by auto
```
```  1237   then obtain d where "d > 0" and d: "cball a d \<subseteq> S"
```
```  1238     unfolding mem_interior_cball by auto
```
```  1239   let ?d = "inverse d" and ?n = "0::'a"
```
```  1240   have "cball ?n 1 \<subseteq> (\<lambda>x. inverse d *\<^sub>R (x - a)) ` S"
```
```  1241     apply rule
```
```  1242     apply (rule_tac x="d *\<^sub>R x + a" in image_eqI)
```
```  1243     defer
```
```  1244     apply (rule d[unfolded subset_eq, rule_format])
```
```  1245     using \<open>d > 0\<close>
```
```  1246     unfolding mem_cball dist_norm
```
```  1247     apply (auto simp add: mult_right_le_one_le)
```
```  1248     done
```
```  1249   then have "(\<lambda>x. inverse d *\<^sub>R (x - a)) ` S homeomorphic cball ?n 1"
```
```  1250     using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *\<^sub>R -a + ?d *\<^sub>R x) ` S",
```
```  1251       OF convex_affinity compact_affinity]
```
```  1252     using assms(1,2)
```
```  1253     by (auto simp add: scaleR_right_diff_distrib)
```
```  1254   then show ?thesis
```
```  1255     apply (rule_tac homeomorphic_trans[OF _ homeomorphic_balls(2)[of 1 _ ?n]])
```
```  1256     apply (rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" S "?d *\<^sub>R -a"]])
```
```  1257     using \<open>d>0\<close> \<open>e>0\<close>
```
```  1258     apply (auto simp add: scaleR_right_diff_distrib)
```
```  1259     done
```
```  1260 qed
```
```  1261
```
```  1262 corollary%important homeomorphic_convex_compact:
```
```  1263   fixes S :: "'a::euclidean_space set"
```
```  1264     and T :: "'a set"
```
```  1265   assumes "convex S" "compact S" "interior S \<noteq> {}"
```
```  1266     and "convex T" "compact T" "interior T \<noteq> {}"
```
```  1267   shows "S homeomorphic T"
```
```  1268   using assms
```
```  1269   by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)
```
```  1270
```
```  1271 subsection%important\<open>Covering spaces and lifting results for them\<close>
```
```  1272
```
```  1273 definition%important covering_space
```
```  1274            :: "'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
```
```  1275   where
```
```  1276   "covering_space c p S \<equiv>
```
```  1277        continuous_on c p \<and> p ` c = S \<and>
```
```  1278        (\<forall>x \<in> S. \<exists>T. x \<in> T \<and> openin (subtopology euclidean S) T \<and>
```
```  1279                     (\<exists>v. \<Union>v = c \<inter> p -` T \<and>
```
```  1280                         (\<forall>u \<in> v. openin (subtopology euclidean c) u) \<and>
```
```  1281                         pairwise disjnt v \<and>
```
```  1282                         (\<forall>u \<in> v. \<exists>q. homeomorphism u T p q)))"
```
```  1283
```
```  1284 lemma%unimportant covering_space_imp_continuous: "covering_space c p S \<Longrightarrow> continuous_on c p"
```
```  1285   by (simp add: covering_space_def)
```
```  1286
```
```  1287 lemma%unimportant covering_space_imp_surjective: "covering_space c p S \<Longrightarrow> p ` c = S"
```
```  1288   by (simp add: covering_space_def)
```
```  1289
```
```  1290 lemma%unimportant homeomorphism_imp_covering_space: "homeomorphism S T f g \<Longrightarrow> covering_space S f T"
```
```  1291   apply (simp add: homeomorphism_def covering_space_def, clarify)
```
```  1292   apply (rule_tac x=T in exI, simp)
```
```  1293   apply (rule_tac x="{S}" in exI, auto)
```
```  1294   done
```
```  1295
```
```  1296 lemma%unimportant covering_space_local_homeomorphism:
```
```  1297   assumes "covering_space c p S" "x \<in> c"
```
```  1298   obtains T u q where "x \<in> T" "openin (subtopology euclidean c) T"
```
```  1299                       "p x \<in> u" "openin (subtopology euclidean S) u"
```
```  1300                       "homeomorphism T u p q"
```
```  1301 using assms
```
```  1302 apply (simp add: covering_space_def, clarify)
```
```  1303   apply (drule_tac x="p x" in bspec, force)
```
```  1304   by (metis IntI UnionE vimage_eq)
```
```  1305
```
```  1306
```
```  1307 lemma%important covering_space_local_homeomorphism_alt:
```
```  1308   assumes p: "covering_space c p S" and "y \<in> S"
```
```  1309   obtains x T U q where "p x = y"
```
```  1310                         "x \<in> T" "openin (subtopology euclidean c) T"
```
```  1311                         "y \<in> U" "openin (subtopology euclidean S) U"
```
```  1312                           "homeomorphism T U p q"
```
```  1313 proof%unimportant -
```
```  1314   obtain x where "p x = y" "x \<in> c"
```
```  1315     using assms covering_space_imp_surjective by blast
```
```  1316   show ?thesis
```
```  1317     apply (rule covering_space_local_homeomorphism [OF p \<open>x \<in> c\<close>])
```
```  1318     using that \<open>p x = y\<close> by blast
```
```  1319 qed
```
```  1320
```
```  1321 proposition%important covering_space_open_map:
```
```  1322   fixes S :: "'a :: metric_space set" and T :: "'b :: metric_space set"
```
```  1323   assumes p: "covering_space c p S" and T: "openin (subtopology euclidean c) T"
```
```  1324     shows "openin (subtopology euclidean S) (p ` T)"
```
```  1325 proof%unimportant -
```
```  1326   have pce: "p ` c = S"
```
```  1327    and covs:
```
```  1328        "\<And>x. x \<in> S \<Longrightarrow>
```
```  1329             \<exists>X VS. x \<in> X \<and> openin (subtopology euclidean S) X \<and>
```
```  1330                   \<Union>VS = c \<inter> p -` X \<and>
```
```  1331                   (\<forall>u \<in> VS. openin (subtopology euclidean c) u) \<and>
```
```  1332                   pairwise disjnt VS \<and>
```
```  1333                   (\<forall>u \<in> VS. \<exists>q. homeomorphism u X p q)"
```
```  1334     using p by (auto simp: covering_space_def)
```
```  1335   have "T \<subseteq> c"  by (metis openin_euclidean_subtopology_iff T)
```
```  1336   have "\<exists>X. openin (subtopology euclidean S) X \<and> y \<in> X \<and> X \<subseteq> p ` T"
```
```  1337           if "y \<in> p ` T" for y
```
```  1338   proof -
```
```  1339     have "y \<in> S" using \<open>T \<subseteq> c\<close> pce that by blast
```
```  1340     obtain U VS where "y \<in> U" and U: "openin (subtopology euclidean S) U"
```
```  1341                   and VS: "\<Union>VS = c \<inter> p -` U"
```
```  1342                   and openVS: "\<forall>V \<in> VS. openin (subtopology euclidean c) V"
```
```  1343                   and homVS: "\<And>V. V \<in> VS \<Longrightarrow> \<exists>q. homeomorphism V U p q"
```
```  1344       using covs [OF \<open>y \<in> S\<close>] by auto
```
```  1345     obtain x where "x \<in> c" "p x \<in> U" "x \<in> T" "p x = y"
```
```  1346       apply simp
```
```  1347       using T [unfolded openin_euclidean_subtopology_iff] \<open>y \<in> U\<close> \<open>y \<in> p ` T\<close> by blast
```
```  1348     with VS obtain V where "x \<in> V" "V \<in> VS" by auto
```
```  1349     then obtain q where q: "homeomorphism V U p q" using homVS by blast
```
```  1350     then have ptV: "p ` (T \<inter> V) = U \<inter> q -` (T \<inter> V)"
```
```  1351       using VS \<open>V \<in> VS\<close> by (auto simp: homeomorphism_def)
```
```  1352     have ocv: "openin (subtopology euclidean c) V"
```
```  1353       by (simp add: \<open>V \<in> VS\<close> openVS)
```
```  1354     have "openin (subtopology euclidean U) (U \<inter> q -` (T \<inter> V))"
```
```  1355       apply (rule continuous_on_open [THEN iffD1, rule_format])
```
```  1356        using homeomorphism_def q apply blast
```
```  1357       using openin_subtopology_Int_subset [of c] q T unfolding homeomorphism_def
```
```  1358       by (metis inf.absorb_iff2 Int_commute ocv openin_euclidean_subtopology_iff)
```
```  1359     then have os: "openin (subtopology euclidean S) (U \<inter> q -` (T \<inter> V))"
```
```  1360       using openin_trans [of U] by (simp add: Collect_conj_eq U)
```
```  1361     show ?thesis
```
```  1362       apply (rule_tac x = "p ` (T \<inter> V)" in exI)
```
```  1363       apply (rule conjI)
```
```  1364       apply (simp only: ptV os)
```
```  1365       using \<open>p x = y\<close> \<open>x \<in> V\<close> \<open>x \<in> T\<close> apply blast
```
```  1366       done
```
```  1367   qed
```
```  1368   with openin_subopen show ?thesis by blast
```
```  1369 qed
```
```  1370
```
```  1371 lemma%important covering_space_lift_unique_gen:
```
```  1372   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
```
```  1373   fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
```
```  1374   assumes cov: "covering_space c p S"
```
```  1375       and eq: "g1 a = g2 a"
```
```  1376       and f: "continuous_on T f"  "f ` T \<subseteq> S"
```
```  1377       and g1: "continuous_on T g1"  "g1 ` T \<subseteq> c"
```
```  1378       and fg1: "\<And>x. x \<in> T \<Longrightarrow> f x = p(g1 x)"
```
```  1379       and g2: "continuous_on T g2"  "g2 ` T \<subseteq> c"
```
```  1380       and fg2: "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)"
```
```  1381       and u_compt: "U \<in> components T" and "a \<in> U" "x \<in> U"
```
```  1382     shows "g1 x = g2 x"
```
```  1383 proof%unimportant -
```
```  1384   have "U \<subseteq> T" by (rule in_components_subset [OF u_compt])
```
```  1385   define G12 where "G12 \<equiv> {x \<in> U. g1 x - g2 x = 0}"
```
```  1386   have "connected U" by (rule in_components_connected [OF u_compt])
```
```  1387   have contu: "continuous_on U g1" "continuous_on U g2"
```
```  1388        using \<open>U \<subseteq> T\<close> continuous_on_subset g1 g2 by blast+
```
```  1389   have o12: "openin (subtopology euclidean U) G12"
```
```  1390   unfolding G12_def
```
```  1391   proof (subst openin_subopen, clarify)
```
```  1392     fix z
```
```  1393     assume z: "z \<in> U" "g1 z - g2 z = 0"
```
```  1394     obtain v w q where "g1 z \<in> v" and ocv: "openin (subtopology euclidean c) v"
```
```  1395                    and "p (g1 z) \<in> w" and osw: "openin (subtopology euclidean S) w"
```
```  1396                    and hom: "homeomorphism v w p q"
```
```  1397       apply (rule_tac x = "g1 z" in covering_space_local_homeomorphism [OF cov])
```
```  1398        using \<open>U \<subseteq> T\<close> \<open>z \<in> U\<close> g1(2) apply blast+
```
```  1399       done
```
```  1400     have "g2 z \<in> v" using \<open>g1 z \<in> v\<close> z by auto
```
```  1401     have gg: "U \<inter> g -` v = U \<inter> g -` (v \<inter> g ` U)" for g
```
```  1402       by auto
```
```  1403     have "openin (subtopology euclidean (g1 ` U)) (v \<inter> g1 ` U)"
```
```  1404       using ocv \<open>U \<subseteq> T\<close> g1 by (fastforce simp add: openin_open)
```
```  1405     then have 1: "openin (subtopology euclidean U) (U \<inter> g1 -` v)"
```
```  1406       unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
```
```  1407     have "openin (subtopology euclidean (g2 ` U)) (v \<inter> g2 ` U)"
```
```  1408       using ocv \<open>U \<subseteq> T\<close> g2 by (fastforce simp add: openin_open)
```
```  1409     then have 2: "openin (subtopology euclidean U) (U \<inter> g2 -` v)"
```
```  1410       unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
```
```  1411     show "\<exists>T. openin (subtopology euclidean U) T \<and> z \<in> T \<and> T \<subseteq> {z \<in> U. g1 z - g2 z = 0}"
```
```  1412       using z
```
```  1413       apply (rule_tac x = "(U \<inter> g1 -` v) \<inter> (U \<inter> g2 -` v)" in exI)
```
```  1414       apply (intro conjI)
```
```  1415       apply (rule openin_Int [OF 1 2])
```
```  1416       using \<open>g1 z \<in> v\<close>  \<open>g2 z \<in> v\<close>  apply (force simp:, clarify)
```
```  1417       apply (metis \<open>U \<subseteq> T\<close> subsetD eq_iff_diff_eq_0 fg1 fg2 hom homeomorphism_def)
```
```  1418       done
```
```  1419   qed
```
```  1420   have c12: "closedin (subtopology euclidean U) G12"
```
```  1421     unfolding G12_def
```
```  1422     by (intro continuous_intros continuous_closedin_preimage_constant contu)
```
```  1423   have "G12 = {} \<or> G12 = U"
```
```  1424     by (intro connected_clopen [THEN iffD1, rule_format] \<open>connected U\<close> conjI o12 c12)
```
```  1425   with eq \<open>a \<in> U\<close> have "\<And>x. x \<in> U \<Longrightarrow> g1 x - g2 x = 0" by (auto simp: G12_def)
```
```  1426   then show ?thesis
```
```  1427     using \<open>x \<in> U\<close> by force
```
```  1428 qed
```
```  1429
```
```  1430 proposition%important covering_space_lift_unique:
```
```  1431   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
```
```  1432   fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
```
```  1433   assumes "covering_space c p S"
```
```  1434           "g1 a = g2 a"
```
```  1435           "continuous_on T f"  "f ` T \<subseteq> S"
```
```  1436           "continuous_on T g1"  "g1 ` T \<subseteq> c"  "\<And>x. x \<in> T \<Longrightarrow> f x = p(g1 x)"
```
```  1437           "continuous_on T g2"  "g2 ` T \<subseteq> c"  "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)"
```
```  1438           "connected T"  "a \<in> T"   "x \<in> T"
```
```  1439    shows "g1 x = g2 x"
```
```  1440   using%unimportant covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv
```
```  1441   by%unimportant blast
```
```  1442
```
```  1443 lemma%unimportant covering_space_locally:
```
```  1444   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  1445   assumes loc: "locally \<phi> C" and cov: "covering_space C p S"
```
```  1446       and pim: "\<And>T. \<lbrakk>T \<subseteq> C; \<phi> T\<rbrakk> \<Longrightarrow> \<psi>(p ` T)"
```
```  1447     shows "locally \<psi> S"
```
```  1448 proof -
```
```  1449   have "locally \<psi> (p ` C)"
```
```  1450     apply (rule locally_open_map_image [OF loc])
```
```  1451     using cov covering_space_imp_continuous apply blast
```
```  1452     using cov covering_space_imp_surjective covering_space_open_map apply blast
```
```  1453     by (simp add: pim)
```
```  1454   then show ?thesis
```
```  1455     using covering_space_imp_surjective [OF cov] by metis
```
```  1456 qed
```
```  1457
```
```  1458
```
```  1459 proposition%important covering_space_locally_eq:
```
```  1460   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  1461   assumes cov: "covering_space C p S"
```
```  1462       and pim: "\<And>T. \<lbrakk>T \<subseteq> C; \<phi> T\<rbrakk> \<Longrightarrow> \<psi>(p ` T)"
```
```  1463       and qim: "\<And>q U. \<lbrakk>U \<subseteq> S; continuous_on U q; \<psi> U\<rbrakk> \<Longrightarrow> \<phi>(q ` U)"
```
```  1464     shows "locally \<psi> S \<longleftrightarrow> locally \<phi> C"
```
```  1465          (is "?lhs = ?rhs")
```
```  1466 proof%unimportant
```
```  1467   assume L: ?lhs
```
```  1468   show ?rhs
```
```  1469   proof (rule locallyI)
```
```  1470     fix V x
```
```  1471     assume V: "openin (subtopology euclidean C) V" and "x \<in> V"
```
```  1472     have "p x \<in> p ` C"
```
```  1473       by (metis IntE V \<open>x \<in> V\<close> imageI openin_open)
```
```  1474     then obtain T \<V> where "p x \<in> T"
```
```  1475                       and opeT: "openin (subtopology euclidean S) T"
```
```  1476                       and veq: "\<Union>\<V> = C \<inter> p -` T"
```
```  1477                       and ope: "\<forall>U\<in>\<V>. openin (subtopology euclidean C) U"
```
```  1478                       and hom: "\<forall>U\<in>\<V>. \<exists>q. homeomorphism U T p q"
```
```  1479       using cov unfolding covering_space_def by (blast intro: that)
```
```  1480     have "x \<in> \<Union>\<V>"
```
```  1481       using V veq \<open>p x \<in> T\<close> \<open>x \<in> V\<close> openin_imp_subset by fastforce
```
```  1482     then obtain U where "x \<in> U" "U \<in> \<V>"
```
```  1483       by blast
```
```  1484     then obtain q where opeU: "openin (subtopology euclidean C) U" and q: "homeomorphism U T p q"
```
```  1485       using ope hom by blast
```
```  1486     with V have "openin (subtopology euclidean C) (U \<inter> V)"
```
```  1487       by blast
```
```  1488     then have UV: "openin (subtopology euclidean S) (p ` (U \<inter> V))"
```
```  1489       using cov covering_space_open_map by blast
```
```  1490     obtain W W' where opeW: "openin (subtopology euclidean S) W" and "\<psi> W'" "p x \<in> W" "W \<subseteq> W'" and W'sub: "W' \<subseteq> p ` (U \<inter> V)"
```
```  1491       using locallyE [OF L UV] \<open>x \<in> U\<close> \<open>x \<in> V\<close> by blast
```
```  1492     then have "W \<subseteq> T"
```
```  1493       by (metis Int_lower1 q homeomorphism_image1 image_Int_subset order_trans)
```
```  1494     show "\<exists>U Z. openin (subtopology euclidean C) U \<and>
```
```  1495                  \<phi> Z \<and> x \<in> U \<and> U \<subseteq> Z \<and> Z \<subseteq> V"
```
```  1496     proof (intro exI conjI)
```
```  1497       have "openin (subtopology euclidean T) W"
```
```  1498         by (meson opeW opeT openin_imp_subset openin_subset_trans \<open>W \<subseteq> T\<close>)
```
```  1499       then have "openin (subtopology euclidean U) (q ` W)"
```
```  1500         by (meson homeomorphism_imp_open_map homeomorphism_symD q)
```
```  1501       then show "openin (subtopology euclidean C) (q ` W)"
```
```  1502         using opeU openin_trans by blast
```
```  1503       show "\<phi> (q ` W')"
```
```  1504         by (metis (mono_tags, lifting) Int_subset_iff UV W'sub \<open>\<psi> W'\<close> continuous_on_subset dual_order.trans homeomorphism_def image_Int_subset openin_imp_subset q qim)
```
```  1505       show "x \<in> q ` W"
```
```  1506         by (metis \<open>p x \<in> W\<close> \<open>x \<in> U\<close> homeomorphism_def imageI q)
```
```  1507       show "q ` W \<subseteq> q ` W'"
```
```  1508         using \<open>W \<subseteq> W'\<close> by blast
```
```  1509       have "W' \<subseteq> p ` V"
```
```  1510         using W'sub by blast
```
```  1511       then show "q ` W' \<subseteq> V"
```
```  1512         using W'sub homeomorphism_apply1 [OF q] by auto
```
```  1513       qed
```
```  1514   qed
```
```  1515 next
```
```  1516   assume ?rhs
```
```  1517   then show ?lhs
```
```  1518     using cov covering_space_locally pim by blast
```
```  1519 qed
```
```  1520
```
```  1521 lemma%unimportant covering_space_locally_compact_eq:
```
```  1522   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  1523   assumes "covering_space C p S"
```
```  1524   shows "locally compact S \<longleftrightarrow> locally compact C"
```
```  1525   apply (rule covering_space_locally_eq [OF assms])
```
```  1526    apply (meson assms compact_continuous_image continuous_on_subset covering_space_imp_continuous)
```
```  1527   using compact_continuous_image by blast
```
```  1528
```
```  1529 lemma%unimportant covering_space_locally_connected_eq:
```
```  1530   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  1531   assumes "covering_space C p S"
```
```  1532     shows "locally connected S \<longleftrightarrow> locally connected C"
```
```  1533   apply (rule covering_space_locally_eq [OF assms])
```
```  1534    apply (meson connected_continuous_image assms continuous_on_subset covering_space_imp_continuous)
```
```  1535   using connected_continuous_image by blast
```
```  1536
```
```  1537 lemma%unimportant covering_space_locally_path_connected_eq:
```
```  1538   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  1539   assumes "covering_space C p S"
```
```  1540     shows "locally path_connected S \<longleftrightarrow> locally path_connected C"
```
```  1541   apply (rule covering_space_locally_eq [OF assms])
```
```  1542    apply (meson path_connected_continuous_image assms continuous_on_subset covering_space_imp_continuous)
```
```  1543   using path_connected_continuous_image by blast
```
```  1544
```
```  1545
```
```  1546 lemma%unimportant covering_space_locally_compact:
```
```  1547   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  1548   assumes "locally compact C" "covering_space C p S"
```
```  1549   shows "locally compact S"
```
```  1550   using assms covering_space_locally_compact_eq by blast
```
```  1551
```
```  1552
```
```  1553 lemma%unimportant covering_space_locally_connected:
```
```  1554   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  1555   assumes "locally connected C" "covering_space C p S"
```
```  1556   shows "locally connected S"
```
```  1557   using assms covering_space_locally_connected_eq by blast
```
```  1558
```
```  1559 lemma%unimportant covering_space_locally_path_connected:
```
```  1560   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  1561   assumes "locally path_connected C" "covering_space C p S"
```
```  1562   shows "locally path_connected S"
```
```  1563   using assms covering_space_locally_path_connected_eq by blast
```
```  1564
```
```  1565 proposition%important covering_space_lift_homotopy:
```
```  1566   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  1567     and h :: "real \<times> 'c::real_normed_vector \<Rightarrow> 'b"
```
```  1568   assumes cov: "covering_space C p S"
```
```  1569       and conth: "continuous_on ({0..1} \<times> U) h"
```
```  1570       and him: "h ` ({0..1} \<times> U) \<subseteq> S"
```
```  1571       and heq: "\<And>y. y \<in> U \<Longrightarrow> h (0,y) = p(f y)"
```
```  1572       and contf: "continuous_on U f" and fim: "f ` U \<subseteq> C"
```
```  1573     obtains k where "continuous_on ({0..1} \<times> U) k"
```
```  1574                     "k ` ({0..1} \<times> U) \<subseteq> C"
```
```  1575                     "\<And>y. y \<in> U \<Longrightarrow> k(0, y) = f y"
```
```  1576                     "\<And>z. z \<in> {0..1} \<times> U \<Longrightarrow> h z = p(k z)"
```
```  1577 proof%unimportant -
```
```  1578   have "\<exists>V k. openin (subtopology euclidean U) V \<and> y \<in> V \<and>
```
```  1579               continuous_on ({0..1} \<times> V) k \<and> k ` ({0..1} \<times> V) \<subseteq> C \<and>
```
```  1580               (\<forall>z \<in> V. k(0, z) = f z) \<and> (\<forall>z \<in> {0..1} \<times> V. h z = p(k z))"
```
```  1581         if "y \<in> U" for y
```
```  1582   proof -
```
```  1583     obtain UU where UU: "\<And>s. s \<in> S \<Longrightarrow> s \<in> (UU s) \<and> openin (subtopology euclidean S) (UU s) \<and>
```
```  1584                                         (\<exists>\<V>. \<Union>\<V> = C \<inter> p -` UU s \<and>
```
```  1585                                             (\<forall>U \<in> \<V>. openin (subtopology euclidean C) U) \<and>
```
```  1586                                             pairwise disjnt \<V> \<and>
```
```  1587                                             (\<forall>U \<in> \<V>. \<exists>q. homeomorphism U (UU s) p q))"
```
```  1588       using cov unfolding covering_space_def by (metis (mono_tags))
```
```  1589     then have ope: "\<And>s. s \<in> S \<Longrightarrow> s \<in> (UU s) \<and> openin (subtopology euclidean S) (UU s)"
```
```  1590       by blast
```
```  1591     have "\<exists>k n i. open k \<and> open n \<and>
```
```  1592                   t \<in> k \<and> y \<in> n \<and> i \<in> S \<and> h ` (({0..1} \<inter> k) \<times> (U \<inter> n)) \<subseteq> UU i" if "t \<in> {0..1}" for t
```
```  1593     proof -
```
```  1594       have hinS: "h (t, y) \<in> S"
```
```  1595         using \<open>y \<in> U\<close> him that by blast
```
```  1596       then have "(t,y) \<in> ({0..1} \<times> U) \<inter> h -` UU(h(t, y))"
```
```  1597         using \<open>y \<in> U\<close> \<open>t \<in> {0..1}\<close>  by (auto simp: ope)
```
```  1598       moreover have ope_01U: "openin (subtopology euclidean ({0..1} \<times> U)) (({0..1} \<times> U) \<inter> h -` UU(h(t, y)))"
```
```  1599         using hinS ope continuous_on_open_gen [OF him] conth by blast
```
```  1600       ultimately obtain V W where opeV: "open V" and "t \<in> {0..1} \<inter> V" "t \<in> {0..1} \<inter> V"
```
```  1601                               and opeW: "open W" and "y \<in> U" "y \<in> W"
```
```  1602                               and VW: "({0..1} \<inter> V) \<times> (U \<inter> W)  \<subseteq> (({0..1} \<times> U) \<inter> h -` UU(h(t, y)))"
```
```  1603         by (rule Times_in_interior_subtopology) (auto simp: openin_open)
```
```  1604       then show ?thesis
```
```  1605         using hinS by blast
```
```  1606     qed
```
```  1607     then obtain K NN X where
```
```  1608               K: "\<And>t. t \<in> {0..1} \<Longrightarrow> open (K t)"
```
```  1609           and NN: "\<And>t. t \<in> {0..1} \<Longrightarrow> open (NN t)"
```
```  1610           and inUS: "\<And>t. t \<in> {0..1} \<Longrightarrow> t \<in> K t \<and> y \<in> NN t \<and> X t \<in> S"
```
```  1611           and him: "\<And>t. t \<in> {0..1} \<Longrightarrow> h ` (({0..1} \<inter> K t) \<times> (U \<inter> NN t)) \<subseteq> UU (X t)"
```
```  1612     by (metis (mono_tags))
```
```  1613     obtain \<T> where "\<T> \<subseteq> ((\<lambda>i. K i \<times> NN i)) ` {0..1}" "finite \<T>" "{0::real..1} \<times> {y} \<subseteq> \<Union>\<T>"
```
```  1614     proof (rule compactE)
```
```  1615       show "compact ({0::real..1} \<times> {y})"
```
```  1616         by (simp add: compact_Times)
```
```  1617       show "{0..1} \<times> {y} \<subseteq> (\<Union>i\<in>{0..1}. K i \<times> NN i)"
```
```  1618         using K inUS by auto
```
```  1619       show "\<And>B. B \<in> (\<lambda>i. K i \<times> NN i) ` {0..1} \<Longrightarrow> open B"
```
```  1620         using K NN by (auto simp: open_Times)
```
```  1621     qed blast
```
```  1622     then obtain tk where "tk \<subseteq> {0..1}" "finite tk"
```
```  1623                      and tk: "{0::real..1} \<times> {y} \<subseteq> (\<Union>i \<in> tk. K i \<times> NN i)"
```
```  1624       by (metis (no_types, lifting) finite_subset_image)
```
```  1625     then have "tk \<noteq> {}"
```
```  1626       by auto
```
```  1627     define n where "n = \<Inter>(NN ` tk)"
```
```  1628     have "y \<in> n" "open n"
```
```  1629       using inUS NN \<open>tk \<subseteq> {0..1}\<close> \<open>finite tk\<close>
```
```  1630       by (auto simp: n_def open_INT subset_iff)
```
```  1631     obtain \<delta> where "0 < \<delta>" and \<delta>: "\<And>T. \<lbrakk>T \<subseteq> {0..1}; diameter T < \<delta>\<rbrakk> \<Longrightarrow> \<exists>B\<in>K ` tk. T \<subseteq> B"
```
```  1632     proof (rule Lebesgue_number_lemma [of "{0..1}" "K ` tk"])
```
```  1633       show "K ` tk \<noteq> {}"
```
```  1634         using \<open>tk \<noteq> {}\<close> by auto
```
```  1635       show "{0..1} \<subseteq> \<Union>(K ` tk)"
```
```  1636         using tk by auto
```
```  1637       show "\<And>B. B \<in> K ` tk \<Longrightarrow> open B"
```
```  1638         using \<open>tk \<subseteq> {0..1}\<close> K by auto
```
```  1639     qed auto
```
```  1640     obtain N::nat where N: "N > 1 / \<delta>"
```
```  1641       using reals_Archimedean2 by blast
```
```  1642     then have "N > 0"
```
```  1643       using \<open>0 < \<delta>\<close> order.asym by force
```
```  1644     have *: "\<exists>V k. openin (subtopology euclidean U) V \<and> y \<in> V \<and>
```
```  1645                    continuous_on ({0..of_nat n / N} \<times> V) k \<and>
```
```  1646                    k ` ({0..of_nat n / N} \<times> V) \<subseteq> C \<and>
```
```  1647                    (\<forall>z\<in>V. k (0, z) = f z) \<and>
```
```  1648                    (\<forall>z\<in>{0..of_nat n / N} \<times> V. h z = p (k z))" if "n \<le> N" for n
```
```  1649       using that
```
```  1650     proof (induction n)
```
```  1651       case 0
```
```  1652       show ?case
```
```  1653         apply (rule_tac x=U in exI)
```
```  1654         apply (rule_tac x="f \<circ> snd" in exI)
```
```  1655         apply (intro conjI \<open>y \<in> U\<close> continuous_intros continuous_on_subset [OF contf])
```
```  1656         using fim  apply (auto simp: heq)
```
```  1657         done
```
```  1658     next
```
```  1659       case (Suc n)
```
```  1660       then obtain V k where opeUV: "openin (subtopology euclidean U) V"
```
```  1661                         and "y \<in> V"
```
```  1662                         and contk: "continuous_on ({0..real n / real N} \<times> V) k"
```
```  1663                         and kim: "k ` ({0..real n / real N} \<times> V) \<subseteq> C"
```
```  1664                         and keq: "\<And>z. z \<in> V \<Longrightarrow> k (0, z) = f z"
```
```  1665                         and heq: "\<And>z. z \<in> {0..real n / real N} \<times> V \<Longrightarrow> h z = p (k z)"
```
```  1666         using Suc_leD by auto
```
```  1667       have "n \<le> N"
```
```  1668         using Suc.prems by auto
```
```  1669       obtain t where "t \<in> tk" and t: "{real n / real N .. (1 + real n) / real N} \<subseteq> K t"
```
```  1670       proof (rule bexE [OF \<delta>])
```
```  1671         show "{real n / real N .. (1 + real n) / real N} \<subseteq> {0..1}"
```
```  1672           using Suc.prems by (auto simp: divide_simps algebra_simps)
```
```  1673         show diameter_less: "diameter {real n / real N .. (1 + real n) / real N} < \<delta>"
```
```  1674           using \<open>0 < \<delta>\<close> N by (auto simp: divide_simps algebra_simps)
```
```  1675       qed blast
```
```  1676       have t01: "t \<in> {0..1}"
```
```  1677         using \<open>t \<in> tk\<close> \<open>tk \<subseteq> {0..1}\<close> by blast
```
```  1678       obtain \<V> where \<V>: "\<Union>\<V> = C \<inter> p -` UU (X t)"
```
```  1679                  and opeC: "\<And>U. U \<in> \<V> \<Longrightarrow> openin (subtopology euclidean C) U"
```
```  1680                  and "pairwise disjnt \<V>"
```
```  1681                  and homuu: "\<And>U. U \<in> \<V> \<Longrightarrow> \<exists>q. homeomorphism U (UU (X t)) p q"
```
```  1682         using inUS [OF t01] UU by meson
```
```  1683       have n_div_N_in: "real n / real N \<in> {real n / real N .. (1 + real n) / real N}"
```
```  1684         using N by (auto simp: divide_simps algebra_simps)
```
```  1685       with t have nN_in_kkt: "real n / real N \<in> K t"
```
```  1686         by blast
```
```  1687       have "k (real n / real N, y) \<in> C \<inter> p -` UU (X t)"
```
```  1688       proof (simp, rule conjI)
```
```  1689         show "k (real n / real N, y) \<in> C"
```
```  1690           using \<open>y \<in> V\<close> kim keq by force
```
```  1691         have "p (k (real n / real N, y)) = h (real n / real N, y)"
```
```  1692           by (simp add: \<open>y \<in> V\<close> heq)
```
```  1693         also have "... \<in> h ` (({0..1} \<inter> K t) \<times> (U \<inter> NN t))"
```
```  1694           apply (rule imageI)
```
```  1695            using \<open>y \<in> V\<close> t01 \<open>n \<le> N\<close>
```
```  1696           apply (simp add: nN_in_kkt \<open>y \<in> U\<close> inUS divide_simps)
```
```  1697           done
```
```  1698         also have "... \<subseteq> UU (X t)"
```
```  1699           using him t01 by blast
```
```  1700         finally show "p (k (real n / real N, y)) \<in> UU (X t)" .
```
```  1701       qed
```
```  1702       with \<V> have "k (real n / real N, y) \<in> \<Union>\<V>"
```
```  1703         by blast
```
```  1704       then obtain W where W: "k (real n / real N, y) \<in> W" and "W \<in> \<V>"
```
```  1705         by blast
```
```  1706       then obtain p' where opeC': "openin (subtopology euclidean C) W"
```
```  1707                        and hom': "homeomorphism W (UU (X t)) p p'"
```
```  1708         using homuu opeC by blast
```
```  1709       then have "W \<subseteq> C"
```
```  1710         using openin_imp_subset by blast
```
```  1711       define W' where "W' = UU(X t)"
```
```  1712       have opeVW: "openin (subtopology euclidean V) (V \<inter> (k \<circ> Pair (n / N)) -` W)"
```
```  1713         apply (rule continuous_openin_preimage [OF _ _ opeC'])
```
```  1714          apply (intro continuous_intros continuous_on_subset [OF contk])
```
```  1715         using kim apply (auto simp: \<open>y \<in> V\<close> W)
```
```  1716         done
```
```  1717       obtain N' where opeUN': "openin (subtopology euclidean U) N'"
```
```  1718                   and "y \<in> N'" and kimw: "k ` ({(real n / real N)} \<times> N') \<subseteq> W"
```
```  1719         apply (rule_tac N' = "(V \<inter> (k \<circ> Pair (n / N)) -` W)" in that)
```
```  1720         apply (fastforce simp:  \<open>y \<in> V\<close> W intro!: openin_trans [OF opeVW opeUV])+
```
```  1721         done
```
```  1722       obtain Q Q' where opeUQ: "openin (subtopology euclidean U) Q"
```
```  1723                     and cloUQ': "closedin (subtopology euclidean U) Q'"
```
```  1724                     and "y \<in> Q" "Q \<subseteq> Q'"
```
```  1725                     and Q': "Q' \<subseteq> (U \<inter> NN(t)) \<inter> N' \<inter> V"
```
```  1726       proof -
```
```  1727         obtain VO VX where "open VO" "open VX" and VO: "V = U \<inter> VO" and VX: "N' = U \<inter> VX"
```
```  1728           using opeUV opeUN' by (auto simp: openin_open)
```
```  1729         then have "open (NN(t) \<inter> VO \<inter> VX)"
```
```  1730           using NN t01 by blast
```
```  1731         then obtain e where "e > 0" and e: "cball y e \<subseteq> NN(t) \<inter> VO \<inter> VX"
```
```  1732           by (metis Int_iff \<open>N' = U \<inter> VX\<close> \<open>V = U \<inter> VO\<close> \<open>y \<in> N'\<close> \<open>y \<in> V\<close> inUS open_contains_cball t01)
```
```  1733         show ?thesis
```
```  1734         proof
```
```  1735           show "openin (subtopology euclidean U) (U \<inter> ball y e)"
```
```  1736             by blast
```
```  1737           show "closedin (subtopology euclidean U) (U \<inter> cball y e)"
```
```  1738             using e by (auto simp: closedin_closed)
```
```  1739         qed (use \<open>y \<in> U\<close> \<open>e > 0\<close> VO VX e in auto)
```
```  1740       qed
```
```  1741       then have "y \<in> Q'" "Q \<subseteq> (U \<inter> NN(t)) \<inter> N' \<inter> V"
```
```  1742         by blast+
```
```  1743       have neq: "{0..real n / real N} \<union> {real n / real N..(1 + real n) / real N} = {0..(1 + real n) / real N}"
```
```  1744         apply (auto simp: divide_simps)
```
```  1745         by (metis mult_zero_left of_nat_0_le_iff of_nat_0_less_iff order_trans real_mult_le_cancel_iff1)
```
```  1746       then have neqQ': "{0..real n / real N} \<times> Q' \<union> {real n / real N..(1 + real n) / real N} \<times> Q' = {0..(1 + real n) / real N} \<times> Q'"
```
```  1747         by blast
```
```  1748       have cont: "continuous_on ({0..(1 + real n) / real N} \<times> Q')
```
```  1749         (\<lambda>x. if x \<in> {0..real n / real N} \<times> Q' then k x else (p' \<circ> h) x)"
```
```  1750         unfolding neqQ' [symmetric]
```
```  1751       proof (rule continuous_on_cases_local, simp_all add: neqQ' del: comp_apply)
```
```  1752         show "closedin (subtopology euclidean ({0..(1 + real n) / real N} \<times> Q'))
```
```  1753                        ({0..real n / real N} \<times> Q')"
```
```  1754           apply (simp add: closedin_closed)
```
```  1755           apply (rule_tac x="{0 .. real n / real N} \<times> UNIV" in exI)
```
```  1756           using n_div_N_in apply (auto simp: closed_Times)
```
```  1757           done
```
```  1758         show "closedin (subtopology euclidean ({0..(1 + real n) / real N} \<times> Q'))
```
```  1759                        ({real n / real N..(1 + real n) / real N} \<times> Q')"
```
```  1760           apply (simp add: closedin_closed)
```
```  1761           apply (rule_tac x="{real n / real N .. (1 + real n) / real N} \<times> UNIV" in exI)
```
```  1762           apply (auto simp: closed_Times)
```
```  1763           by (meson divide_nonneg_nonneg of_nat_0_le_iff order_trans)
```
```  1764         show "continuous_on ({0..real n / real N} \<times> Q') k"
```
```  1765           apply (rule continuous_on_subset [OF contk])
```
```  1766           using Q' by auto
```
```  1767         have "continuous_on ({real n / real N..(1 + real n) / real N} \<times> Q') h"
```
```  1768         proof (rule continuous_on_subset [OF conth])
```
```  1769           show "{real n / real N..(1 + real n) / real N} \<times> Q' \<subseteq> {0..1} \<times> U"
```
```  1770             using \<open>N > 0\<close>
```
```  1771             apply auto
```
```  1772               apply (meson divide_nonneg_nonneg of_nat_0_le_iff order_trans)
```
```  1773             using Suc.prems order_trans apply fastforce
```
```  1774             apply (metis IntE  cloUQ' closedin_closed)
```
```  1775             done
```
```  1776         qed
```
```  1777         moreover have "continuous_on (h ` ({real n / real N..(1 + real n) / real N} \<times> Q')) p'"
```
```  1778         proof (rule continuous_on_subset [OF homeomorphism_cont2 [OF hom']])
```
```  1779           have "h ` ({real n / real N..(1 + real n) / real N} \<times> Q') \<subseteq> h ` (({0..1} \<inter> K t) \<times> (U \<inter> NN t))"
```
```  1780             apply (rule image_mono)
```
```  1781             using \<open>0 < \<delta>\<close> \<open>N > 0\<close> Suc.prems apply auto
```
```  1782               apply (meson divide_nonneg_nonneg of_nat_0_le_iff order_trans)
```
```  1783             using Suc.prems order_trans apply fastforce
```
```  1784             using t Q' apply auto
```
```  1785             done
```
```  1786           with him show "h ` ({real n / real N..(1 + real n) / real N} \<times> Q') \<subseteq> UU (X t)"
```
```  1787             using t01 by blast
```
```  1788         qed
```
```  1789         ultimately show "continuous_on ({real n / real N..(1 + real n) / real N} \<times> Q') (p' \<circ> h)"
```
```  1790           by (rule continuous_on_compose)
```
```  1791         have "k (real n / real N, b) = p' (h (real n / real N, b))" if "b \<in> Q'" for b
```
```  1792         proof -
```
```  1793           have "k (real n / real N, b) \<in> W"
```
```  1794             using that Q' kimw  by force
```
```  1795           then have "k (real n / real N, b) = p' (p (k (real n / real N, b)))"
```
```  1796             by (simp add:  homeomorphism_apply1 [OF hom'])
```
```  1797           then show ?thesis
```
```  1798             using Q' that by (force simp: heq)
```
```  1799         qed
```
```  1800         then show "\<And>x. x \<in> {real n / real N..(1 + real n) / real N} \<times> Q' \<and>
```
```  1801                   x \<in> {0..real n / real N} \<times> Q' \<Longrightarrow> k x = (p' \<circ> h) x"
```
```  1802           by auto
```
```  1803       qed
```
```  1804       have h_in_UU: "h (x, y) \<in> UU (X t)" if "y \<in> Q" "\<not> x \<le> real n / real N" "0 \<le> x" "x \<le> (1 + real n) / real N" for x y
```
```  1805       proof -
```
```  1806         have "x \<le> 1"
```
```  1807           using Suc.prems that order_trans by force
```
```  1808         moreover have "x \<in> K t"
```
```  1809           by (meson atLeastAtMost_iff le_less not_le subset_eq t that)
```
```  1810         moreover have "y \<in> U"
```
```  1811           using \<open>y \<in> Q\<close> opeUQ openin_imp_subset by blast
```
```  1812         moreover have "y \<in> NN t"
```
```  1813           using Q' \<open>Q \<subseteq> Q'\<close> \<open>y \<in> Q\<close> by auto
```
```  1814         ultimately have "(x, y) \<in> (({0..1} \<inter> K t) \<times> (U \<inter> NN t))"
```
```  1815           using that by auto
```
```  1816         then have "h (x, y) \<in> h ` (({0..1} \<inter> K t) \<times> (U \<inter> NN t))"
```
```  1817           by blast
```
```  1818         also have "... \<subseteq> UU (X t)"
```
```  1819           by (metis him t01)
```
```  1820         finally show ?thesis .
```
```  1821       qed
```
```  1822       let ?k = "(\<lambda>x. if x \<in> {0..real n / real N} \<times> Q' then k x else (p' \<circ> h) x)"
```
```  1823       show ?case
```
```  1824       proof (intro exI conjI)
```
```  1825         show "continuous_on ({0..real (Suc n) / real N} \<times> Q) ?k"
```
```  1826           apply (rule continuous_on_subset [OF cont])
```
```  1827           using \<open>Q \<subseteq> Q'\<close> by auto
```
```  1828         have "\<And>a b. \<lbrakk>a \<le> real n / real N; b \<in> Q'; 0 \<le> a\<rbrakk> \<Longrightarrow> k (a, b) \<in> C"
```
```  1829           using kim Q' by force
```
```  1830         moreover have "\<And>a b. \<lbrakk>b \<in> Q; 0 \<le> a; a \<le> (1 + real n) / real N; \<not> a \<le> real n / real N\<rbrakk> \<Longrightarrow> p' (h (a, b)) \<in> C"
```
```  1831           apply (rule \<open>W \<subseteq> C\<close> [THEN subsetD])
```
```  1832           using homeomorphism_image2 [OF hom', symmetric]  h_in_UU  Q' \<open>Q \<subseteq> Q'\<close> \<open>W \<subseteq> C\<close>
```
```  1833           apply auto
```
```  1834           done
```
```  1835         ultimately show "?k ` ({0..real (Suc n) / real N} \<times> Q) \<subseteq> C"
```
```  1836           using Q' \<open>Q \<subseteq> Q'\<close> by force
```
```  1837         show "\<forall>z\<in>Q. ?k (0, z) = f z"
```
```  1838           using Q' keq  \<open>Q \<subseteq> Q'\<close> by auto
```
```  1839         show "\<forall>z \<in> {0..real (Suc n) / real N} \<times> Q. h z = p(?k z)"
```
```  1840           using \<open>Q \<subseteq> U \<inter> NN t \<inter> N' \<inter> V\<close> heq apply clarsimp
```
```  1841           using h_in_UU Q' \<open>Q \<subseteq> Q'\<close> apply (auto simp: homeomorphism_apply2 [OF hom', symmetric])
```
```  1842           done
```
```  1843         qed (auto simp: \<open>y \<in> Q\<close> opeUQ)
```
```  1844     qed
```
```  1845     show ?thesis
```
```  1846       using*[OF order_refl] N \<open>0 < \<delta>\<close> by (simp add: split: if_split_asm)
```
```  1847   qed
```
```  1848   then obtain V fs where opeV: "\<And>y. y \<in> U \<Longrightarrow> openin (subtopology euclidean U) (V y)"
```
```  1849           and V: "\<And>y. y \<in> U \<Longrightarrow> y \<in> V y"
```
```  1850           and contfs: "\<And>y. y \<in> U \<Longrightarrow> continuous_on ({0..1} \<times> V y) (fs y)"
```
```  1851           and *: "\<And>y. y \<in> U \<Longrightarrow> (fs y) ` ({0..1} \<times> V y) \<subseteq> C \<and>
```
```  1852                             (\<forall>z \<in> V y. fs y (0, z) = f z) \<and>
```
```  1853                             (\<forall>z \<in> {0..1} \<times> V y. h z = p(fs y z))"
```
```  1854     by (metis (mono_tags))
```
```  1855   then have VU: "\<And>y. y \<in> U \<Longrightarrow> V y \<subseteq> U"
```
```  1856     by (meson openin_imp_subset)
```
```  1857   obtain k where contk: "continuous_on ({0..1} \<times> U) k"
```
```  1858              and k: "\<And>x i. \<lbrakk>i \<in> U; x \<in> {0..1} \<times> U \<inter> {0..1} \<times> V i\<rbrakk> \<Longrightarrow> k x = fs i x"
```
```  1859   proof (rule pasting_lemma_exists)
```
```  1860     show "{0..1} \<times> U \<subseteq> (\<Union>i\<in>U. {0..1} \<times> V i)"
```
```  1861       apply auto
```
```  1862       using V by blast
```
```  1863     show "\<And>i. i \<in> U \<Longrightarrow> openin (subtopology euclidean ({0..1} \<times> U)) ({0..1} \<times> V i)"
```
```  1864       by (simp add: opeV openin_Times)
```
```  1865     show "\<And>i. i \<in> U \<Longrightarrow> continuous_on ({0..1} \<times> V i) (fs i)"
```
```  1866       using contfs by blast
```
```  1867     show "fs i x = fs j x"  if "i \<in> U" "j \<in> U" and x: "x \<in> {0..1} \<times> U \<inter> {0..1} \<times> V i \<inter> {0..1} \<times> V j"
```
```  1868          for i j x
```
```  1869     proof -
```
```  1870       obtain u y where "x = (u, y)" "y \<in> V i" "y \<in> V j" "0 \<le> u" "u \<le> 1"
```
```  1871         using x by auto
```
```  1872       show ?thesis
```
```  1873       proof (rule covering_space_lift_unique [OF cov, of _ "(0,y)" _ "{0..1} \<times> {y}" h])
```
```  1874         show "fs i (0, y) = fs j (0, y)"
```
```  1875           using*V by (simp add: \<open>y \<in> V i\<close> \<open>y \<in> V j\<close> that)
```
```  1876         show conth_y: "continuous_on ({0..1} \<times> {y}) h"
```
```  1877           apply (rule continuous_on_subset [OF conth])
```
```  1878           using VU \<open>y \<in> V j\<close> that by auto
```
```  1879         show "h ` ({0..1} \<times> {y}) \<subseteq> S"
```
```  1880           using \<open>y \<in> V i\<close> assms(3) VU that by fastforce
```
```  1881         show "continuous_on ({0..1} \<times> {y}) (fs i)"
```
```  1882           using continuous_on_subset [OF contfs] \<open>i \<in> U\<close>
```
```  1883           by (simp add: \<open>y \<in> V i\<close> subset_iff)
```
```  1884         show "fs i ` ({0..1} \<times> {y}) \<subseteq> C"
```
```  1885           using "*" \<open>y \<in> V i\<close> \<open>i \<in> U\<close> by fastforce
```
```  1886         show "\<And>x. x \<in> {0..1} \<times> {y} \<Longrightarrow> h x = p (fs i x)"
```
```  1887           using "*" \<open>y \<in> V i\<close> \<open>i \<in> U\<close> by blast
```
```  1888         show "continuous_on ({0..1} \<times> {y}) (fs j)"
```
```  1889           using continuous_on_subset [OF contfs] \<open>j \<in> U\<close>
```
```  1890           by (simp add: \<open>y \<in> V j\<close> subset_iff)
```
```  1891         show "fs j ` ({0..1} \<times> {y}) \<subseteq> C"
```
```  1892           using "*" \<open>y \<in> V j\<close> \<open>j \<in> U\<close> by fastforce
```
```  1893         show "\<And>x. x \<in> {0..1} \<times> {y} \<Longrightarrow> h x = p (fs j x)"
```
```  1894           using "*" \<open>y \<in> V j\<close> \<open>j \<in> U\<close> by blast
```
```  1895         show "connected ({0..1::real} \<times> {y})"
```
```  1896           using connected_Icc connected_Times connected_sing by blast
```
```  1897         show "(0, y) \<in> {0..1::real} \<times> {y}"
```
```  1898           by force
```
```  1899         show "x \<in> {0..1} \<times> {y}"
```
```  1900           using \<open>x = (u, y)\<close> x by blast
```
```  1901       qed
```
```  1902     qed
```
```  1903   qed blast
```
```  1904   show ?thesis
```
```  1905   proof
```
```  1906     show "k ` ({0..1} \<times> U) \<subseteq> C"
```
```  1907       using V*k VU by fastforce
```
```  1908     show "\<And>y. y \<in> U \<Longrightarrow> k (0, y) = f y"
```
```  1909       by (simp add: V*k)
```
```  1910     show "\<And>z. z \<in> {0..1} \<times> U \<Longrightarrow> h z = p (k z)"
```
```  1911       using V*k by auto
```
```  1912   qed (auto simp: contk)
```
```  1913 qed
```
```  1914
```
```  1915 corollary%important covering_space_lift_homotopy_alt:
```
```  1916   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  1917     and h :: "'c::real_normed_vector \<times> real \<Rightarrow> 'b"
```
```  1918   assumes cov: "covering_space C p S"
```
```  1919       and conth: "continuous_on (U \<times> {0..1}) h"
```
```  1920       and him: "h ` (U \<times> {0..1}) \<subseteq> S"
```
```  1921       and heq: "\<And>y. y \<in> U \<Longrightarrow> h (y,0) = p(f y)"
```
```  1922       and contf: "continuous_on U f" and fim: "f ` U \<subseteq> C"
```
```  1923   obtains k where "continuous_on (U \<times> {0..1}) k"
```
```  1924                   "k ` (U \<times> {0..1}) \<subseteq> C"
```
```  1925                   "\<And>y. y \<in> U \<Longrightarrow> k(y, 0) = f y"
```
```  1926                   "\<And>z. z \<in> U \<times> {0..1} \<Longrightarrow> h z = p(k z)"
```
```  1927 proof%unimportant -
```
```  1928   have "continuous_on ({0..1} \<times> U) (h \<circ> (\<lambda>z. (snd z, fst z)))"
```
```  1929     by (intro continuous_intros continuous_on_subset [OF conth]) auto
```
```  1930   then obtain k where contk: "continuous_on ({0..1} \<times> U) k"
```
```  1931                   and kim:  "k ` ({0..1} \<times> U) \<subseteq> C"
```
```  1932                   and k0: "\<And>y. y \<in> U \<Longrightarrow> k(0, y) = f y"
```
```  1933                   and heqp: "\<And>z. z \<in> {0..1} \<times> U \<Longrightarrow> (h \<circ> (\<lambda>z. Pair (snd z) (fst z))) z = p(k z)"
```
```  1934     apply (rule covering_space_lift_homotopy [OF cov _ _ _ contf fim])
```
```  1935     using him  by (auto simp: contf heq)
```
```  1936   show ?thesis
```
```  1937     apply (rule_tac k="k \<circ> (\<lambda>z. Pair (snd z) (fst z))" in that)
```
```  1938        apply (intro continuous_intros continuous_on_subset [OF contk])
```
```  1939     using kim heqp apply (auto simp: k0)
```
```  1940     done
```
```  1941 qed
```
```  1942
```
```  1943 corollary%important covering_space_lift_homotopic_function:
```
```  1944   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" and g:: "'c::real_normed_vector \<Rightarrow> 'a"
```
```  1945   assumes cov: "covering_space C p S"
```
```  1946       and contg: "continuous_on U g"
```
```  1947       and gim: "g ` U \<subseteq> C"
```
```  1948       and pgeq: "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
```
```  1949       and hom: "homotopic_with (\<lambda>x. True) U S f f'"
```
```  1950     obtains g' where "continuous_on U g'" "image g' U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g' y) = f' y"
```
```  1951 proof%unimportant -
```
```  1952   obtain h where conth: "continuous_on ({0..1::real} \<times> U) h"
```
```  1953              and him: "h ` ({0..1} \<times> U) \<subseteq> S"
```
```  1954              and h0:  "\<And>x. h(0, x) = f x"
```
```  1955              and h1: "\<And>x. h(1, x) = f' x"
```
```  1956     using hom by (auto simp: homotopic_with_def)
```
```  1957   have "\<And>y. y \<in> U \<Longrightarrow> h (0, y) = p (g y)"
```
```  1958     by (simp add: h0 pgeq)
```
```  1959   then obtain k where contk: "continuous_on ({0..1} \<times> U) k"
```
```  1960                   and kim: "k ` ({0..1} \<times> U) \<subseteq> C"
```
```  1961                   and k0: "\<And>y. y \<in> U \<Longrightarrow> k(0, y) = g y"
```
```  1962                   and heq: "\<And>z. z \<in> {0..1} \<times> U \<Longrightarrow> h z = p(k z)"
```
```  1963     using covering_space_lift_homotopy [OF cov conth him _ contg gim] by metis
```
```  1964   show ?thesis
```
```  1965   proof
```
```  1966     show "continuous_on U (k \<circ> Pair 1)"
```
```  1967       by (meson contk atLeastAtMost_iff continuous_on_o_Pair order_refl zero_le_one)
```
```  1968     show "(k \<circ> Pair 1) ` U \<subseteq> C"
```
```  1969       using kim by auto
```
```  1970     show "\<And>y. y \<in> U \<Longrightarrow> p ((k \<circ> Pair 1) y) = f' y"
```
```  1971       by (auto simp: h1 heq [symmetric])
```
```  1972   qed
```
```  1973 qed
```
```  1974
```
```  1975 corollary%important covering_space_lift_inessential_function:
```
```  1976   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" and U :: "'c::real_normed_vector set"
```
```  1977   assumes cov: "covering_space C p S"
```
```  1978       and hom: "homotopic_with (\<lambda>x. True) U S f (\<lambda>x. a)"
```
```  1979   obtains g where "continuous_on U g" "g ` U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
```
```  1980 proof%unimportant (cases "U = {}")
```
```  1981   case True
```
```  1982   then show ?thesis
```
```  1983     using that continuous_on_empty by blast
```
```  1984 next
```
```  1985   case False
```
```  1986   then obtain b where b: "b \<in> C" "p b = a"
```
```  1987     using covering_space_imp_surjective [OF cov] homotopic_with_imp_subset2 [OF hom]
```
```  1988     by auto
```
```  1989   then have gim: "(\<lambda>y. b) ` U \<subseteq> C"
```
```  1990     by blast
```
```  1991   show ?thesis
```
```  1992     apply (rule covering_space_lift_homotopic_function
```
```  1993                   [OF cov continuous_on_const gim _ homotopic_with_symD [OF hom]])
```
```  1994     using b that apply auto
```
```  1995     done
```
```  1996 qed
```
```  1997
```
```  1998 subsection%important\<open> Lifting of general functions to covering space\<close>
```
```  1999
```
```  2000 proposition%important covering_space_lift_path_strong:
```
```  2001   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  2002     and f :: "'c::real_normed_vector \<Rightarrow> 'b"
```
```  2003   assumes cov: "covering_space C p S" and "a \<in> C"
```
```  2004       and "path g" and pag: "path_image g \<subseteq> S" and pas: "pathstart g = p a"
```
```  2005     obtains h where "path h" "path_image h \<subseteq> C" "pathstart h = a"
```
```  2006                 and "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h t) = g t"
```
```  2007 proof%unimportant -
```
```  2008   obtain k:: "real \<times> 'c \<Rightarrow> 'a"
```
```  2009     where contk: "continuous_on ({0..1} \<times> {undefined}) k"
```
```  2010       and kim: "k ` ({0..1} \<times> {undefined}) \<subseteq> C"
```
```  2011       and k0:  "k (0, undefined) = a"
```
```  2012       and pk: "\<And>z. z \<in> {0..1} \<times> {undefined} \<Longrightarrow> p(k z) = (g \<circ> fst) z"
```
```  2013   proof (rule covering_space_lift_homotopy [OF cov, of "{undefined}" "g \<circ> fst"])
```
```  2014     show "continuous_on ({0..1::real} \<times> {undefined::'c}) (g \<circ> fst)"
```
```  2015       apply (intro continuous_intros)
```
```  2016       using \<open>path g\<close> by (simp add: path_def)
```
```  2017     show "(g \<circ> fst) ` ({0..1} \<times> {undefined}) \<subseteq> S"
```
```  2018       using pag by (auto simp: path_image_def)
```
```  2019     show "(g \<circ> fst) (0, y) = p a" if "y \<in> {undefined}" for y::'c
```
```  2020       by (metis comp_def fst_conv pas pathstart_def)
```
```  2021   qed (use assms in auto)
```
```  2022   show ?thesis
```
```  2023   proof
```
```  2024     show "path (k \<circ> (\<lambda>t. Pair t undefined))"
```
```  2025       unfolding path_def
```
```  2026       by (intro continuous_on_compose continuous_intros continuous_on_subset [OF contk]) auto
```
```  2027     show "path_image (k \<circ> (\<lambda>t. (t, undefined))) \<subseteq> C"
```
```  2028       using kim by (auto simp: path_image_def)
```
```  2029     show "pathstart (k \<circ> (\<lambda>t. (t, undefined))) = a"
```
```  2030       by (auto simp: pathstart_def k0)
```
```  2031     show "\<And>t. t \<in> {0..1} \<Longrightarrow> p ((k \<circ> (\<lambda>t. (t, undefined))) t) = g t"
```
```  2032       by (auto simp: pk)
```
```  2033   qed
```
```  2034 qed
```
```  2035
```
```  2036 corollary%important covering_space_lift_path:
```
```  2037   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  2038   assumes cov: "covering_space C p S" and "path g" and pig: "path_image g \<subseteq> S"
```
```  2039   obtains h where "path h" "path_image h \<subseteq> C" "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h t) = g t"
```
```  2040 proof%unimportant -
```
```  2041   obtain a where "a \<in> C" "pathstart g = p a"
```
```  2042     by (metis pig cov covering_space_imp_surjective imageE pathstart_in_path_image subsetCE)
```
```  2043   show ?thesis
```
```  2044     using covering_space_lift_path_strong [OF cov \<open>a \<in> C\<close> \<open>path g\<close> pig]
```
```  2045     by (metis \<open>pathstart g = p a\<close> that)
```
```  2046 qed
```
```  2047
```
```  2048
```
```  2049 proposition%important covering_space_lift_homotopic_paths:
```
```  2050   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  2051   assumes cov: "covering_space C p S"
```
```  2052       and "path g1" and pig1: "path_image g1 \<subseteq> S"
```
```  2053       and "path g2" and pig2: "path_image g2 \<subseteq> S"
```
```  2054       and hom: "homotopic_paths S g1 g2"
```
```  2055       and "path h1" and pih1: "path_image h1 \<subseteq> C" and ph1: "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h1 t) = g1 t"
```
```  2056       and "path h2" and pih2: "path_image h2 \<subseteq> C" and ph2: "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h2 t) = g2 t"
```
```  2057       and h1h2: "pathstart h1 = pathstart h2"
```
```  2058     shows "homotopic_paths C h1 h2"
```
```  2059 proof%unimportant -
```
```  2060   obtain h :: "real \<times> real \<Rightarrow> 'b"
```
```  2061      where conth: "continuous_on ({0..1} \<times> {0..1}) h"
```
```  2062        and him: "h ` ({0..1} \<times> {0..1}) \<subseteq> S"
```
```  2063        and h0: "\<And>x. h (0, x) = g1 x" and h1: "\<And>x. h (1, x) = g2 x"
```
```  2064        and heq0: "\<And>t. t \<in> {0..1} \<Longrightarrow> h (t, 0) = g1 0"
```
```  2065        and heq1: "\<And>t. t \<in> {0..1} \<Longrightarrow> h (t, 1) = g1 1"
```
```  2066     using hom by (auto simp: homotopic_paths_def homotopic_with_def pathstart_def pathfinish_def)
```
```  2067   obtain k where contk: "continuous_on ({0..1} \<times> {0..1}) k"
```
```  2068              and kim: "k ` ({0..1} \<times> {0..1}) \<subseteq> C"
```
```  2069              and kh2: "\<And>y. y \<in> {0..1} \<Longrightarrow> k (y, 0) = h2 0"
```
```  2070              and hpk: "\<And>z. z \<in> {0..1} \<times> {0..1} \<Longrightarrow> h z = p (k z)"
```
```  2071     apply (rule covering_space_lift_homotopy_alt [OF cov conth him, of "\<lambda>x. h2 0"])
```
```  2072     using h1h2 ph1 ph2 apply (force simp: heq0 pathstart_def pathfinish_def)
```
```  2073     using path_image_def pih2 continuous_on_const by fastforce+
```
```  2074   have contg1: "continuous_on {0..1} g1" and contg2: "continuous_on {0..1} g2"
```
```  2075     using \<open>path g1\<close> \<open>path g2\<close> path_def by blast+
```
```  2076   have g1im: "g1 ` {0..1} \<subseteq> S" and g2im: "g2 ` {0..1} \<subseteq> S"
```
```  2077     using path_image_def pig1 pig2 by auto
```
```  2078   have conth1: "continuous_on {0..1} h1" and conth2: "continuous_on {0..1} h2"
```
```  2079     using \<open>path h1\<close> \<open>path h2\<close> path_def by blast+
```
```  2080   have h1im: "h1 ` {0..1} \<subseteq> C" and h2im: "h2 ` {0..1} \<subseteq> C"
```
```  2081     using path_image_def pih1 pih2 by auto
```
```  2082   show ?thesis
```
```  2083     unfolding homotopic_paths pathstart_def pathfinish_def
```
```  2084   proof (intro exI conjI ballI)
```
```  2085     show keqh1: "k(0, x) = h1 x" if "x \<in> {0..1}" for x
```
```  2086     proof (rule covering_space_lift_unique [OF cov _ contg1 g1im])
```
```  2087       show "k (0,0) = h1 0"
```
```  2088         by (metis atLeastAtMost_iff h1h2 kh2 order_refl pathstart_def zero_le_one)
```
```  2089       show "continuous_on {0..1} (\<lambda>a. k (0, a))"
```
```  2090         by (intro continuous_intros continuous_on_compose2 [OF contk]) auto
```
```  2091       show "\<And>x. x \<in> {0..1} \<Longrightarrow> g1 x = p (k (0, x))"
```
```  2092         by (metis atLeastAtMost_iff h0 hpk zero_le_one mem_Sigma_iff order_refl)
```
```  2093     qed (use conth1 h1im kim that in \<open>auto simp: ph1\<close>)
```
```  2094     show "k(1, x) = h2 x" if "x \<in> {0..1}" for x
```
```  2095     proof (rule covering_space_lift_unique [OF cov _ contg2 g2im])
```
```  2096       show "k (1,0) = h2 0"
```
```  2097         by (metis atLeastAtMost_iff kh2 order_refl zero_le_one)
```
```  2098       show "continuous_on {0..1} (\<lambda>a. k (1, a))"
```
```  2099         by (intro continuous_intros continuous_on_compose2 [OF contk]) auto
```
```  2100       show "\<And>x. x \<in> {0..1} \<Longrightarrow> g2 x = p (k (1, x))"
```
```  2101         by (metis atLeastAtMost_iff h1 hpk mem_Sigma_iff order_refl zero_le_one)
```
```  2102     qed (use conth2 h2im kim that in \<open>auto simp: ph2\<close>)
```
```  2103     show "\<And>t. t \<in> {0..1} \<Longrightarrow> (k \<circ> Pair t) 0 = h1 0"
```
```  2104       by (metis comp_apply h1h2 kh2 pathstart_def)
```
```  2105     show "(k \<circ> Pair t) 1 = h1 1" if "t \<in> {0..1}" for t
```
```  2106     proof (rule covering_space_lift_unique
```
```  2107            [OF cov, of "\<lambda>a. (k \<circ> Pair a) 1" 0 "\<lambda>a. h1 1" "{0..1}"  "\<lambda>x. g1 1"])
```
```  2108       show "(k \<circ> Pair 0) 1 = h1 1"
```
```  2109         using keqh1 by auto
```
```  2110       show "continuous_on {0..1} (\<lambda>a. (k \<circ> Pair a) 1)"
```
```  2111         apply simp
```
```  2112         by (intro continuous_intros continuous_on_compose2 [OF contk]) auto
```
```  2113       show "\<And>x. x \<in> {0..1} \<Longrightarrow> g1 1 = p ((k \<circ> Pair x) 1)"
```
```  2114         using heq1 hpk by auto
```
```  2115     qed (use contk kim g1im h1im that in \<open>auto simp: ph1 continuous_on_const\<close>)
```
```  2116   qed (use contk kim in auto)
```
```  2117 qed
```
```  2118
```
```  2119
```
```  2120 corollary%important covering_space_monodromy:
```
```  2121   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  2122   assumes cov: "covering_space C p S"
```
```  2123       and "path g1" and pig1: "path_image g1 \<subseteq> S"
```
```  2124       and "path g2" and pig2: "path_image g2 \<subseteq> S"
```
```  2125       and hom: "homotopic_paths S g1 g2"
```
```  2126       and "path h1" and pih1: "path_image h1 \<subseteq> C" and ph1: "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h1 t) = g1 t"
```
```  2127       and "path h2" and pih2: "path_image h2 \<subseteq> C" and ph2: "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h2 t) = g2 t"
```
```  2128       and h1h2: "pathstart h1 = pathstart h2"
```
```  2129     shows "pathfinish h1 = pathfinish h2"
```
```  2130   using%unimportant covering_space_lift_homotopic_paths [OF assms] homotopic_paths_imp_pathfinish
```
```  2131   by%unimportant blast
```
```  2132
```
```  2133
```
```  2134 corollary%important covering_space_lift_homotopic_path:
```
```  2135   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  2136   assumes cov: "covering_space C p S"
```
```  2137       and hom: "homotopic_paths S f f'"
```
```  2138       and "path g" and pig: "path_image g \<subseteq> C"
```
```  2139       and a: "pathstart g = a" and b: "pathfinish g = b"
```
```  2140       and pgeq: "\<And>t. t \<in> {0..1} \<Longrightarrow> p(g t) = f t"
```
```  2141   obtains g' where "path g'" "path_image g' \<subseteq> C"
```
```  2142                    "pathstart g' = a" "pathfinish g' = b" "\<And>t. t \<in> {0..1} \<Longrightarrow> p(g' t) = f' t"
```
```  2143 proof%unimportant (rule covering_space_lift_path_strong [OF cov, of a f'])
```
```  2144   show "a \<in> C"
```
```  2145     using a pig by auto
```
```  2146   show "path f'" "path_image f' \<subseteq> S"
```
```  2147     using hom homotopic_paths_imp_path homotopic_paths_imp_subset by blast+
```
```  2148   show "pathstart f' = p a"
```
```  2149     by (metis a atLeastAtMost_iff hom homotopic_paths_imp_pathstart order_refl pathstart_def pgeq zero_le_one)
```
```  2150 qed (metis (mono_tags, lifting) assms cov covering_space_monodromy hom homotopic_paths_imp_path homotopic_paths_imp_subset pgeq pig)
```
```  2151
```
```  2152
```
```  2153 proposition%important covering_space_lift_general:
```
```  2154   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  2155     and f :: "'c::real_normed_vector \<Rightarrow> 'b"
```
```  2156   assumes cov: "covering_space C p S" and "a \<in> C" "z \<in> U"
```
```  2157       and U: "path_connected U" "locally path_connected U"
```
```  2158       and contf: "continuous_on U f" and fim: "f ` U \<subseteq> S"
```
```  2159       and feq: "f z = p a"
```
```  2160       and hom: "\<And>r. \<lbrakk>path r; path_image r \<subseteq> U; pathstart r = z; pathfinish r = z\<rbrakk>
```
```  2161                      \<Longrightarrow> \<exists>q. path q \<and> path_image q \<subseteq> C \<and>
```
```  2162                              pathstart q = a \<and> pathfinish q = a \<and>
```
```  2163                              homotopic_paths S (f \<circ> r) (p \<circ> q)"
```
```  2164   obtains g where "continuous_on U g" "g ` U \<subseteq> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
```
```  2165 proof%unimportant -
```
```  2166   have *: "\<exists>g h. path g \<and> path_image g \<subseteq> U \<and>
```
```  2167                  pathstart g = z \<and> pathfinish g = y \<and>
```
```  2168                  path h \<and> path_image h \<subseteq> C \<and> pathstart h = a \<and>
```
```  2169                  (\<forall>t \<in> {0..1}. p(h t) = f(g t))"
```
```  2170           if "y \<in> U" for y
```
```  2171   proof -
```
```  2172     obtain g where "path g" "path_image g \<subseteq> U" and pastg: "pathstart g = z"
```
```  2173                and pafig: "pathfinish g = y"
```
```  2174       using U \<open>z \<in> U\<close> \<open>y \<in> U\<close> by (force simp: path_connected_def)
```
```  2175     obtain h where "path h" "path_image h \<subseteq> C" "pathstart h = a"
```
```  2176                and "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h t) = (f \<circ> g) t"
```
```  2177     proof (rule covering_space_lift_path_strong [OF cov \<open>a \<in> C\<close>])
```
```  2178       show "path (f \<circ> g)"
```
```  2179         using \<open>path g\<close> \<open>path_image g \<subseteq> U\<close> contf continuous_on_subset path_continuous_image by blast
```
```  2180       show "path_image (f \<circ> g) \<subseteq> S"
```
```  2181         by (metis \<open>path_image g \<subseteq> U\<close> fim image_mono path_image_compose subset_trans)
```
```  2182       show "pathstart (f \<circ> g) = p a"
```
```  2183         by (simp add: feq pastg pathstart_compose)
```
```  2184     qed auto
```
```  2185     then show ?thesis
```
```  2186       by (metis \<open>path g\<close> \<open>path_image g \<subseteq> U\<close> comp_apply pafig pastg)
```
```  2187   qed
```
```  2188   have "\<exists>l. \<forall>g h. path g \<and> path_image g \<subseteq> U \<and> pathstart g = z \<and> pathfinish g = y \<and>
```
```  2189                   path h \<and> path_image h \<subseteq> C \<and> pathstart h = a \<and>
```
```  2190                   (\<forall>t \<in> {0..1}. p(h t) = f(g t))  \<longrightarrow> pathfinish h = l" for y
```
```  2191   proof -
```
```  2192     have "pathfinish h = pathfinish h'"
```
```  2193          if g: "path g" "path_image g \<subseteq> U" "pathstart g = z" "pathfinish g = y"
```
```  2194             and h: "path h" "path_image h \<subseteq> C" "pathstart h = a"
```
```  2195             and phg: "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h t) = f(g t)"
```
```  2196             and g': "path g'" "path_image g' \<subseteq> U" "pathstart g' = z" "pathfinish g' = y"
```
```  2197             and h': "path h'" "path_image h' \<subseteq> C" "pathstart h' = a"
```
```  2198             and phg': "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h' t) = f(g' t)"
```
```  2199          for g h g' h'
```
```  2200     proof -
```
```  2201       obtain q where "path q" and piq: "path_image q \<subseteq> C" and pastq: "pathstart q = a" and pafiq: "pathfinish q = a"
```
```  2202                  and homS: "homotopic_paths S (f \<circ> g +++ reversepath g') (p \<circ> q)"
```
```  2203         using g g' hom [of "g +++ reversepath g'"] by (auto simp:  subset_path_image_join)
```
```  2204               have papq: "path (p \<circ> q)"
```
```  2205                 using homS homotopic_paths_imp_path by blast
```
```  2206               have pipq: "path_image (p \<circ> q) \<subseteq> S"
```
```  2207                 using homS homotopic_paths_imp_subset by blast
```
```  2208       obtain q' where "path q'" "path_image q' \<subseteq> C"
```
```  2209                 and "pathstart q' = pathstart q" "pathfinish q' = pathfinish q"
```
```  2210                 and pq'_eq: "\<And>t. t \<in> {0..1} \<Longrightarrow> p (q' t) = (f \<circ> g +++ reversepath g') t"
```
```  2211         using covering_space_lift_homotopic_path [OF cov homotopic_paths_sym [OF homS] \<open>path q\<close> piq refl refl]
```
```  2212         by auto
```
```  2213       have "q' t = (h \<circ> (*\<^sub>R) 2) t" if "0 \<le> t" "t \<le> 1/2" for t
```
```  2214       proof (rule covering_space_lift_unique [OF cov, of q' 0 "h \<circ> (*\<^sub>R) 2" "{0..1/2}" "f \<circ> g \<circ> (*\<^sub>R) 2" t])
```
```  2215         show "q' 0 = (h \<circ> (*\<^sub>R) 2) 0"
```
```  2216           by (metis \<open>pathstart q' = pathstart q\<close> comp_def g h pastq pathstart_def pth_4(2))
```
```  2217         show "continuous_on {0..1/2} (f \<circ> g \<circ> (*\<^sub>R) 2)"
```
```  2218           apply (intro continuous_intros continuous_on_compose continuous_on_path [OF \<open>path g\<close>] continuous_on_subset [OF contf])
```
```  2219           using g(2) path_image_def by fastforce+
```
```  2220         show "(f \<circ> g \<circ> (*\<^sub>R) 2) ` {0..1/2} \<subseteq> S"
```
```  2221           using g(2) path_image_def fim by fastforce
```
```  2222         show "(h \<circ> (*\<^sub>R) 2) ` {0..1/2} \<subseteq> C"
```
```  2223           using h path_image_def by fastforce
```
```  2224         show "q' ` {0..1/2} \<subseteq> C"
```
```  2225           using \<open>path_image q' \<subseteq> C\<close> path_image_def by fastforce
```
```  2226         show "\<And>x. x \<in> {0..1/2} \<Longrightarrow> (f \<circ> g \<circ> (*\<^sub>R) 2) x = p (q' x)"
```
```  2227           by (auto simp: joinpaths_def pq'_eq)
```
```  2228         show "\<And>x. x \<in> {0..1/2} \<Longrightarrow> (f \<circ> g \<circ> (*\<^sub>R) 2) x = p ((h \<circ> (*\<^sub>R) 2) x)"
```
```  2229           by (simp add: phg)
```
```  2230         show "continuous_on {0..1/2} q'"
```
```  2231           by (simp add: continuous_on_path \<open>path q'\<close>)
```
```  2232         show "continuous_on {0..1/2} (h \<circ> (*\<^sub>R) 2)"
```
```  2233           apply (intro continuous_intros continuous_on_compose continuous_on_path [OF \<open>path h\<close>], force)
```
```  2234           done
```
```  2235       qed (use that in auto)
```
```  2236       moreover have "q' t = (reversepath h' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1)) t" if "1/2 < t" "t \<le> 1" for t
```
```  2237       proof (rule covering_space_lift_unique [OF cov, of q' 1 "reversepath h' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1)" "{1/2<..1}" "f \<circ> reversepath g' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1)" t])
```
```  2238         show "q' 1 = (reversepath h' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1)) 1"
```
```  2239           using h' \<open>pathfinish q' = pathfinish q\<close> pafiq
```
```  2240           by (simp add: pathstart_def pathfinish_def reversepath_def)
```
```  2241         show "continuous_on {1/2<..1} (f \<circ> reversepath g' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1))"
```
```  2242           apply (intro continuous_intros continuous_on_compose continuous_on_path \<open>path g'\<close> continuous_on_subset [OF contf])
```
```  2243           using g' apply simp_all
```
```  2244           by (auto simp: path_image_def reversepath_def)
```
```  2245         show "(f \<circ> reversepath g' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1)) ` {1/2<..1} \<subseteq> S"
```
```  2246           using g'(2) path_image_def fim by (auto simp: image_subset_iff path_image_def reversepath_def)
```
```  2247         show "q' ` {1/2<..1} \<subseteq> C"
```
```  2248           using \<open>path_image q' \<subseteq> C\<close> path_image_def by fastforce
```
```  2249         show "(reversepath h' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1)) ` {1/2<..1} \<subseteq> C"
```
```  2250           using h' by (simp add: path_image_def reversepath_def subset_eq)
```
```  2251         show "\<And>x. x \<in> {1/2<..1} \<Longrightarrow> (f \<circ> reversepath g' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1)) x = p (q' x)"
```
```  2252           by (auto simp: joinpaths_def pq'_eq)
```
```  2253         show "\<And>x. x \<in> {1/2<..1} \<Longrightarrow>
```
```  2254                   (f \<circ> reversepath g' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1)) x = p ((reversepath h' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1)) x)"
```
```  2255           by (simp add: phg' reversepath_def)
```
```  2256         show "continuous_on {1/2<..1} q'"
```
```  2257           by (auto intro: continuous_on_path [OF \<open>path q'\<close>])
```
```  2258         show "continuous_on {1/2<..1} (reversepath h' \<circ> (\<lambda>t. 2 *\<^sub>R t - 1))"
```
```  2259           apply (intro continuous_intros continuous_on_compose continuous_on_path \<open>path h'\<close>)
```
```  2260           using h' apply auto
```
```  2261           done
```
```  2262       qed (use that in auto)
```
```  2263       ultimately have "q' t = (h +++ reversepath h') t" if "0 \<le> t" "t \<le> 1" for t
```
```  2264         using that by (simp add: joinpaths_def)
```
```  2265       then have "path(h +++ reversepath h')"
```
```  2266         by (auto intro: path_eq [OF \<open>path q'\<close>])
```
```  2267       then show ?thesis
```
```  2268         by (auto simp: \<open>path h\<close> \<open>path h'\<close>)
```
```  2269     qed
```
```  2270     then show ?thesis by metis
```
```  2271   qed
```
```  2272   then obtain l :: "'c \<Rightarrow> 'a"
```
```  2273           where l: "\<And>y g h. \<lbrakk>path g; path_image g \<subseteq> U; pathstart g = z; pathfinish g = y;
```
```  2274                              path h; path_image h \<subseteq> C; pathstart h = a;
```
```  2275                              \<And>t. t \<in> {0..1} \<Longrightarrow> p(h t) = f(g t)\<rbrakk> \<Longrightarrow> pathfinish h = l y"
```
```  2276     by metis
```
```  2277   show ?thesis
```
```  2278   proof
```
```  2279     show pleq: "p (l y) = f y" if "y \<in> U" for y
```
```  2280       using*[OF \<open>y \<in> U\<close>]  by (metis l atLeastAtMost_iff order_refl pathfinish_def zero_le_one)
```
```  2281     show "l z = a"
```
```  2282       using l [of "linepath z z" z "linepath a a"] by (auto simp: assms)
```
```  2283     show LC: "l ` U \<subseteq> C"
```
```  2284       by (clarify dest!: *) (metis (full_types) l pathfinish_in_path_image subsetCE)
```
```  2285     have "\<exists>T. openin (subtopology euclidean U) T \<and> y \<in> T \<and> T \<subseteq> U \<inter> l -` X"
```
```  2286          if X: "openin (subtopology euclidean C) X" and "y \<in> U" "l y \<in> X" for X y
```
```  2287     proof -
```
```  2288       have "X \<subseteq> C"
```
```  2289         using X openin_euclidean_subtopology_iff by blast
```
```  2290       have "f y \<in> S"
```
```  2291         using fim \<open>y \<in> U\<close> by blast
```
```  2292       then obtain W \<V>
```
```  2293               where WV: "f y \<in> W \<and> openin (subtopology euclidean S) W \<and>
```
```  2294                          (\<Union>\<V> = C \<inter> p -` W \<and>
```
```  2295                           (\<forall>U \<in> \<V>. openin (subtopology euclidean C) U) \<and>
```
```  2296                           pairwise disjnt \<V> \<and>
```
```  2297                           (\<forall>U \<in> \<V>. \<exists>q. homeomorphism U W p q))"
```
```  2298         using cov by (force simp: covering_space_def)
```
```  2299       then have "l y \<in> \<Union>\<V>"
```
```  2300         using \<open>X \<subseteq> C\<close> pleq that by auto
```
```  2301       then obtain W' where "l y \<in> W'" and "W' \<in> \<V>"
```
```  2302         by blast
```
```  2303       with WV obtain p' where opeCW': "openin (subtopology euclidean C) W'"
```
```  2304                           and homUW': "homeomorphism W' W p p'"
```
```  2305         by blast
```
```  2306       then have contp': "continuous_on W p'" and p'im: "p' ` W \<subseteq> W'"
```
```  2307         using homUW' homeomorphism_image2 homeomorphism_cont2 by fastforce+
```
```  2308       obtain V where "y \<in> V" "y \<in> U" and fimW: "f ` V \<subseteq> W" "V \<subseteq> U"
```
```  2309                  and "path_connected V" and opeUV: "openin (subtopology euclidean U) V"
```
```  2310       proof -
```
```  2311         have "openin (subtopology euclidean U) (U \<inter> f -` W)"
```
```  2312           using WV contf continuous_on_open_gen fim by auto
```
```  2313         then show ?thesis
```
```  2314           using U WV
```
```  2315           apply (auto simp: locally_path_connected)
```
```  2316           apply (drule_tac x="U \<inter> f -` W" in spec)
```
```  2317           apply (drule_tac x=y in spec)
```
```  2318           apply (auto simp: \<open>y \<in> U\<close> intro: that)
```
```  2319           done
```
```  2320       qed
```
```  2321       have "W' \<subseteq> C" "W \<subseteq> S"
```
```  2322         using opeCW' WV openin_imp_subset by auto
```
```  2323       have p'im: "p' ` W \<subseteq> W'"
```
```  2324         using homUW' homeomorphism_image2 by fastforce
```
```  2325       show ?thesis
```
```  2326       proof (intro exI conjI)
```
```  2327         have "openin (subtopology euclidean S) (W \<inter> p' -` (W' \<inter> X))"
```
```  2328         proof (rule openin_trans)
```
```  2329           show "openin (subtopology euclidean W) (W \<inter> p' -` (W' \<inter> X))"
```
```  2330             apply (rule continuous_openin_preimage [OF contp' p'im])
```
```  2331             using X \<open>W' \<subseteq> C\<close> apply (auto simp: openin_open)
```
```  2332             done
```
```  2333           show "openin (subtopology euclidean S) W"
```
```  2334             using WV by blast
```
```  2335         qed
```
```  2336         then show "openin (subtopology euclidean U) (V \<inter> (U \<inter> (f -` (W \<inter> (p' -` (W' \<inter> X))))))"
```
```  2337           by (blast intro: opeUV openin_subtopology_self continuous_openin_preimage [OF contf fim])
```
```  2338          have "p' (f y) \<in> X"
```
```  2339           using \<open>l y \<in> W'\<close> homeomorphism_apply1 [OF homUW'] pleq \<open>y \<in> U\<close> \<open>l y \<in> X\<close> by fastforce
```
```  2340         then show "y \<in> V \<inter> (U \<inter> f -` (W \<inter> p' -` (W' \<inter> X)))"
```
```  2341           using \<open>y \<in> U\<close> \<open>y \<in> V\<close> WV p'im by auto
```
```  2342         show "V \<inter> (U \<inter> f -` (W \<inter> p' -` (W' \<inter> X))) \<subseteq> U \<inter> l -` X"
```
```  2343         proof (intro subsetI IntI; clarify)
```
```  2344           fix y'
```
```  2345           assume y': "y' \<in> V" "y' \<in> U" "f y' \<in> W" "p' (f y') \<in> W'" "p' (f y') \<in> X"
```
```  2346           then obtain \<gamma> where "path \<gamma>" "path_image \<gamma> \<subseteq> V" "pathstart \<gamma> = y" "pathfinish \<gamma> = y'"
```
```  2347             by (meson \<open>path_connected V\<close> \<open>y \<in> V\<close> path_connected_def)
```
```  2348           obtain pp qq where "path pp" "path_image pp \<subseteq> U"
```
```  2349                              "pathstart pp = z" "pathfinish pp = y"
```
```  2350                              "path qq" "path_image qq \<subseteq> C" "pathstart qq = a"
```
```  2351                          and pqqeq: "\<And>t. t \<in> {0..1} \<Longrightarrow> p(qq t) = f(pp t)"
```
```  2352             using*[OF \<open>y \<in> U\<close>] by blast
```
```  2353           have finW: "\<And>x. \<lbrakk>0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> f (\<gamma> x) \<in> W"
```
```  2354             using \<open>path_image \<gamma> \<subseteq> V\<close> by (auto simp: image_subset_iff path_image_def fimW [THEN subsetD])
```
```  2355           have "pathfinish (qq +++ (p' \<circ> f \<circ> \<gamma>)) = l y'"
```
```  2356           proof (rule l [of "pp +++ \<gamma>" y' "qq +++ (p' \<circ> f \<circ> \<gamma>)"])
```
```  2357             show "path (pp +++ \<gamma>)"
```
```  2358               by (simp add: \<open>path \<gamma>\<close> \<open>path pp\<close> \<open>pathfinish pp = y\<close> \<open>pathstart \<gamma> = y\<close>)
```
```  2359             show "path_image (pp +++ \<gamma>) \<subseteq> U"
```
```  2360               using \<open>V \<subseteq> U\<close> \<open>path_image \<gamma> \<subseteq> V\<close> \<open>path_image pp \<subseteq> U\<close> not_in_path_image_join by blast
```
```  2361             show "pathstart (pp +++ \<gamma>) = z"
```
```  2362               by (simp add: \<open>pathstart pp = z\<close>)
```
```  2363             show "pathfinish (pp +++ \<gamma>) = y'"
```
```  2364               by (simp add: \<open>pathfinish \<gamma> = y'\<close>)
```
```  2365             have paqq: "pathfinish qq = pathstart (p' \<circ> f \<circ> \<gamma>)"
```
```  2366               apply (simp add: \<open>pathstart \<gamma> = y\<close> pathstart_compose)
```
```  2367               apply (metis (mono_tags, lifting) \<open>l y \<in> W'\<close> \<open>path pp\<close> \<open>path qq\<close> \<open>path_image pp \<subseteq> U\<close> \<open>path_image qq \<subseteq> C\<close>
```
```  2368                            \<open>pathfinish pp = y\<close> \<open>pathstart pp = z\<close> \<open>pathstart qq = a\<close>
```
```  2369                            homeomorphism_apply1 [OF homUW'] l pleq pqqeq \<open>y \<in> U\<close>)
```
```  2370               done
```
```  2371             have "continuous_on (path_image \<gamma>) (p' \<circ> f)"
```
```  2372             proof (rule continuous_on_compose)
```
```  2373               show "continuous_on (path_image \<gamma>) f"
```
```  2374                 using \<open>path_image \<gamma> \<subseteq> V\<close> \<open>V \<subseteq> U\<close> contf continuous_on_subset by blast
```
```  2375               show "continuous_on (f ` path_image \<gamma>) p'"
```
```  2376                 apply (rule continuous_on_subset [OF contp'])
```
```  2377                 apply (auto simp: path_image_def pathfinish_def pathstart_def finW)
```
```  2378                 done
```
```  2379             qed
```
```  2380             then show "path (qq +++ (p' \<circ> f \<circ> \<gamma>))"
```
```  2381               using \<open>path \<gamma>\<close> \<open>path qq\<close> paqq path_continuous_image path_join_imp by blast
```
```  2382             show "path_image (qq +++ (p' \<circ> f \<circ> \<gamma>)) \<subseteq> C"
```
```  2383               apply (rule subset_path_image_join)
```
```  2384                apply (simp add: \<open>path_image qq \<subseteq> C\<close>)
```
```  2385               by (metis \<open>W' \<subseteq> C\<close> \<open>path_image \<gamma> \<subseteq> V\<close> dual_order.trans fimW(1) image_comp image_mono p'im path_image_compose)
```
```  2386             show "pathstart (qq +++ (p' \<circ> f \<circ> \<gamma>)) = a"
```
```  2387               by (simp add: \<open>pathstart qq = a\<close>)
```
```  2388             show "p ((qq +++ (p' \<circ> f \<circ> \<gamma>)) \<xi>) = f ((pp +++ \<gamma>) \<xi>)" if \<xi>: "\<xi> \<in> {0..1}" for \<xi>
```
```  2389             proof (simp add: joinpaths_def, safe)
```
```  2390               show "p (qq (2*\<xi>)) = f (pp (2*\<xi>))" if "\<xi>*2 \<le> 1"
```
```  2391                 using \<open>\<xi> \<in> {0..1}\<close> pqqeq that by auto
```
```  2392               show "p (p' (f (\<gamma> (2*\<xi> - 1)))) = f (\<gamma> (2*\<xi> - 1))" if "\<not> \<xi>*2 \<le> 1"
```
```  2393                 apply (rule homeomorphism_apply2 [OF homUW' finW])
```
```  2394                 using that \<xi> by auto
```
```  2395             qed
```
```  2396           qed
```
```  2397           with \<open>pathfinish \<gamma> = y'\<close>  \<open>p' (f y') \<in> X\<close> show "y' \<in> l -` X"
```
```  2398             unfolding pathfinish_join by (simp add: pathfinish_def)
```
```  2399         qed
```
```  2400       qed
```
```  2401     qed
```
```  2402     then show "continuous_on U l"
```
```  2403       by (metis IntD1 IntD2 vimage_eq openin_subopen continuous_on_open_gen [OF LC])
```
```  2404   qed
```
```  2405 qed
```
```  2406
```
```  2407
```
```  2408 corollary%important covering_space_lift_stronger:
```
```  2409   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  2410     and f :: "'c::real_normed_vector \<Rightarrow> 'b"
```
```  2411   assumes cov: "covering_space C p S" "a \<in> C" "z \<in> U"
```
```  2412       and U: "path_connected U" "locally path_connected U"
```
```  2413       and contf: "continuous_on U f" and fim: "f ` U \<subseteq> S"
```
```  2414       and feq: "f z = p a"
```
```  2415       and hom: "\<And>r. \<lbrakk>path r; path_image r \<subseteq> U; pathstart r = z; pathfinish r = z\<rbrakk>
```
```  2416                      \<Longrightarrow> \<exists>b. homotopic_paths S (f \<circ> r) (linepath b b)"
```
```  2417   obtains g where "continuous_on U g" "g ` U \<subseteq> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
```
```  2418 proof%unimportant (rule covering_space_lift_general [OF cov U contf fim feq])
```
```  2419   fix r
```
```  2420   assume "path r" "path_image r \<subseteq> U" "pathstart r = z" "pathfinish r = z"
```
```  2421   then obtain b where b: "homotopic_paths S (f \<circ> r) (linepath b b)"
```
```  2422     using hom by blast
```
```  2423   then have "f (pathstart r) = b"
```
```  2424     by (metis homotopic_paths_imp_pathstart pathstart_compose pathstart_linepath)
```
```  2425   then have "homotopic_paths S (f \<circ> r) (linepath (f z) (f z))"
```
```  2426     by (simp add: b \<open>pathstart r = z\<close>)
```
```  2427   then have "homotopic_paths S (f \<circ> r) (p \<circ> linepath a a)"
```
```  2428     by (simp add: o_def feq linepath_def)
```
```  2429   then show "\<exists>q. path q \<and>
```
```  2430                   path_image q \<subseteq> C \<and>
```
```  2431                   pathstart q = a \<and> pathfinish q = a \<and> homotopic_paths S (f \<circ> r) (p \<circ> q)"
```
```  2432     by (force simp: \<open>a \<in> C\<close>)
```
```  2433 qed auto
```
```  2434
```
```  2435 corollary%important covering_space_lift_strong:
```
```  2436   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  2437     and f :: "'c::real_normed_vector \<Rightarrow> 'b"
```
```  2438   assumes cov: "covering_space C p S" "a \<in> C" "z \<in> U"
```
```  2439       and scU: "simply_connected U" and lpcU: "locally path_connected U"
```
```  2440       and contf: "continuous_on U f" and fim: "f ` U \<subseteq> S"
```
```  2441       and feq: "f z = p a"
```
```  2442   obtains g where "continuous_on U g" "g ` U \<subseteq> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
```
```  2443 proof%unimportant (rule covering_space_lift_stronger [OF cov _ lpcU contf fim feq])
```
```  2444   show "path_connected U"
```
```  2445     using scU simply_connected_eq_contractible_loop_some by blast
```
```  2446   fix r
```
```  2447   assume r: "path r" "path_image r \<subseteq> U" "pathstart r = z" "pathfinish r = z"
```
```  2448   have "linepath (f z) (f z) = f \<circ> linepath z z"
```
```  2449     by (simp add: o_def linepath_def)
```
```  2450   then have "homotopic_paths S (f \<circ> r) (linepath (f z) (f z))"
```
```  2451     by (metis r contf fim homotopic_paths_continuous_image scU simply_connected_eq_contractible_path)
```
```  2452   then show "\<exists>b. homotopic_paths S (f \<circ> r) (linepath b b)"
```
```  2453     by blast
```
```  2454 qed blast
```
```  2455
```
```  2456 corollary%important covering_space_lift:
```
```  2457   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
```
```  2458     and f :: "'c::real_normed_vector \<Rightarrow> 'b"
```
```  2459   assumes cov: "covering_space C p S"
```
```  2460       and U: "simply_connected U"  "locally path_connected U"
```
```  2461       and contf: "continuous_on U f" and fim: "f ` U \<subseteq> S"
```
```  2462     obtains g where "continuous_on U g" "g ` U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
```
```  2463 proof%unimportant (cases "U = {}")
```
```  2464   case True
```
```  2465   with that show ?thesis by auto
```
```  2466 next
```
```  2467   case False
```
```  2468   then obtain z where "z \<in> U" by blast
```
```  2469   then obtain a where "a \<in> C" "f z = p a"
```
```  2470     by (metis cov covering_space_imp_surjective fim image_iff image_subset_iff)
```
```  2471   then show ?thesis
```
```  2472     by (metis that covering_space_lift_strong [OF cov _ \<open>z \<in> U\<close> U contf fim])
```
```  2473 qed
```
```  2474
```
```  2475 end
```