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