src/HOL/Analysis/Homeomorphism.thy
author paulson <lp15@cam.ac.uk>
Tue Sep 27 16:24:53 2016 +0100 (2016-09-27)
changeset 63945 444eafb6e864
parent 63918 6bf55e6e0b75
child 64267 b9a1486e79be
permissions -rw-r--r--
a few new theorems and a renaming
hoelzl@63627
     1
(*  Title:      HOL/Analysis/Homeomorphism.thy
lp15@63130
     2
    Author: LC Paulson (ported from HOL Light)
lp15@63130
     3
*)
lp15@63130
     4
lp15@63130
     5
section \<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
lp15@63130
    11
subsection \<open>Homeomorphism of all convex compact sets with nonempty interior\<close>
lp15@63130
    12
lp15@63130
    13
proposition ray_to_rel_frontier:
lp15@63130
    14
  fixes a :: "'a::real_inner"
lp15@63130
    15
  assumes "bounded S"
lp15@63130
    16
      and a: "a \<in> rel_interior S"
lp15@63130
    17
      and aff: "(a + l) \<in> affine hull S"
lp15@63130
    18
      and "l \<noteq> 0"
lp15@63130
    19
  obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> rel_frontier S"
lp15@63130
    20
           "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> rel_interior S"
lp15@63130
    21
proof -
lp15@63130
    22
  have aaff: "a \<in> affine hull S"
lp15@63130
    23
    by (meson a hull_subset rel_interior_subset rev_subsetD)
lp15@63130
    24
  let ?D = "{d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}"
lp15@63130
    25
  obtain B where "B > 0" and B: "S \<subseteq> ball a B"
lp15@63130
    26
    using bounded_subset_ballD [OF \<open>bounded S\<close>] by blast
lp15@63130
    27
  have "a + (B / norm l) *\<^sub>R l \<notin> ball a B"
lp15@63130
    28
    by (simp add: dist_norm \<open>l \<noteq> 0\<close>)
lp15@63130
    29
  with B have "a + (B / norm l) *\<^sub>R l \<notin> rel_interior S"
lp15@63130
    30
    using rel_interior_subset subsetCE by blast
lp15@63130
    31
  with \<open>B > 0\<close> \<open>l \<noteq> 0\<close> have nonMT: "?D \<noteq> {}"
lp15@63130
    32
    using divide_pos_pos zero_less_norm_iff by fastforce
lp15@63130
    33
  have bdd: "bdd_below ?D"
lp15@63130
    34
    by (metis (no_types, lifting) bdd_belowI le_less mem_Collect_eq)
lp15@63130
    35
  have relin_Ex: "\<And>x. x \<in> rel_interior S \<Longrightarrow>
lp15@63130
    36
                    \<exists>e>0. \<forall>x'\<in>affine hull S. dist x' x < e \<longrightarrow> x' \<in> rel_interior S"
lp15@63130
    37
    using openin_rel_interior [of S] by (simp add: openin_euclidean_subtopology_iff)
lp15@63130
    38
  define d where "d = Inf ?D"
lp15@63130
    39
  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
    40
  proof -
lp15@63130
    41
    obtain e where "e>0"
lp15@63130
    42
            and e: "\<And>x'. x' \<in> affine hull S \<Longrightarrow> dist x' a < e \<Longrightarrow> x' \<in> rel_interior S"
lp15@63130
    43
      using relin_Ex a by blast
lp15@63130
    44
    show thesis
lp15@63130
    45
    proof (rule_tac \<epsilon> = "e / norm l" in that)
lp15@63130
    46
      show "0 < e / norm l" by (simp add: \<open>0 < e\<close> \<open>l \<noteq> 0\<close>)
lp15@63130
    47
    next
lp15@63130
    48
      show "a + \<eta> *\<^sub>R l \<in> rel_interior S" if "0 \<le> \<eta>" "\<eta> < e / norm l" for \<eta>
lp15@63130
    49
      proof (rule e)
lp15@63130
    50
        show "a + \<eta> *\<^sub>R l \<in> affine hull S"
lp15@63130
    51
          by (metis (no_types) add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff)
lp15@63130
    52
        show "dist (a + \<eta> *\<^sub>R l) a < e"
lp15@63130
    53
          using that by (simp add: \<open>l \<noteq> 0\<close> dist_norm pos_less_divide_eq)
lp15@63130
    54
      qed
lp15@63130
    55
    qed
lp15@63130
    56
  qed
lp15@63130
    57
  have inint: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> a + e *\<^sub>R l \<in> rel_interior S"
lp15@63130
    58
    unfolding d_def using cInf_lower [OF _ bdd]
lp15@63130
    59
    by (metis (no_types, lifting) a add.right_neutral le_less mem_Collect_eq not_less real_vector.scale_zero_left)
lp15@63130
    60
  have "\<epsilon> \<le> d"
lp15@63130
    61
    unfolding d_def
lp15@63130
    62
    apply (rule cInf_greatest [OF nonMT])
lp15@63130
    63
    using \<epsilon> dual_order.strict_implies_order le_less_linear by blast
lp15@63130
    64
  with \<open>0 < \<epsilon>\<close> have "0 < d" by simp
lp15@63130
    65
  have "a + d *\<^sub>R l \<notin> rel_interior S"
lp15@63130
    66
  proof
lp15@63130
    67
    assume adl: "a + d *\<^sub>R l \<in> rel_interior S"
lp15@63130
    68
    obtain e where "e > 0"
lp15@63130
    69
             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
    70
      using relin_Ex adl by blast
lp15@63130
    71
    have "d + e / norm l \<le> Inf {d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}"
lp15@63130
    72
    proof (rule cInf_greatest [OF nonMT], clarsimp)
lp15@63130
    73
      fix x::real
lp15@63130
    74
      assume "0 < x" and nonrel: "a + x *\<^sub>R l \<notin> rel_interior S"
lp15@63130
    75
      show "d + e / norm l \<le> x"
lp15@63130
    76
      proof (cases "x < d")
lp15@63130
    77
        case True with inint nonrel \<open>0 < x\<close>
lp15@63130
    78
          show ?thesis by auto
lp15@63130
    79
      next
lp15@63130
    80
        case False
lp15@63130
    81
          then have dle: "x < d + e / norm l \<Longrightarrow> dist (a + x *\<^sub>R l) (a + d *\<^sub>R l) < e"
lp15@63130
    82
            by (simp add: field_simps \<open>l \<noteq> 0\<close>)
lp15@63130
    83
          have ain: "a + x *\<^sub>R l \<in> affine hull S"
lp15@63130
    84
            by (metis add_diff_cancel_left' aff affine_affine_hull mem_affine_3_minus aaff)
lp15@63130
    85
          show ?thesis
lp15@63130
    86
            using e [OF ain] nonrel dle by force
lp15@63130
    87
      qed
lp15@63130
    88
    qed
lp15@63130
    89
    then show False
lp15@63130
    90
      using \<open>0 < e\<close> \<open>l \<noteq> 0\<close> by (simp add: d_def [symmetric] divide_simps)
lp15@63130
    91
  qed
lp15@63130
    92
  moreover have "a + d *\<^sub>R l \<in> closure S"
lp15@63130
    93
  proof (clarsimp simp: closure_approachable)
lp15@63130
    94
    fix \<eta>::real assume "0 < \<eta>"
lp15@63130
    95
    have 1: "a + (d - min d (\<eta> / 2 / norm l)) *\<^sub>R l \<in> S"
lp15@63130
    96
      apply (rule subsetD [OF rel_interior_subset inint])
lp15@63130
    97
      using \<open>l \<noteq> 0\<close> \<open>0 < d\<close> \<open>0 < \<eta>\<close> by auto
lp15@63130
    98
    have "norm l * min d (\<eta> / (norm l * 2)) \<le> norm l * (\<eta> / (norm l * 2))"
lp15@63130
    99
      by (metis min_def mult_left_mono norm_ge_zero order_refl)
lp15@63130
   100
    also have "... < \<eta>"
lp15@63130
   101
      using \<open>l \<noteq> 0\<close> \<open>0 < \<eta>\<close> by (simp add: divide_simps)
lp15@63130
   102
    finally have 2: "norm l * min d (\<eta> / (norm l * 2)) < \<eta>" .
lp15@63130
   103
    show "\<exists>y\<in>S. dist y (a + d *\<^sub>R l) < \<eta>"
lp15@63130
   104
      apply (rule_tac x="a + (d - min d (\<eta> / 2 / norm l)) *\<^sub>R l" in bexI)
lp15@63130
   105
      using 1 2 \<open>0 < d\<close> \<open>0 < \<eta>\<close> apply (auto simp: algebra_simps)
lp15@63130
   106
      done
lp15@63130
   107
  qed
lp15@63130
   108
  ultimately have infront: "a + d *\<^sub>R l \<in> rel_frontier S"
lp15@63130
   109
    by (simp add: rel_frontier_def)
lp15@63130
   110
  show ?thesis
lp15@63130
   111
    by (rule that [OF \<open>0 < d\<close> infront inint])
lp15@63130
   112
qed
lp15@63130
   113
lp15@63130
   114
corollary ray_to_frontier:
lp15@63130
   115
  fixes a :: "'a::euclidean_space"
lp15@63130
   116
  assumes "bounded S"
lp15@63130
   117
      and a: "a \<in> interior S"
lp15@63130
   118
      and "l \<noteq> 0"
lp15@63130
   119
  obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> frontier S"
lp15@63130
   120
           "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> interior S"
lp15@63130
   121
proof -
lp15@63130
   122
  have "interior S = rel_interior S"
lp15@63130
   123
    using a rel_interior_nonempty_interior by auto
lp15@63130
   124
  then have "a \<in> rel_interior S"
lp15@63130
   125
    using a by simp
lp15@63130
   126
  then show ?thesis
lp15@63130
   127
    apply (rule ray_to_rel_frontier [OF \<open>bounded S\<close> _ _ \<open>l \<noteq> 0\<close>])
lp15@63130
   128
     using a affine_hull_nonempty_interior apply blast
lp15@63130
   129
    by (simp add: \<open>interior S = rel_interior S\<close> frontier_def rel_frontier_def that)
lp15@63130
   130
qed
lp15@63130
   131
lp15@63130
   132
proposition
lp15@63130
   133
  fixes S :: "'a::euclidean_space set"
lp15@63130
   134
  assumes "compact S" and 0: "0 \<in> rel_interior S"
lp15@63130
   135
      and star: "\<And>x. x \<in> S \<Longrightarrow> open_segment 0 x \<subseteq> rel_interior S"
lp15@63130
   136
    shows starlike_compact_projective1_0:
lp15@63130
   137
            "S - rel_interior S homeomorphic sphere 0 1 \<inter> affine hull S"
lp15@63130
   138
            (is "?SMINUS homeomorphic ?SPHER")
lp15@63130
   139
      and starlike_compact_projective2_0:
lp15@63130
   140
            "S homeomorphic cball 0 1 \<inter> affine hull S"
lp15@63130
   141
            (is "S homeomorphic ?CBALL")
lp15@63130
   142
proof -
lp15@63130
   143
  have starI: "(u *\<^sub>R x) \<in> rel_interior S" if "x \<in> S" "0 \<le> u" "u < 1" for x u
lp15@63130
   144
  proof (cases "x=0 \<or> u=0")
lp15@63130
   145
    case True with 0 show ?thesis by force
lp15@63130
   146
  next
lp15@63130
   147
    case False with that show ?thesis
lp15@63130
   148
      by (auto simp: in_segment intro: star [THEN subsetD])
lp15@63130
   149
  qed
lp15@63130
   150
  have "0 \<in> S"  using assms rel_interior_subset by auto
lp15@63130
   151
  define proj where "proj \<equiv> \<lambda>x::'a. x /\<^sub>R norm x"
lp15@63130
   152
  have eqI: "x = y" if "proj x = proj y" "norm x = norm y" for x y
lp15@63130
   153
    using that  by (force simp: proj_def)
lp15@63130
   154
  then have iff_eq: "\<And>x y. (proj x = proj y \<and> norm x = norm y) \<longleftrightarrow> x = y"
lp15@63130
   155
    by blast
lp15@63130
   156
  have projI: "x \<in> affine hull S \<Longrightarrow> proj x \<in> affine hull S" for x
lp15@63130
   157
    by (metis \<open>0 \<in> S\<close> affine_hull_span_0 hull_inc span_mul proj_def)
lp15@63130
   158
  have nproj1 [simp]: "x \<noteq> 0 \<Longrightarrow> norm(proj x) = 1" for x
lp15@63130
   159
    by (simp add: proj_def)
lp15@63130
   160
  have proj0_iff [simp]: "proj x = 0 \<longleftrightarrow> x = 0" for x
lp15@63130
   161
    by (simp add: proj_def)
lp15@63130
   162
  have cont_proj: "continuous_on (UNIV - {0}) proj"
lp15@63130
   163
    unfolding proj_def by (rule continuous_intros | force)+
lp15@63130
   164
  have proj_spherI: "\<And>x. \<lbrakk>x \<in> affine hull S; x \<noteq> 0\<rbrakk> \<Longrightarrow> proj x \<in> ?SPHER"
lp15@63130
   165
    by (simp add: projI)
lp15@63130
   166
  have "bounded S" "closed S"
lp15@63130
   167
    using \<open>compact S\<close> compact_eq_bounded_closed by blast+
lp15@63130
   168
  have inj_on_proj: "inj_on proj (S - rel_interior S)"
lp15@63130
   169
  proof
lp15@63130
   170
    fix x y
lp15@63130
   171
    assume x: "x \<in> S - rel_interior S"
lp15@63130
   172
       and y: "y \<in> S - rel_interior S" and eq: "proj x = proj y"
lp15@63130
   173
    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
   174
      using 0 by auto
lp15@63130
   175
    consider "norm x = norm y" | "norm x < norm y" | "norm x > norm y" by linarith
lp15@63130
   176
    then show "x = y"
lp15@63130
   177
    proof cases
lp15@63130
   178
      assume "norm x = norm y"
lp15@63130
   179
        with iff_eq eq show "x = y" by blast
lp15@63130
   180
    next
lp15@63130
   181
      assume *: "norm x < norm y"
lp15@63130
   182
      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
   183
        by force
lp15@63130
   184
      then have "proj ((norm x / norm y) *\<^sub>R y) = proj x"
lp15@63130
   185
        by (metis (no_types) divide_inverse local.proj_def eq scaleR_scaleR)
lp15@63130
   186
      then have [simp]: "(norm x / norm y) *\<^sub>R y = x"
lp15@63130
   187
        by (rule eqI) (simp add: \<open>y \<noteq> 0\<close>)
lp15@63130
   188
      have no: "0 \<le> norm x / norm y" "norm x / norm y < 1"
lp15@63130
   189
        using * by (auto simp: divide_simps)
lp15@63130
   190
      then show "x = y"
lp15@63130
   191
        using starI [OF \<open>y \<in> S\<close> no] xynot by auto
lp15@63130
   192
    next
lp15@63130
   193
      assume *: "norm x > norm y"
lp15@63130
   194
      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
   195
        by force
lp15@63130
   196
      then have "proj ((norm y / norm x) *\<^sub>R x) = proj y"
lp15@63130
   197
        by (metis (no_types) divide_inverse local.proj_def eq scaleR_scaleR)
lp15@63130
   198
      then have [simp]: "(norm y / norm x) *\<^sub>R x = y"
lp15@63130
   199
        by (rule eqI) (simp add: \<open>x \<noteq> 0\<close>)
lp15@63130
   200
      have no: "0 \<le> norm y / norm x" "norm y / norm x < 1"
lp15@63130
   201
        using * by (auto simp: divide_simps)
lp15@63130
   202
      then show "x = y"
lp15@63130
   203
        using starI [OF \<open>x \<in> S\<close> no] xynot by auto
lp15@63130
   204
    qed
lp15@63130
   205
  qed
lp15@63130
   206
  have "\<exists>surf. homeomorphism (S - rel_interior S) ?SPHER proj surf"
lp15@63130
   207
  proof (rule homeomorphism_compact)
lp15@63130
   208
    show "compact (S - rel_interior S)"
lp15@63130
   209
       using \<open>compact S\<close> compact_rel_boundary by blast
lp15@63130
   210
    show "continuous_on (S - rel_interior S) proj"
lp15@63130
   211
      using 0 by (blast intro: continuous_on_subset [OF cont_proj])
lp15@63130
   212
    show "proj ` (S - rel_interior S) = ?SPHER"
lp15@63130
   213
    proof
lp15@63130
   214
      show "proj ` (S - rel_interior S) \<subseteq> ?SPHER"
lp15@63130
   215
        using 0 by (force simp: hull_inc projI intro: nproj1)
lp15@63130
   216
      show "?SPHER \<subseteq> proj ` (S - rel_interior S)"
lp15@63130
   217
      proof (clarsimp simp: proj_def)
lp15@63130
   218
        fix x
lp15@63130
   219
        assume "x \<in> affine hull S" and nox: "norm x = 1"
lp15@63130
   220
        then have "x \<noteq> 0" by auto
lp15@63130
   221
        obtain d where "0 < d" and dx: "(d *\<^sub>R x) \<in> rel_frontier S"
lp15@63130
   222
                   and ri: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (e *\<^sub>R x) \<in> rel_interior S"
lp15@63130
   223
          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
   224
        show "x \<in> (\<lambda>x. x /\<^sub>R norm x) ` (S - rel_interior S)"
lp15@63130
   225
          apply (rule_tac x="d *\<^sub>R x" in image_eqI)
lp15@63130
   226
          using \<open>0 < d\<close>
lp15@63130
   227
          using dx \<open>closed S\<close> apply (auto simp: rel_frontier_def divide_simps nox)
lp15@63130
   228
          done
lp15@63130
   229
      qed
lp15@63130
   230
    qed
lp15@63130
   231
  qed (rule inj_on_proj)
lp15@63130
   232
  then obtain surf where surf: "homeomorphism (S - rel_interior S) ?SPHER proj surf"
lp15@63130
   233
    by blast
lp15@63130
   234
  then have cont_surf: "continuous_on (proj ` (S - rel_interior S)) surf"
lp15@63130
   235
    by (auto simp: homeomorphism_def)
lp15@63130
   236
  have surf_nz: "\<And>x. x \<in> ?SPHER \<Longrightarrow> surf x \<noteq> 0"
lp15@63130
   237
    by (metis "0" DiffE homeomorphism_def imageI surf)
lp15@63130
   238
  have cont_nosp: "continuous_on (?SPHER) (\<lambda>x. norm x *\<^sub>R ((surf o proj) x))"
lp15@63130
   239
    apply (rule continuous_intros)+
lp15@63130
   240
    apply (rule continuous_on_subset [OF cont_proj], force)
lp15@63130
   241
    apply (rule continuous_on_subset [OF cont_surf])
lp15@63130
   242
    apply (force simp: homeomorphism_image1 [OF surf] dest: proj_spherI)
lp15@63130
   243
    done
lp15@63130
   244
  have surfpS: "\<And>x. \<lbrakk>norm x = 1; x \<in> affine hull S\<rbrakk> \<Longrightarrow> surf (proj x) \<in> S"
lp15@63130
   245
    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
   246
  have *: "\<exists>y. norm y = 1 \<and> y \<in> affine hull S \<and> x = surf (proj y)"
lp15@63130
   247
          if "x \<in> S" "x \<notin> rel_interior S" for x
lp15@63130
   248
  proof -
lp15@63130
   249
    have "proj x \<in> ?SPHER"
lp15@63130
   250
      by (metis (full_types) "0" hull_inc proj_spherI that)
lp15@63130
   251
    moreover have "surf (proj x) = x"
lp15@63130
   252
      by (metis Diff_iff homeomorphism_def surf that)
lp15@63130
   253
    ultimately show ?thesis
lp15@63130
   254
      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
   255
  qed
lp15@63130
   256
  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
   257
    by (metis (full_types) DiffE one_neq_zero homeomorphism_def image_eqI norm_zero proj_spherI surf)
lp15@63130
   258
  have no_sp_im: "(\<lambda>x. norm x *\<^sub>R surf (proj x)) ` (?SPHER) = S - rel_interior S"
lp15@63130
   259
    by (auto simp: surfpS image_def Bex_def surfp_notin *)
lp15@63130
   260
  have inj_spher: "inj_on (\<lambda>x. norm x *\<^sub>R surf (proj x)) ?SPHER"
lp15@63130
   261
  proof
lp15@63130
   262
    fix x y
lp15@63130
   263
    assume xy: "x \<in> ?SPHER" "y \<in> ?SPHER"
lp15@63130
   264
       and eq: " norm x *\<^sub>R surf (proj x) = norm y *\<^sub>R surf (proj y)"
lp15@63130
   265
    then have "norm x = 1" "norm y = 1" "x \<in> affine hull S" "y \<in> affine hull S"
lp15@63130
   266
      using 0 by auto
lp15@63130
   267
    with eq show "x = y"
lp15@63130
   268
      by (simp add: proj_def) (metis surf xy homeomorphism_def)
lp15@63130
   269
  qed
lp15@63130
   270
  have co01: "compact ?SPHER"
lp15@63130
   271
    by (simp add: closed_affine_hull compact_Int_closed)
lp15@63130
   272
  show "?SMINUS homeomorphic ?SPHER"
lp15@63130
   273
    apply (subst homeomorphic_sym)
lp15@63130
   274
    apply (rule homeomorphic_compact [OF co01 cont_nosp [unfolded o_def] no_sp_im inj_spher])
lp15@63130
   275
    done
lp15@63130
   276
  have proj_scaleR: "\<And>a x. 0 < a \<Longrightarrow> proj (a *\<^sub>R x) = proj x"
lp15@63130
   277
    by (simp add: proj_def)
lp15@63130
   278
  have cont_sp0: "continuous_on (affine hull S - {0}) (surf o proj)"
lp15@63130
   279
    apply (rule continuous_on_compose [OF continuous_on_subset [OF cont_proj]], force)
lp15@63130
   280
    apply (rule continuous_on_subset [OF cont_surf])
lp15@63130
   281
    using homeomorphism_image1 proj_spherI surf by fastforce
lp15@63130
   282
  obtain B where "B>0" and B: "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B"
lp15@63130
   283
    by (metis compact_imp_bounded \<open>compact S\<close> bounded_pos_less less_eq_real_def)
lp15@63130
   284
  have cont_nosp: "continuous (at x within ?CBALL) (\<lambda>x. norm x *\<^sub>R surf (proj x))"
lp15@63130
   285
         if "norm x \<le> 1" "x \<in> affine hull S" for x
lp15@63130
   286
  proof (cases "x=0")
lp15@63130
   287
    case True
lp15@63130
   288
    show ?thesis using True
lp15@63130
   289
      apply (simp add: continuous_within)
lp15@63130
   290
      apply (rule lim_null_scaleR_bounded [where B=B])
lp15@63130
   291
      apply (simp_all add: tendsto_norm_zero eventually_at)
lp15@63130
   292
      apply (rule_tac x=B in exI)
lp15@63130
   293
      using B surfpS proj_def projI apply (auto simp: \<open>B > 0\<close>)
lp15@63130
   294
      done
lp15@63130
   295
  next
lp15@63130
   296
    case False
lp15@63130
   297
    then have "\<forall>\<^sub>F x in at x. (x \<in> affine hull S - {0}) = (x \<in> affine hull S)"
lp15@63130
   298
      apply (simp add: eventually_at)
lp15@63130
   299
      apply (rule_tac x="norm x" in exI)
lp15@63130
   300
      apply (auto simp: False)
lp15@63130
   301
      done
lp15@63130
   302
    with cont_sp0 have *: "continuous (at x within affine hull S) (\<lambda>x. surf (proj x))"
lp15@63130
   303
      apply (simp add: continuous_on_eq_continuous_within)
lp15@63130
   304
      apply (drule_tac x=x in bspec, force simp: False that)
lp15@63130
   305
      apply (simp add: continuous_within Lim_transform_within_set)
lp15@63130
   306
      done
lp15@63130
   307
    show ?thesis
lp15@63130
   308
      apply (rule continuous_within_subset [where s = "affine hull S", OF _ Int_lower2])
lp15@63130
   309
      apply (rule continuous_intros *)+
lp15@63130
   310
      done
lp15@63130
   311
  qed
lp15@63130
   312
  have cont_nosp2: "continuous_on ?CBALL (\<lambda>x. norm x *\<^sub>R ((surf o proj) x))"
lp15@63130
   313
    by (simp add: continuous_on_eq_continuous_within cont_nosp)
lp15@63130
   314
  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
   315
  proof (cases "y=0")
lp15@63130
   316
    case True then show ?thesis
lp15@63130
   317
      by (simp add: \<open>0 \<in> S\<close>)
lp15@63130
   318
  next
lp15@63130
   319
    case False
lp15@63130
   320
    then have "norm y *\<^sub>R surf (proj y) = norm y *\<^sub>R surf (proj (y /\<^sub>R norm y))"
lp15@63130
   321
      by (simp add: proj_def)
lp15@63130
   322
    have "norm y \<le> 1" using that by simp
lp15@63130
   323
    have "surf (proj (y /\<^sub>R norm y)) \<in> S"
lp15@63130
   324
      apply (rule surfpS)
lp15@63130
   325
      using proj_def projI yaff
lp15@63130
   326
      by (auto simp: False)
lp15@63130
   327
    then have "surf (proj y) \<in> S"
lp15@63130
   328
      by (simp add: False proj_def)
lp15@63130
   329
    then show "norm y *\<^sub>R surf (proj y) \<in> S"
lp15@63130
   330
      by (metis dual_order.antisym le_less_linear norm_ge_zero rel_interior_subset scaleR_one
lp15@63130
   331
                starI subset_eq \<open>norm y \<le> 1\<close>)
lp15@63130
   332
  qed
lp15@63130
   333
  moreover have "x \<in> (\<lambda>x. norm x *\<^sub>R surf (proj x)) ` (?CBALL)" if "x \<in> S" for x
lp15@63130
   334
  proof (cases "x=0")
lp15@63130
   335
    case True with that hull_inc  show ?thesis by fastforce
lp15@63130
   336
  next
lp15@63130
   337
    case False
lp15@63130
   338
    then have psp: "proj (surf (proj x)) = proj x"
lp15@63130
   339
      by (metis homeomorphism_def hull_inc proj_spherI surf that)
lp15@63130
   340
    have nxx: "norm x *\<^sub>R proj x = x"
lp15@63130
   341
      by (simp add: False local.proj_def)
lp15@63130
   342
    have affineI: "(1 / norm (surf (proj x))) *\<^sub>R x \<in> affine hull S"
lp15@63130
   343
      by (metis \<open>0 \<in> S\<close> affine_hull_span_0 hull_inc span_clauses(4) that)
lp15@63130
   344
    have sproj_nz: "surf (proj x) \<noteq> 0"
lp15@63130
   345
      by (metis False proj0_iff psp)
lp15@63130
   346
    then have "proj x = proj (proj x)"
lp15@63130
   347
      by (metis False nxx proj_scaleR zero_less_norm_iff)
lp15@63130
   348
    moreover have scaleproj: "\<And>a r. r *\<^sub>R proj a = (r / norm a) *\<^sub>R a"
lp15@63130
   349
      by (simp add: divide_inverse local.proj_def)
lp15@63130
   350
    ultimately have "(norm (surf (proj x)) / norm x) *\<^sub>R x \<notin> rel_interior S"
lp15@63130
   351
      by (metis (no_types) sproj_nz divide_self_if hull_inc norm_eq_zero nproj1 projI psp scaleR_one surfp_notin that)
lp15@63130
   352
    then have "(norm (surf (proj x)) / norm x) \<ge> 1"
lp15@63130
   353
      using starI [OF that] by (meson starI [OF that] le_less_linear norm_ge_zero zero_le_divide_iff)
lp15@63130
   354
    then have nole: "norm x \<le> norm (surf (proj x))"
lp15@63130
   355
      by (simp add: le_divide_eq_1)
lp15@63130
   356
    show ?thesis
lp15@63130
   357
      apply (rule_tac x="inverse(norm(surf (proj x))) *\<^sub>R x" in image_eqI)
lp15@63130
   358
      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
   359
      apply (auto simp: divide_simps nole affineI)
lp15@63130
   360
      done
lp15@63130
   361
  qed
lp15@63130
   362
  ultimately have im_cball: "(\<lambda>x. norm x *\<^sub>R surf (proj x)) ` ?CBALL = S"
lp15@63130
   363
    by blast
lp15@63130
   364
  have inj_cball: "inj_on (\<lambda>x. norm x *\<^sub>R surf (proj x)) ?CBALL"
lp15@63130
   365
  proof
lp15@63130
   366
    fix x y
lp15@63130
   367
    assume "x \<in> ?CBALL" "y \<in> ?CBALL"
lp15@63130
   368
       and eq: "norm x *\<^sub>R surf (proj x) = norm y *\<^sub>R surf (proj y)"
lp15@63130
   369
    then have x: "x \<in> affine hull S" and y: "y \<in> affine hull S"
lp15@63130
   370
      using 0 by auto
lp15@63130
   371
    show "x = y"
lp15@63130
   372
    proof (cases "x=0 \<or> y=0")
lp15@63130
   373
      case True then show "x = y" using eq proj_spherI surf_nz x y by force
lp15@63130
   374
    next
lp15@63130
   375
      case False
lp15@63130
   376
      with x y have speq: "surf (proj x) = surf (proj y)"
lp15@63130
   377
        by (metis eq homeomorphism_apply2 proj_scaleR proj_spherI surf zero_less_norm_iff)
lp15@63130
   378
      then have "norm x = norm y"
lp15@63130
   379
        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
   380
      moreover have "proj x = proj y"
lp15@63130
   381
        by (metis (no_types) False speq homeomorphism_apply2 proj_spherI surf x y)
lp15@63130
   382
      ultimately show "x = y"
lp15@63130
   383
        using eq eqI by blast
lp15@63130
   384
    qed
lp15@63130
   385
  qed
lp15@63130
   386
  have co01: "compact ?CBALL"
lp15@63130
   387
    by (simp add: closed_affine_hull compact_Int_closed)
lp15@63130
   388
  show "S homeomorphic ?CBALL"
lp15@63130
   389
    apply (subst homeomorphic_sym)
lp15@63130
   390
    apply (rule homeomorphic_compact [OF co01 cont_nosp2 [unfolded o_def] im_cball inj_cball])
lp15@63130
   391
    done
lp15@63130
   392
qed
lp15@63130
   393
lp15@63130
   394
corollary
lp15@63130
   395
  fixes S :: "'a::euclidean_space set"
lp15@63130
   396
  assumes "compact S" and a: "a \<in> rel_interior S"
lp15@63130
   397
      and star: "\<And>x. x \<in> S \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
lp15@63130
   398
    shows starlike_compact_projective1:
lp15@63130
   399
            "S - rel_interior S homeomorphic sphere a 1 \<inter> affine hull S"
lp15@63130
   400
      and starlike_compact_projective2:
lp15@63130
   401
            "S homeomorphic cball a 1 \<inter> affine hull S"
lp15@63130
   402
proof -
lp15@63130
   403
  have 1: "compact (op+ (-a) ` S)" by (meson assms compact_translation)
lp15@63130
   404
  have 2: "0 \<in> rel_interior (op+ (-a) ` S)"
lp15@63130
   405
    by (simp add: a rel_interior_translation)
lp15@63130
   406
  have 3: "open_segment 0 x \<subseteq> rel_interior (op+ (-a) ` S)" if "x \<in> (op+ (-a) ` S)" for x
lp15@63130
   407
  proof -
lp15@63130
   408
    have "x+a \<in> S" using that by auto
lp15@63130
   409
    then have "open_segment a (x+a) \<subseteq> rel_interior S" by (metis star)
lp15@63130
   410
    then show ?thesis using open_segment_translation
lp15@63130
   411
      using rel_interior_translation by fastforce
lp15@63130
   412
  qed
lp15@63130
   413
  have "S - rel_interior S homeomorphic (op+ (-a) ` S) - rel_interior (op+ (-a) ` S)"
lp15@63130
   414
    by (metis rel_interior_translation translation_diff homeomorphic_translation)
lp15@63130
   415
  also have "... homeomorphic sphere 0 1 \<inter> affine hull (op+ (-a) ` S)"
lp15@63130
   416
    by (rule starlike_compact_projective1_0 [OF 1 2 3])
lp15@63130
   417
  also have "... = op+ (-a) ` (sphere a 1 \<inter> affine hull S)"
lp15@63130
   418
    by (metis affine_hull_translation left_minus sphere_translation translation_Int)
lp15@63130
   419
  also have "... homeomorphic sphere a 1 \<inter> affine hull S"
lp15@63130
   420
    using homeomorphic_translation homeomorphic_sym by blast
lp15@63130
   421
  finally show "S - rel_interior S homeomorphic sphere a 1 \<inter> affine hull S" .
lp15@63130
   422
lp15@63130
   423
  have "S homeomorphic (op+ (-a) ` S)"
lp15@63130
   424
    by (metis homeomorphic_translation)
lp15@63130
   425
  also have "... homeomorphic cball 0 1 \<inter> affine hull (op+ (-a) ` S)"
lp15@63130
   426
    by (rule starlike_compact_projective2_0 [OF 1 2 3])
lp15@63130
   427
  also have "... = op+ (-a) ` (cball a 1 \<inter> affine hull S)"
lp15@63130
   428
    by (metis affine_hull_translation left_minus cball_translation translation_Int)
lp15@63130
   429
  also have "... homeomorphic cball a 1 \<inter> affine hull S"
lp15@63130
   430
    using homeomorphic_translation homeomorphic_sym by blast
lp15@63130
   431
  finally show "S homeomorphic cball a 1 \<inter> affine hull S" .
lp15@63130
   432
qed
lp15@63130
   433
lp15@63130
   434
corollary starlike_compact_projective_special:
lp15@63130
   435
  assumes "compact S"
lp15@63130
   436
    and cb01: "cball (0::'a::euclidean_space) 1 \<subseteq> S"
lp15@63130
   437
    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
   438
  shows "S homeomorphic (cball (0::'a::euclidean_space) 1)"
lp15@63130
   439
proof -
lp15@63130
   440
  have "ball 0 1 \<subseteq> interior S"
lp15@63130
   441
    using cb01 interior_cball interior_mono by blast
lp15@63130
   442
  then have 0: "0 \<in> rel_interior S"
lp15@63130
   443
    by (meson centre_in_ball subsetD interior_subset_rel_interior le_numeral_extra(2) not_le)
lp15@63130
   444
  have [simp]: "affine hull S = UNIV"
lp15@63130
   445
    using \<open>ball 0 1 \<subseteq> interior S\<close> by (auto intro!: affine_hull_nonempty_interior)
lp15@63130
   446
  have star: "open_segment 0 x \<subseteq> rel_interior S" if "x \<in> S" for x
hoelzl@63627
   447
  proof
lp15@63130
   448
    fix p assume "p \<in> open_segment 0 x"
lp15@63130
   449
    then obtain u where "x \<noteq> 0" and u: "0 \<le> u" "u < 1" and p: "u *\<^sub>R x = p"
hoelzl@63627
   450
      by (auto simp: in_segment)
lp15@63130
   451
    then show "p \<in> rel_interior S"
lp15@63130
   452
      using scale [OF that u] closure_subset frontier_def interior_subset_rel_interior by fastforce
lp15@63130
   453
  qed
lp15@63130
   454
  show ?thesis
lp15@63130
   455
    using starlike_compact_projective2_0 [OF \<open>compact S\<close> 0 star] by simp
lp15@63130
   456
qed
lp15@63130
   457
lp15@63130
   458
lemma homeomorphic_convex_lemma:
lp15@63130
   459
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
lp15@63130
   460
  assumes "convex S" "compact S" "convex T" "compact T"
lp15@63130
   461
      and affeq: "aff_dim S = aff_dim T"
lp15@63130
   462
    shows "(S - rel_interior S) homeomorphic (T - rel_interior T) \<and>
lp15@63130
   463
           S homeomorphic T"
lp15@63130
   464
proof (cases "rel_interior S = {} \<or> rel_interior T = {}")
lp15@63130
   465
  case True
lp15@63130
   466
    then show ?thesis
lp15@63130
   467
      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
   468
next
lp15@63130
   469
  case False
lp15@63130
   470
  then obtain a b where a: "a \<in> rel_interior S" and b: "b \<in> rel_interior T" by auto
lp15@63130
   471
  have starS: "\<And>x. x \<in> S \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
lp15@63130
   472
    using rel_interior_closure_convex_segment
lp15@63130
   473
          a \<open>convex S\<close> closure_subset subsetCE by blast
lp15@63130
   474
  have starT: "\<And>x. x \<in> T \<Longrightarrow> open_segment b x \<subseteq> rel_interior T"
lp15@63130
   475
    using rel_interior_closure_convex_segment
lp15@63130
   476
          b \<open>convex T\<close> closure_subset subsetCE by blast
lp15@63130
   477
  let ?aS = "op+ (-a) ` S" and ?bT = "op+ (-b) ` T"
lp15@63130
   478
  have 0: "0 \<in> affine hull ?aS" "0 \<in> affine hull ?bT"
lp15@63130
   479
    by (metis a b subsetD hull_inc image_eqI left_minus rel_interior_subset)+
lp15@63130
   480
  have subs: "subspace (span ?aS)" "subspace (span ?bT)"
lp15@63130
   481
    by (rule subspace_span)+
lp15@63130
   482
  moreover
lp15@63130
   483
  have "dim (span (op + (- a) ` S)) = dim (span (op + (- b) ` T))"
lp15@63130
   484
    by (metis 0 aff_dim_translation_eq aff_dim_zero affeq dim_span nat_int)
lp15@63130
   485
  ultimately obtain f g where "linear f" "linear g"
lp15@63130
   486
                and fim: "f ` span ?aS = span ?bT"
lp15@63130
   487
                and gim: "g ` span ?bT = span ?aS"
lp15@63130
   488
                and fno: "\<And>x. x \<in> span ?aS \<Longrightarrow> norm(f x) = norm x"
lp15@63130
   489
                and gno: "\<And>x. x \<in> span ?bT \<Longrightarrow> norm(g x) = norm x"
lp15@63130
   490
                and gf: "\<And>x. x \<in> span ?aS \<Longrightarrow> g(f x) = x"
lp15@63130
   491
                and fg: "\<And>x. x \<in> span ?bT \<Longrightarrow> f(g x) = x"
lp15@63130
   492
    by (rule isometries_subspaces) blast
lp15@63130
   493
  have [simp]: "continuous_on A f" for A
lp15@63130
   494
    using \<open>linear f\<close> linear_conv_bounded_linear linear_continuous_on by blast
lp15@63130
   495
  have [simp]: "continuous_on B g" for B
lp15@63130
   496
    using \<open>linear g\<close> linear_conv_bounded_linear linear_continuous_on by blast
lp15@63130
   497
  have eqspanS: "affine hull ?aS = span ?aS"
lp15@63130
   498
    by (metis a affine_hull_span_0 subsetD hull_inc image_eqI left_minus rel_interior_subset)
lp15@63130
   499
  have eqspanT: "affine hull ?bT = span ?bT"
lp15@63130
   500
    by (metis b affine_hull_span_0 subsetD hull_inc image_eqI left_minus rel_interior_subset)
lp15@63130
   501
  have "S homeomorphic cball a 1 \<inter> affine hull S"
lp15@63130
   502
    by (rule starlike_compact_projective2 [OF \<open>compact S\<close> a starS])
lp15@63130
   503
  also have "... homeomorphic op+ (-a) ` (cball a 1 \<inter> affine hull S)"
lp15@63130
   504
    by (metis homeomorphic_translation)
lp15@63130
   505
  also have "... = cball 0 1 \<inter> op+ (-a) ` (affine hull S)"
lp15@63130
   506
    by (auto simp: dist_norm)
lp15@63130
   507
  also have "... = cball 0 1 \<inter> span ?aS"
lp15@63130
   508
    using eqspanS affine_hull_translation by blast
lp15@63130
   509
  also have "... homeomorphic cball 0 1 \<inter> span ?bT"
lp15@63130
   510
    proof (rule homeomorphicI [where f=f and g=g])
lp15@63130
   511
      show fim1: "f ` (cball 0 1 \<inter> span ?aS) = cball 0 1 \<inter> span ?bT"
lp15@63130
   512
        apply (rule subset_antisym)
lp15@63130
   513
         using fim fno apply (force simp:, clarify)
lp15@63130
   514
        by (metis IntI fg gim gno image_eqI mem_cball_0)
lp15@63130
   515
      show "g ` (cball 0 1 \<inter> span ?bT) = cball 0 1 \<inter> span ?aS"
lp15@63130
   516
        apply (rule subset_antisym)
lp15@63130
   517
         using gim gno apply (force simp:, clarify)
lp15@63130
   518
        by (metis IntI fim1 gf image_eqI)
lp15@63130
   519
    qed (auto simp: fg gf)
lp15@63130
   520
  also have "... = cball 0 1 \<inter> op+ (-b) ` (affine hull T)"
lp15@63130
   521
    using eqspanT affine_hull_translation by blast
lp15@63130
   522
  also have "... = op+ (-b) ` (cball b 1 \<inter> affine hull T)"
lp15@63130
   523
    by (auto simp: dist_norm)
lp15@63130
   524
  also have "... homeomorphic (cball b 1 \<inter> affine hull T)"
lp15@63130
   525
    by (metis homeomorphic_translation homeomorphic_sym)
lp15@63130
   526
  also have "... homeomorphic T"
lp15@63130
   527
    by (metis starlike_compact_projective2 [OF \<open>compact T\<close> b starT] homeomorphic_sym)
lp15@63130
   528
  finally have 1: "S homeomorphic T" .
lp15@63130
   529
lp15@63130
   530
  have "S - rel_interior S homeomorphic sphere a 1 \<inter> affine hull S"
lp15@63130
   531
    by (rule starlike_compact_projective1 [OF \<open>compact S\<close> a starS])
lp15@63130
   532
  also have "... homeomorphic op+ (-a) ` (sphere a 1 \<inter> affine hull S)"
lp15@63130
   533
    by (metis homeomorphic_translation)
lp15@63130
   534
  also have "... = sphere 0 1 \<inter> op+ (-a) ` (affine hull S)"
lp15@63130
   535
    by (auto simp: dist_norm)
lp15@63130
   536
  also have "... = sphere 0 1 \<inter> span ?aS"
lp15@63130
   537
    using eqspanS affine_hull_translation by blast
lp15@63130
   538
  also have "... homeomorphic sphere 0 1 \<inter> span ?bT"
lp15@63130
   539
    proof (rule homeomorphicI [where f=f and g=g])
lp15@63130
   540
      show fim1: "f ` (sphere 0 1 \<inter> span ?aS) = sphere 0 1 \<inter> span ?bT"
lp15@63130
   541
        apply (rule subset_antisym)
lp15@63130
   542
        using fim fno apply (force simp:, clarify)
lp15@63130
   543
        by (metis IntI fg gim gno image_eqI mem_sphere_0)
lp15@63130
   544
      show "g ` (sphere 0 1 \<inter> span ?bT) = sphere 0 1 \<inter> span ?aS"
lp15@63130
   545
        apply (rule subset_antisym)
lp15@63130
   546
        using gim gno apply (force simp:, clarify)
lp15@63130
   547
        by (metis IntI fim1 gf image_eqI)
lp15@63130
   548
    qed (auto simp: fg gf)
lp15@63130
   549
  also have "... = sphere 0 1 \<inter> op+ (-b) ` (affine hull T)"
lp15@63130
   550
    using eqspanT affine_hull_translation by blast
lp15@63130
   551
  also have "... = op+ (-b) ` (sphere b 1 \<inter> affine hull T)"
lp15@63130
   552
    by (auto simp: dist_norm)
lp15@63130
   553
  also have "... homeomorphic (sphere b 1 \<inter> affine hull T)"
lp15@63130
   554
    by (metis homeomorphic_translation homeomorphic_sym)
lp15@63130
   555
  also have "... homeomorphic T - rel_interior T"
lp15@63130
   556
    by (metis starlike_compact_projective1 [OF \<open>compact T\<close> b starT] homeomorphic_sym)
lp15@63130
   557
  finally have 2: "S - rel_interior S homeomorphic T - rel_interior T" .
lp15@63130
   558
  show ?thesis
lp15@63130
   559
    using 1 2 by blast
lp15@63130
   560
qed
lp15@63130
   561
lp15@63130
   562
lemma homeomorphic_convex_compact_sets:
lp15@63130
   563
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
lp15@63130
   564
  assumes "convex S" "compact S" "convex T" "compact T"
lp15@63130
   565
      and affeq: "aff_dim S = aff_dim T"
lp15@63130
   566
    shows "S homeomorphic T"
lp15@63130
   567
using homeomorphic_convex_lemma [OF assms] assms
lp15@63130
   568
by (auto simp: rel_frontier_def)
lp15@63130
   569
lp15@63130
   570
lemma homeomorphic_rel_frontiers_convex_bounded_sets:
lp15@63130
   571
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
lp15@63130
   572
  assumes "convex S" "bounded S" "convex T" "bounded T"
lp15@63130
   573
      and affeq: "aff_dim S = aff_dim T"
lp15@63130
   574
    shows  "rel_frontier S homeomorphic rel_frontier T"
lp15@63130
   575
using assms homeomorphic_convex_lemma [of "closure S" "closure T"]
lp15@63130
   576
by (simp add: rel_frontier_def convex_rel_interior_closure)
lp15@63130
   577
lp15@63130
   578
lp15@63130
   579
subsection\<open>Homeomorphisms between punctured spheres and affine sets\<close>
lp15@63130
   580
text\<open>Including the famous stereoscopic projection of the 3-D sphere to the complex plane\<close>
lp15@63130
   581
lp15@63130
   582
text\<open>The special case with centre 0 and radius 1\<close>
lp15@63130
   583
lemma homeomorphic_punctured_affine_sphere_affine_01:
lp15@63130
   584
  assumes "b \<in> sphere 0 1" "affine T" "0 \<in> T" "b \<in> T" "affine p"
lp15@63130
   585
      and affT: "aff_dim T = aff_dim p + 1"
lp15@63130
   586
    shows "(sphere 0 1 \<inter> T) - {b} homeomorphic p"
lp15@63130
   587
proof -
lp15@63130
   588
  have [simp]: "norm b = 1" "b\<bullet>b = 1"
lp15@63130
   589
    using assms by (auto simp: norm_eq_1)
lp15@63130
   590
  have [simp]: "T \<inter> {v. b\<bullet>v = 0} \<noteq> {}"
lp15@63130
   591
    using \<open>0 \<in> T\<close> by auto
lp15@63130
   592
  have [simp]: "\<not> T \<subseteq> {v. b\<bullet>v = 0}"
lp15@63130
   593
    using \<open>norm b = 1\<close> \<open>b \<in> T\<close> by auto
lp15@63130
   594
  define f where "f \<equiv> \<lambda>x. 2 *\<^sub>R b + (2 / (1 - b\<bullet>x)) *\<^sub>R (x - b)"
lp15@63130
   595
  define g where "g \<equiv> \<lambda>y. b + (4 / (norm y ^ 2 + 4)) *\<^sub>R (y - 2 *\<^sub>R b)"
lp15@63130
   596
  have [simp]: "\<And>x. \<lbrakk>x \<in> T; b\<bullet>x = 0\<rbrakk> \<Longrightarrow> f (g x) = x"
lp15@63130
   597
    unfolding f_def g_def by (simp add: algebra_simps divide_simps add_nonneg_eq_0_iff)
lp15@63130
   598
  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
   599
    apply (simp add: dot_square_norm [symmetric])
lp15@63130
   600
    apply (simp add: f_def vector_add_divide_simps divide_simps norm_eq_1)
lp15@63130
   601
    apply (simp add: algebra_simps inner_commute)
lp15@63130
   602
    done
lp15@63130
   603
  have [simp]: "\<And>u::real. 8 + u * (u * 8) = u * 16 \<longleftrightarrow> u=1"
lp15@63130
   604
    by algebra
lp15@63130
   605
  have [simp]: "\<And>x. \<lbrakk>norm x = 1; b \<bullet> x \<noteq> 1\<rbrakk> \<Longrightarrow> g (f x) = x"
lp15@63130
   606
    unfolding g_def no by (auto simp: f_def divide_simps)
lp15@63130
   607
  have [simp]: "\<And>x. \<lbrakk>x \<in> T; b \<bullet> x = 0\<rbrakk> \<Longrightarrow> norm (g x) = 1"
lp15@63130
   608
    unfolding g_def
lp15@63130
   609
    apply (rule power2_eq_imp_eq)
lp15@63130
   610
    apply (simp_all add: dot_square_norm [symmetric] divide_simps vector_add_divide_simps)
lp15@63130
   611
    apply (simp add: algebra_simps inner_commute)
lp15@63130
   612
    done
lp15@63130
   613
  have [simp]: "\<And>x. \<lbrakk>x \<in> T; b \<bullet> x = 0\<rbrakk> \<Longrightarrow> b \<bullet> g x \<noteq> 1"
lp15@63130
   614
    unfolding g_def
lp15@63130
   615
    apply (simp_all add: dot_square_norm [symmetric] divide_simps vector_add_divide_simps add_nonneg_eq_0_iff)
lp15@63130
   616
    apply (auto simp: algebra_simps)
lp15@63130
   617
    done
lp15@63130
   618
  have "subspace T"
lp15@63130
   619
    by (simp add: assms subspace_affine)
lp15@63130
   620
  have [simp]: "\<And>x. \<lbrakk>x \<in> T; b \<bullet> x = 0\<rbrakk> \<Longrightarrow> g x \<in> T"
lp15@63130
   621
    unfolding g_def
lp15@63130
   622
    by (blast intro: \<open>subspace T\<close> \<open>b \<in> T\<close> subspace_add subspace_mul subspace_diff)
lp15@63130
   623
  have "f ` {x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<subseteq> {x. b\<bullet>x = 0}"
lp15@63130
   624
    unfolding f_def using \<open>norm b = 1\<close> norm_eq_1
lp15@63130
   625
    by (force simp: field_simps inner_add_right inner_diff_right)
lp15@63130
   626
  moreover have "f ` T \<subseteq> T"
lp15@63130
   627
    unfolding f_def using assms
lp15@63130
   628
    apply (auto simp: field_simps inner_add_right inner_diff_right)
lp15@63130
   629
    by (metis add_0 diff_zero mem_affine_3_minus)
lp15@63130
   630
  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
   631
    apply clarify
lp15@63130
   632
    apply (rule_tac x = "g x" in image_eqI, auto)
lp15@63130
   633
    done
lp15@63130
   634
  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
   635
    by blast
lp15@63130
   636
  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
   637
    apply (rule power2_eq_imp_eq)
lp15@63130
   638
    apply (simp_all add: dot_square_norm [symmetric])
lp15@63130
   639
    apply (auto simp: power2_eq_square algebra_simps inner_commute)
lp15@63130
   640
    done
lp15@63130
   641
  have [simp]: "\<And>x. \<lbrakk>norm x = 1; b \<bullet> x \<noteq> 1\<rbrakk> \<Longrightarrow> b \<bullet> f x = 0"
lp15@63130
   642
    by (simp add: f_def algebra_simps divide_simps)
lp15@63130
   643
  have [simp]: "\<And>x. \<lbrakk>x \<in> T; norm x = 1; b \<bullet> x \<noteq> 1\<rbrakk> \<Longrightarrow> f x \<in> T"
lp15@63130
   644
    unfolding f_def
lp15@63130
   645
    by (blast intro: \<open>subspace T\<close> \<open>b \<in> T\<close> subspace_add subspace_mul subspace_diff)
lp15@63130
   646
  have "g ` {x. b\<bullet>x = 0} \<subseteq> {x. norm x = 1 \<and> b\<bullet>x \<noteq> 1}"
lp15@63130
   647
    unfolding g_def
lp15@63130
   648
    apply (clarsimp simp: no4 vector_add_divide_simps divide_simps add_nonneg_eq_0_iff dot_square_norm [symmetric])
lp15@63130
   649
    apply (auto simp: algebra_simps)
lp15@63130
   650
    done
lp15@63130
   651
  moreover have "g ` T \<subseteq> T"
lp15@63130
   652
    unfolding g_def
lp15@63130
   653
    by (blast intro: \<open>subspace T\<close> \<open>b \<in> T\<close> subspace_add subspace_mul subspace_diff)
lp15@63130
   654
  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
   655
    apply clarify
lp15@63130
   656
    apply (rule_tac x = "f x" in image_eqI, auto)
lp15@63130
   657
    done
lp15@63130
   658
  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
   659
    by blast
lp15@63130
   660
  have aff: "affine ({x. b\<bullet>x = 0} \<inter> T)"
lp15@63130
   661
    by (blast intro: affine_hyperplane assms)
lp15@63130
   662
  have contf: "continuous_on ({x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T) f"
lp15@63130
   663
    unfolding f_def by (rule continuous_intros | force)+
lp15@63130
   664
  have contg: "continuous_on ({x. b\<bullet>x = 0} \<inter> T) g"
lp15@63130
   665
    unfolding g_def by (rule continuous_intros | force simp: add_nonneg_eq_0_iff)+
lp15@63130
   666
  have "(sphere 0 1 \<inter> T) - {b} = {x. norm x = 1 \<and> (b\<bullet>x \<noteq> 1)} \<inter> T"
lp15@63130
   667
    using  \<open>norm b = 1\<close> by (auto simp: norm_eq_1) (metis vector_eq  \<open>b\<bullet>b = 1\<close>)
lp15@63130
   668
  also have "... homeomorphic {x. b\<bullet>x = 0} \<inter> T"
lp15@63130
   669
    by (rule homeomorphicI [OF imf img contf contg]) auto
lp15@63130
   670
  also have "... homeomorphic p"
lp15@63130
   671
    apply (rule homeomorphic_affine_sets [OF aff \<open>affine p\<close>])
lp15@63130
   672
    apply (simp add: Int_commute aff_dim_affine_Int_hyperplane [OF \<open>affine T\<close>] affT)
lp15@63130
   673
    done
lp15@63130
   674
  finally show ?thesis .
lp15@63130
   675
qed
lp15@63130
   676
lp15@63130
   677
theorem homeomorphic_punctured_affine_sphere_affine:
lp15@63130
   678
  fixes a :: "'a :: euclidean_space"
lp15@63130
   679
  assumes "0 < r" "b \<in> sphere a r" "affine T" "a \<in> T" "b \<in> T" "affine p"
lp15@63130
   680
      and aff: "aff_dim T = aff_dim p + 1"
lp15@63130
   681
    shows "((sphere a r \<inter> T) - {b}) homeomorphic p"
lp15@63130
   682
proof -
lp15@63130
   683
  have "a \<noteq> b" using assms by auto
lp15@63130
   684
  then have inj: "inj (\<lambda>x::'a. x /\<^sub>R norm (a - b))"
lp15@63130
   685
    by (simp add: inj_on_def)
lp15@63130
   686
  have "((sphere a r \<inter> T) - {b}) homeomorphic
lp15@63130
   687
        op+ (-a) ` ((sphere a r \<inter> T) - {b})"
lp15@63130
   688
    by (rule homeomorphic_translation)
lp15@63130
   689
  also have "... homeomorphic op *\<^sub>R (inverse r) ` op + (- a) ` (sphere a r \<inter> T - {b})"
lp15@63130
   690
    by (metis \<open>0 < r\<close> homeomorphic_scaling inverse_inverse_eq inverse_zero less_irrefl)
lp15@63130
   691
  also have "... = sphere 0 1 \<inter> (op *\<^sub>R (inverse r) ` op + (- a) ` T) - {(b - a) /\<^sub>R r}"
lp15@63130
   692
    using assms by (auto simp: dist_norm norm_minus_commute divide_simps)
lp15@63130
   693
  also have "... homeomorphic p"
lp15@63130
   694
    apply (rule homeomorphic_punctured_affine_sphere_affine_01)
lp15@63130
   695
    using assms
lp15@63130
   696
    apply (auto simp: dist_norm norm_minus_commute affine_scaling affine_translation [symmetric] aff_dim_translation_eq inj)
lp15@63130
   697
    done
lp15@63130
   698
  finally show ?thesis .
lp15@63130
   699
qed
lp15@63130
   700
lp15@63130
   701
proposition homeomorphic_punctured_sphere_affine_gen:
lp15@63130
   702
  fixes a :: "'a :: euclidean_space"
lp15@63130
   703
  assumes "convex S" "bounded S" and a: "a \<in> rel_frontier S"
lp15@63130
   704
      and "affine T" and affS: "aff_dim S = aff_dim T + 1"
lp15@63130
   705
    shows "rel_frontier S - {a} homeomorphic T"
lp15@63130
   706
proof -
lp15@63130
   707
  have "S \<noteq> {}" using assms by auto
lp15@63130
   708
  obtain U :: "'a set" where "affine U" and affdS: "aff_dim U = aff_dim S"
lp15@63130
   709
    using choose_affine_subset [OF affine_UNIV aff_dim_geq]
lp15@63130
   710
    by (meson aff_dim_affine_hull affine_affine_hull)
lp15@63130
   711
  have "convex U"
lp15@63130
   712
    by (simp add: affine_imp_convex \<open>affine U\<close>)
lp15@63130
   713
  have "U \<noteq> {}"
lp15@63130
   714
    by (metis \<open>S \<noteq> {}\<close> \<open>aff_dim U = aff_dim S\<close> aff_dim_empty)
lp15@63130
   715
  then obtain z where "z \<in> U"
lp15@63130
   716
    by auto
lp15@63130
   717
  then have bne: "ball z 1 \<inter> U \<noteq> {}" by force
lp15@63130
   718
  have [simp]: "aff_dim(ball z 1 \<inter> U) = aff_dim U"
lp15@63130
   719
    using aff_dim_convex_Int_open [OF \<open>convex U\<close> open_ball] bne
lp15@63130
   720
    by (fastforce simp add: Int_commute)
lp15@63130
   721
  have "rel_frontier S homeomorphic rel_frontier (ball z 1 \<inter> U)"
lp15@63130
   722
    apply (rule homeomorphic_rel_frontiers_convex_bounded_sets)
lp15@63130
   723
    apply (auto simp: \<open>affine U\<close> affine_imp_convex convex_Int affdS assms)
lp15@63130
   724
    done
lp15@63130
   725
  also have "... = sphere z 1 \<inter> U"
lp15@63130
   726
    using convex_affine_rel_frontier_Int [of "ball z 1" U]
lp15@63130
   727
    by (simp add: \<open>affine U\<close> bne)
lp15@63130
   728
  finally obtain h k where him: "h ` rel_frontier S = sphere z 1 \<inter> U"
lp15@63130
   729
                    and kim: "k ` (sphere z 1 \<inter> U) = rel_frontier S"
lp15@63130
   730
                    and hcon: "continuous_on (rel_frontier S) h"
lp15@63130
   731
                    and kcon: "continuous_on (sphere z 1 \<inter> U) k"
lp15@63130
   732
                    and kh:  "\<And>x. x \<in> rel_frontier S \<Longrightarrow> k(h(x)) = x"
lp15@63130
   733
                    and hk:  "\<And>y. y \<in> sphere z 1 \<inter> U \<Longrightarrow> h(k(y)) = y"
lp15@63130
   734
    unfolding homeomorphic_def homeomorphism_def by auto
lp15@63130
   735
  have "rel_frontier S - {a} homeomorphic (sphere z 1 \<inter> U) - {h a}"
lp15@63130
   736
  proof (rule homeomorphicI [where f=h and g=k])
lp15@63130
   737
    show h: "h ` (rel_frontier S - {a}) = sphere z 1 \<inter> U - {h a}"
lp15@63130
   738
      using him a kh by auto metis
lp15@63130
   739
    show "k ` (sphere z 1 \<inter> U - {h a}) = rel_frontier S - {a}"
lp15@63130
   740
      by (force simp: h [symmetric] image_comp o_def kh)
lp15@63130
   741
  qed (auto intro: continuous_on_subset hcon kcon simp: kh hk)
lp15@63130
   742
  also have "... homeomorphic T"
lp15@63130
   743
    apply (rule homeomorphic_punctured_affine_sphere_affine)
lp15@63130
   744
    using a him
lp15@63130
   745
    by (auto simp: affS affdS \<open>affine T\<close>  \<open>affine U\<close> \<open>z \<in> U\<close>)
lp15@63130
   746
  finally show ?thesis .
lp15@63130
   747
qed
lp15@63130
   748
lp15@63130
   749
lp15@63130
   750
lemma homeomorphic_punctured_sphere_affine:
lp15@63130
   751
  fixes a :: "'a :: euclidean_space"
lp15@63130
   752
  assumes "0 < r" and b: "b \<in> sphere a r"
lp15@63130
   753
      and "affine T" and affS: "aff_dim T + 1 = DIM('a)"
lp15@63130
   754
    shows "(sphere a r - {b}) homeomorphic T"
lp15@63130
   755
using homeomorphic_punctured_sphere_affine_gen [of "cball a r" b T]
lp15@63130
   756
  assms aff_dim_cball by force
lp15@63130
   757
lp15@63130
   758
corollary homeomorphic_punctured_sphere_hyperplane:
lp15@63130
   759
  fixes a :: "'a :: euclidean_space"
lp15@63130
   760
  assumes "0 < r" and b: "b \<in> sphere a r"
lp15@63130
   761
      and "c \<noteq> 0"
lp15@63130
   762
    shows "(sphere a r - {b}) homeomorphic {x::'a. c \<bullet> x = d}"
lp15@63130
   763
apply (rule homeomorphic_punctured_sphere_affine)
lp15@63130
   764
using assms
lp15@63130
   765
apply (auto simp: affine_hyperplane of_nat_diff)
lp15@63130
   766
done
lp15@63130
   767
lp15@63130
   768
lp15@63130
   769
text\<open> When dealing with AR, ANR and ANR later, it's useful to know that every set
lp15@63130
   770
  is homeomorphic to a closed subset of a convex set, and
lp15@63130
   771
  if the set is locally compact we can take the convex set to be the universe.\<close>
lp15@63130
   772
lp15@63130
   773
proposition homeomorphic_closedin_convex:
lp15@63130
   774
  fixes S :: "'m::euclidean_space set"
lp15@63130
   775
  assumes "aff_dim S < DIM('n)"
lp15@63130
   776
  obtains U and T :: "'n::euclidean_space set"
lp15@63130
   777
     where "convex U" "U \<noteq> {}" "closedin (subtopology euclidean U) T"
lp15@63130
   778
           "S homeomorphic T"
lp15@63130
   779
proof (cases "S = {}")
lp15@63130
   780
  case True then show ?thesis
lp15@63130
   781
    by (rule_tac U=UNIV and T="{}" in that) auto
lp15@63130
   782
next
lp15@63130
   783
  case False
lp15@63130
   784
  then obtain a where "a \<in> S" by auto
lp15@63130
   785
  obtain i::'n where i: "i \<in> Basis" "i \<noteq> 0"
lp15@63130
   786
    using SOME_Basis Basis_zero by force
lp15@63130
   787
  have "0 \<in> affine hull (op + (- a) ` S)"
lp15@63130
   788
    by (simp add: \<open>a \<in> S\<close> hull_inc)
lp15@63130
   789
  then have "dim (op + (- a) ` S) = aff_dim (op + (- a) ` S)"
lp15@63130
   790
    by (simp add: aff_dim_zero)
lp15@63130
   791
  also have "... < DIM('n)"
lp15@63130
   792
    by (simp add: aff_dim_translation_eq assms)
lp15@63130
   793
  finally have dd: "dim (op + (- a) ` S) < DIM('n)"
lp15@63130
   794
    by linarith
lp15@63130
   795
  obtain T where "subspace T" and Tsub: "T \<subseteq> {x. i \<bullet> x = 0}"
lp15@63130
   796
             and dimT: "dim T = dim (op + (- a) ` S)"
lp15@63130
   797
    apply (rule choose_subspace_of_subspace [of "dim (op + (- a) ` S)" "{x::'n. i \<bullet> x = 0}"])
lp15@63130
   798
     apply (simp add: dim_hyperplane [OF \<open>i \<noteq> 0\<close>])
lp15@63130
   799
     apply (metis DIM_positive Suc_pred dd not_le not_less_eq_eq)
lp15@63130
   800
    apply (metis span_eq subspace_hyperplane)
lp15@63130
   801
    done
lp15@63130
   802
  have "subspace (span (op + (- a) ` S))"
lp15@63130
   803
    using subspace_span by blast
lp15@63130
   804
  then obtain h k where "linear h" "linear k"
lp15@63130
   805
               and heq: "h ` span (op + (- a) ` S) = T"
lp15@63130
   806
               and keq:"k ` T = span (op + (- a) ` S)"
lp15@63130
   807
               and hinv [simp]:  "\<And>x. x \<in> span (op + (- a) ` S) \<Longrightarrow> k(h x) = x"
lp15@63130
   808
               and kinv [simp]:  "\<And>x. x \<in> T \<Longrightarrow> h(k x) = x"
lp15@63130
   809
    apply (rule isometries_subspaces [OF _ \<open>subspace T\<close>])
lp15@63130
   810
    apply (auto simp: dimT)
lp15@63130
   811
    done
lp15@63130
   812
  have hcont: "continuous_on A h" and kcont: "continuous_on B k" for A B
lp15@63130
   813
    using \<open>linear h\<close> \<open>linear k\<close> linear_continuous_on linear_conv_bounded_linear by blast+
lp15@63130
   814
  have ihhhh[simp]: "\<And>x. x \<in> S \<Longrightarrow> i \<bullet> h (x - a) = 0"
lp15@63130
   815
    using Tsub [THEN subsetD] heq span_inc by fastforce
lp15@63130
   816
  have "sphere 0 1 - {i} homeomorphic {x. i \<bullet> x = 0}"
lp15@63130
   817
    apply (rule homeomorphic_punctured_sphere_affine)
lp15@63130
   818
    using i
lp15@63130
   819
    apply (auto simp: affine_hyperplane)
lp15@63130
   820
    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
   821
  then obtain f g where fg: "homeomorphism (sphere 0 1 - {i}) {x. i \<bullet> x = 0} f g"
lp15@63130
   822
    by (force simp: homeomorphic_def)
lp15@63130
   823
  have "h ` op + (- a) ` S \<subseteq> T"
lp15@63130
   824
    using heq span_clauses(1) span_linear_image by blast
lp15@63130
   825
  then have "g ` h ` op + (- a) ` S \<subseteq> g ` {x. i \<bullet> x = 0}"
lp15@63130
   826
    using Tsub by (simp add: image_mono)
lp15@63130
   827
  also have "... \<subseteq> sphere 0 1 - {i}"
lp15@63130
   828
    by (simp add: fg [unfolded homeomorphism_def])
lp15@63130
   829
  finally have gh_sub_sph: "(g \<circ> h) ` op + (- a) ` S \<subseteq> sphere 0 1 - {i}"
lp15@63130
   830
    by (metis image_comp)
lp15@63130
   831
  then have gh_sub_cb: "(g \<circ> h) ` op + (- a) ` S \<subseteq> cball 0 1"
lp15@63130
   832
    by (metis Diff_subset order_trans sphere_cball)
lp15@63130
   833
  have [simp]: "\<And>u. u \<in> S \<Longrightarrow> norm (g (h (u - a))) = 1"
lp15@63130
   834
    using gh_sub_sph [THEN subsetD] by (auto simp: o_def)
lp15@63130
   835
  have ghcont: "continuous_on (op + (- a) ` S) (\<lambda>x. g (h x))"
lp15@63130
   836
    apply (rule continuous_on_compose2 [OF homeomorphism_cont2 [OF fg] hcont], force)
lp15@63130
   837
    done
lp15@63130
   838
  have kfcont: "continuous_on ((g \<circ> h \<circ> op + (- a)) ` S) (\<lambda>x. k (f x))"
lp15@63130
   839
    apply (rule continuous_on_compose2 [OF kcont])
lp15@63130
   840
    using homeomorphism_cont1 [OF fg] gh_sub_sph apply (force intro: continuous_on_subset, blast)
lp15@63130
   841
    done
lp15@63130
   842
  have "S homeomorphic op + (- a) ` S"
lp15@63130
   843
    by (simp add: homeomorphic_translation)
lp15@63130
   844
  also have Shom: "\<dots> homeomorphic (g \<circ> h) ` op + (- a) ` S"
lp15@63130
   845
    apply (simp add: homeomorphic_def homeomorphism_def)
lp15@63130
   846
    apply (rule_tac x="g \<circ> h" in exI)
lp15@63130
   847
    apply (rule_tac x="k \<circ> f" in exI)
lp15@63130
   848
    apply (auto simp: ghcont kfcont span_clauses(1) homeomorphism_apply2 [OF fg] image_comp)
lp15@63130
   849
    apply (force simp: o_def homeomorphism_apply2 [OF fg] span_clauses(1))
lp15@63130
   850
    done
lp15@63130
   851
  finally have Shom: "S homeomorphic (g \<circ> h) ` op + (- a) ` S" .
lp15@63130
   852
  show ?thesis
lp15@63130
   853
    apply (rule_tac U = "ball 0 1 \<union> image (g o h) (op + (- a) ` S)"
lp15@63130
   854
                and T = "image (g o h) (op + (- a) ` S)"
lp15@63130
   855
                    in that)
lp15@63130
   856
    apply (rule convex_intermediate_ball [of 0 1], force)
lp15@63130
   857
    using gh_sub_cb apply force
lp15@63130
   858
    apply force
lp15@63130
   859
    apply (simp add: closedin_closed)
lp15@63130
   860
    apply (rule_tac x="sphere 0 1" in exI)
lp15@63130
   861
    apply (auto simp: Shom)
lp15@63130
   862
    done
lp15@63130
   863
qed
lp15@63130
   864
lp15@63130
   865
subsection\<open>Locally compact sets in an open set\<close>
lp15@63130
   866
lp15@63130
   867
text\<open> Locally compact sets are closed in an open set and are homeomorphic
lp15@63130
   868
  to an absolutely closed set if we have one more dimension to play with.\<close>
lp15@63130
   869
lp15@63130
   870
lemma locally_compact_open_Int_closure:
lp15@63130
   871
  fixes S :: "'a :: metric_space set"
lp15@63130
   872
  assumes "locally compact S"
lp15@63130
   873
  obtains T where "open T" "S = T \<inter> closure S"
lp15@63130
   874
proof -
lp15@63130
   875
  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
   876
    by (metis assms locally_compact openin_open)
lp15@63130
   877
  then obtain t v where
lp15@63130
   878
        tv: "\<And>x. x \<in> S
lp15@63130
   879
             \<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
   880
    by metis
lp15@63130
   881
  then have o: "open (UNION S t)"
lp15@63130
   882
    by blast
lp15@63130
   883
  have "S = \<Union> (v ` S)"
lp15@63130
   884
    using tv by blast
lp15@63130
   885
  also have "... = UNION S t \<inter> closure S"
lp15@63130
   886
  proof
lp15@63130
   887
    show "UNION S v \<subseteq> UNION S t \<inter> closure S"
lp15@63130
   888
      apply safe
lp15@63130
   889
       apply (metis Int_iff subsetD UN_iff tv)
lp15@63130
   890
      apply (simp add: closure_def rev_subsetD tv)
lp15@63130
   891
      done
lp15@63130
   892
    have "t x \<inter> closure S \<subseteq> v x" if "x \<in> S" for x
lp15@63130
   893
    proof -
lp15@63130
   894
      have "t x \<inter> closure S \<subseteq> closure (t x \<inter> S)"
lp15@63130
   895
        by (simp add: open_Int_closure_subset that tv)
lp15@63130
   896
      also have "... \<subseteq> v x"
lp15@63130
   897
        by (metis Int_commute closure_minimal compact_imp_closed that tv)
lp15@63130
   898
      finally show ?thesis .
lp15@63130
   899
    qed
lp15@63130
   900
    then show "UNION S t \<inter> closure S \<subseteq> UNION S v"
lp15@63130
   901
      by blast
lp15@63130
   902
  qed
lp15@63130
   903
  finally have e: "S = UNION S t \<inter> closure S" .
lp15@63130
   904
  show ?thesis
lp15@63130
   905
    by (rule that [OF o e])
lp15@63130
   906
qed
lp15@63130
   907
lp15@63130
   908
lp15@63130
   909
lemma locally_compact_closedin_open:
lp15@63130
   910
    fixes S :: "'a :: metric_space set"
lp15@63130
   911
    assumes "locally compact S"
lp15@63130
   912
    obtains T where "open T" "closedin (subtopology euclidean T) S"
lp15@63130
   913
  by (metis locally_compact_open_Int_closure [OF assms] closed_closure closedin_closed_Int)
lp15@63130
   914
lp15@63130
   915
lp15@63130
   916
lemma locally_compact_homeomorphism_projection_closed:
lp15@63130
   917
  assumes "locally compact S"
lp15@63130
   918
  obtains T and f :: "'a \<Rightarrow> 'a :: euclidean_space \<times> 'b :: euclidean_space"
lp15@63130
   919
    where "closed T" "homeomorphism S T f fst"
lp15@63130
   920
proof (cases "closed S")
lp15@63130
   921
  case True
lp15@63130
   922
    then show ?thesis
lp15@63130
   923
      apply (rule_tac T = "S \<times> {0}" and f = "\<lambda>x. (x, 0)" in that)
lp15@63130
   924
      apply (auto simp: closed_Times homeomorphism_def continuous_intros)
lp15@63130
   925
      done
lp15@63130
   926
next
lp15@63130
   927
  case False
lp15@63130
   928
    obtain U where "open U" and US: "U \<inter> closure S = S"
lp15@63130
   929
      by (metis locally_compact_open_Int_closure [OF assms])
lp15@63130
   930
    with False have Ucomp: "-U \<noteq> {}"
lp15@63130
   931
      using closure_eq by auto
lp15@63130
   932
    have [simp]: "closure (- U) = -U"
lp15@63130
   933
      by (simp add: \<open>open U\<close> closed_Compl)
lp15@63130
   934
    define f :: "'a \<Rightarrow> 'a \<times> 'b" where "f \<equiv> \<lambda>x. (x, One /\<^sub>R setdist {x} (- U))"
lp15@63130
   935
    have "continuous_on U (\<lambda>x. (x, One /\<^sub>R setdist {x} (- U)))"
lp15@63301
   936
      apply (intro continuous_intros continuous_on_setdist)
lp15@63301
   937
      by (simp add: Ucomp setdist_eq_0_sing_1)
lp15@63130
   938
    then have homU: "homeomorphism U (f`U) f fst"
lp15@63130
   939
      by (auto simp: f_def homeomorphism_def image_iff continuous_intros)
lp15@63130
   940
    have cloS: "closedin (subtopology euclidean U) S"
lp15@63130
   941
      by (metis US closed_closure closedin_closed_Int)
lp15@63130
   942
    have cont: "isCont ((\<lambda>x. setdist {x} (- U)) o fst) z" for z :: "'a \<times> 'b"
lp15@63130
   943
      by (rule isCont_o continuous_intros continuous_at_setdist)+
lp15@63130
   944
    have setdist1D: "setdist {a} (- U) *\<^sub>R b = One \<Longrightarrow> setdist {a} (- U) \<noteq> 0" for a::'a and b::'b
lp15@63130
   945
      by force
lp15@63130
   946
    have *: "r *\<^sub>R b = One \<Longrightarrow> b = (1 / r) *\<^sub>R One" for r and b::'b
lp15@63130
   947
      by (metis One_non_0 nonzero_divide_eq_eq real_vector.scale_eq_0_iff real_vector.scale_scale scaleR_one)
lp15@63130
   948
    have "f ` U = {z. (setdist {fst z} (- U) *\<^sub>R snd z) \<in> {One}}"
lp15@63301
   949
      apply (auto simp: f_def setdist_eq_0_sing_1 field_simps Ucomp)
lp15@63130
   950
      apply (rule_tac x=a in image_eqI)
lp15@63301
   951
      apply (auto simp: * setdist_eq_0_sing_1 dest: setdist1D)
lp15@63130
   952
      done
lp15@63130
   953
    then have clfU: "closed (f ` U)"
lp15@63130
   954
      apply (rule ssubst)
lp15@63130
   955
      apply (rule continuous_closed_preimage_univ)
lp15@63130
   956
      apply (auto intro: continuous_intros cont [unfolded o_def])
lp15@63130
   957
      done
lp15@63130
   958
    have "closed (f ` S)"
lp15@63130
   959
       apply (rule closedin_closed_trans [OF _ clfU])
lp15@63130
   960
       apply (rule homeomorphism_imp_closed_map [OF homU cloS])
lp15@63130
   961
       done
lp15@63130
   962
    then show ?thesis
lp15@63130
   963
      apply (rule that)
lp15@63130
   964
      apply (rule homeomorphism_of_subsets [OF homU])
lp15@63130
   965
      using US apply auto
lp15@63130
   966
      done
lp15@63130
   967
qed
lp15@63130
   968
lp15@63130
   969
lemma locally_compact_closed_Int_open:
lp15@63130
   970
  fixes S :: "'a :: euclidean_space set"
lp15@63130
   971
  shows
lp15@63130
   972
    "locally compact S \<longleftrightarrow> (\<exists>U u. closed U \<and> open u \<and> S = U \<inter> u)"
lp15@63130
   973
by (metis closed_closure closed_imp_locally_compact inf_commute locally_compact_Int locally_compact_open_Int_closure open_imp_locally_compact)
lp15@63130
   974
lp15@63130
   975
lp15@63945
   976
lemma lowerdim_embeddings:
lp15@63945
   977
  assumes  "DIM('a) < DIM('b)"
lp15@63945
   978
  obtains f :: "'a::euclidean_space*real \<Rightarrow> 'b::euclidean_space" 
lp15@63945
   979
      and g :: "'b \<Rightarrow> 'a*real"
lp15@63945
   980
      and j :: 'b
lp15@63945
   981
  where "linear f" "linear g" "\<And>z. g (f z) = z" "j \<in> Basis" "\<And>x. f(x,0) \<bullet> j = 0"
lp15@63945
   982
proof -
lp15@63945
   983
  let ?B = "Basis :: ('a*real) set"
lp15@63945
   984
  have b01: "(0,1) \<in> ?B"
lp15@63945
   985
    by (simp add: Basis_prod_def)
lp15@63945
   986
  have "DIM('a * real) \<le> DIM('b)"
lp15@63945
   987
    by (simp add: Suc_leI assms)
lp15@63945
   988
  then obtain basf :: "'a*real \<Rightarrow> 'b" where sbf: "basf ` ?B \<subseteq> Basis" and injbf: "inj_on basf Basis"
lp15@63945
   989
    by (metis finite_Basis card_le_inj)
lp15@63945
   990
  define basg:: "'b \<Rightarrow> 'a * real" where
lp15@63945
   991
    "basg \<equiv> \<lambda>i. if i \<in> basf ` Basis then inv_into Basis basf i else (0,1)"
lp15@63945
   992
  have bgf[simp]: "basg (basf i) = i" if "i \<in> Basis" for i
lp15@63945
   993
    using inv_into_f_f injbf that by (force simp: basg_def)
lp15@63945
   994
  have sbg: "basg ` Basis \<subseteq> ?B" 
lp15@63945
   995
    by (force simp: basg_def injbf b01)
lp15@63945
   996
  define f :: "'a*real \<Rightarrow> 'b" where "f \<equiv> \<lambda>u. \<Sum>j\<in>Basis. (u \<bullet> basg j) *\<^sub>R j"
lp15@63945
   997
  define g :: "'b \<Rightarrow> 'a*real" where "g \<equiv> \<lambda>z. (\<Sum>i\<in>Basis. (z \<bullet> basf i) *\<^sub>R i)" 
lp15@63945
   998
  show ?thesis
lp15@63945
   999
  proof
lp15@63945
  1000
    show "linear f"
lp15@63945
  1001
      unfolding f_def
lp15@63945
  1002
      by (intro linear_compose_setsum linearI ballI) (auto simp: algebra_simps)
lp15@63945
  1003
    show "linear g"
lp15@63945
  1004
      unfolding g_def
lp15@63945
  1005
      by (intro linear_compose_setsum linearI ballI) (auto simp: algebra_simps)
lp15@63945
  1006
    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
  1007
      using sbf that by auto
lp15@63945
  1008
    show gf: "g (f x) = x" for x
lp15@63945
  1009
      apply (rule euclidean_eqI)
lp15@63945
  1010
      apply (simp add: f_def g_def inner_setsum_left scaleR_setsum_left algebra_simps)
lp15@63945
  1011
      apply (simp add: Groups_Big.setsum_distrib_left [symmetric] *)
lp15@63945
  1012
      done
lp15@63945
  1013
    show "basf(0,1) \<in> Basis"
lp15@63945
  1014
      using b01 sbf by auto
lp15@63945
  1015
    then show "f(x,0) \<bullet> basf(0,1) = 0" for x
lp15@63945
  1016
      apply (simp add: f_def inner_setsum_left)
lp15@63945
  1017
      apply (rule comm_monoid_add_class.setsum.neutral)
lp15@63945
  1018
      using b01 inner_not_same_Basis by fastforce
lp15@63945
  1019
  qed
lp15@63945
  1020
qed
lp15@63945
  1021
lp15@63130
  1022
proposition locally_compact_homeomorphic_closed:
lp15@63130
  1023
  fixes S :: "'a::euclidean_space set"
lp15@63130
  1024
  assumes "locally compact S" and dimlt: "DIM('a) < DIM('b)"
lp15@63130
  1025
  obtains T :: "'b::euclidean_space set" where "closed T" "S homeomorphic T"
lp15@63130
  1026
proof -
lp15@63130
  1027
  obtain U:: "('a*real)set" and h
lp15@63130
  1028
    where "closed U" and homU: "homeomorphism S U h fst"
lp15@63130
  1029
    using locally_compact_homeomorphism_projection_closed assms by metis
lp15@63945
  1030
  obtain f :: "'a*real \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'a*real"
lp15@63945
  1031
    where "linear f" "linear g" and gf [simp]: "\<And>z. g (f z) = z"
lp15@63945
  1032
    using lowerdim_embeddings [OF dimlt] by metis 
lp15@63945
  1033
  then have "inj f"
lp15@63945
  1034
    by (metis injI)
lp15@63130
  1035
  have gfU: "g ` f ` U = U"
lp15@63945
  1036
    by (simp add: image_comp o_def)
lp15@63130
  1037
  have "S homeomorphic U"
lp15@63130
  1038
    using homU homeomorphic_def by blast
lp15@63130
  1039
  also have "... homeomorphic f ` U"
lp15@63130
  1040
    apply (rule homeomorphicI [OF refl gfU])
lp15@63130
  1041
       apply (meson \<open>inj f\<close> \<open>linear f\<close> homeomorphism_cont2 linear_homeomorphism_image)
lp15@63945
  1042
    using \<open>linear g\<close> linear_continuous_on linear_conv_bounded_linear apply blast
lp15@63945
  1043
    apply (auto simp: o_def)
lp15@63945
  1044
    done
lp15@63130
  1045
  finally show ?thesis
lp15@63130
  1046
    apply (rule_tac T = "f ` U" in that)
lp15@63130
  1047
    apply (rule closed_injective_linear_image [OF \<open>closed U\<close> \<open>linear f\<close> \<open>inj f\<close>], assumption)
lp15@63130
  1048
    done
lp15@63130
  1049
qed
lp15@63130
  1050
lp15@63130
  1051
lp15@63130
  1052
lemma homeomorphic_convex_compact_lemma:
lp15@63130
  1053
  fixes s :: "'a::euclidean_space set"
lp15@63130
  1054
  assumes "convex s"
lp15@63130
  1055
    and "compact s"
lp15@63130
  1056
    and "cball 0 1 \<subseteq> s"
lp15@63130
  1057
  shows "s homeomorphic (cball (0::'a) 1)"
lp15@63130
  1058
proof (rule starlike_compact_projective_special[OF assms(2-3)])
lp15@63130
  1059
  fix x u
lp15@63130
  1060
  assume "x \<in> s" and "0 \<le> u" and "u < (1::real)"
lp15@63130
  1061
  have "open (ball (u *\<^sub>R x) (1 - u))"
lp15@63130
  1062
    by (rule open_ball)
lp15@63130
  1063
  moreover have "u *\<^sub>R x \<in> ball (u *\<^sub>R x) (1 - u)"
lp15@63130
  1064
    unfolding centre_in_ball using \<open>u < 1\<close> by simp
lp15@63130
  1065
  moreover have "ball (u *\<^sub>R x) (1 - u) \<subseteq> s"
lp15@63130
  1066
  proof
lp15@63130
  1067
    fix y
lp15@63130
  1068
    assume "y \<in> ball (u *\<^sub>R x) (1 - u)"
lp15@63130
  1069
    then have "dist (u *\<^sub>R x) y < 1 - u"
lp15@63130
  1070
      unfolding mem_ball .
lp15@63130
  1071
    with \<open>u < 1\<close> have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> cball 0 1"
lp15@63130
  1072
      by (simp add: dist_norm inverse_eq_divide norm_minus_commute)
lp15@63130
  1073
    with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s" ..
lp15@63130
  1074
    with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \<in> s"
lp15@63130
  1075
      using \<open>x \<in> s\<close> \<open>0 \<le> u\<close> \<open>u < 1\<close> [THEN less_imp_le] by (rule convexD_alt)
lp15@63130
  1076
    then show "y \<in> s" using \<open>u < 1\<close>
lp15@63130
  1077
      by simp
lp15@63130
  1078
  qed
lp15@63130
  1079
  ultimately have "u *\<^sub>R x \<in> interior s" ..
lp15@63130
  1080
  then show "u *\<^sub>R x \<in> s - frontier s"
lp15@63130
  1081
    using frontier_def and interior_subset by auto
lp15@63130
  1082
qed
lp15@63130
  1083
lp15@63130
  1084
proposition homeomorphic_convex_compact_cball:
lp15@63130
  1085
  fixes e :: real
lp15@63130
  1086
    and s :: "'a::euclidean_space set"
lp15@63130
  1087
  assumes "convex s"
lp15@63130
  1088
    and "compact s"
lp15@63130
  1089
    and "interior s \<noteq> {}"
lp15@63130
  1090
    and "e > 0"
lp15@63130
  1091
  shows "s homeomorphic (cball (b::'a) e)"
lp15@63130
  1092
proof -
lp15@63130
  1093
  obtain a where "a \<in> interior s"
lp15@63130
  1094
    using assms(3) by auto
lp15@63130
  1095
  then obtain d where "d > 0" and d: "cball a d \<subseteq> s"
lp15@63130
  1096
    unfolding mem_interior_cball by auto
lp15@63130
  1097
  let ?d = "inverse d" and ?n = "0::'a"
lp15@63130
  1098
  have "cball ?n 1 \<subseteq> (\<lambda>x. inverse d *\<^sub>R (x - a)) ` s"
lp15@63130
  1099
    apply rule
lp15@63130
  1100
    apply (rule_tac x="d *\<^sub>R x + a" in image_eqI)
lp15@63130
  1101
    defer
lp15@63130
  1102
    apply (rule d[unfolded subset_eq, rule_format])
lp15@63130
  1103
    using \<open>d > 0\<close>
lp15@63130
  1104
    unfolding mem_cball dist_norm
lp15@63130
  1105
    apply (auto simp add: mult_right_le_one_le)
lp15@63130
  1106
    done
lp15@63130
  1107
  then have "(\<lambda>x. inverse d *\<^sub>R (x - a)) ` s homeomorphic cball ?n 1"
lp15@63130
  1108
    using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *\<^sub>R -a + ?d *\<^sub>R x) ` s",
lp15@63130
  1109
      OF convex_affinity compact_affinity]
lp15@63130
  1110
    using assms(1,2)
lp15@63130
  1111
    by (auto simp add: scaleR_right_diff_distrib)
lp15@63130
  1112
  then show ?thesis
lp15@63130
  1113
    apply (rule_tac homeomorphic_trans[OF _ homeomorphic_balls(2)[of 1 _ ?n]])
lp15@63130
  1114
    apply (rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" s "?d *\<^sub>R -a"]])
lp15@63130
  1115
    using \<open>d>0\<close> \<open>e>0\<close>
lp15@63130
  1116
    apply (auto simp add: scaleR_right_diff_distrib)
lp15@63130
  1117
    done
lp15@63130
  1118
qed
lp15@63130
  1119
lp15@63130
  1120
corollary homeomorphic_convex_compact:
lp15@63130
  1121
  fixes s :: "'a::euclidean_space set"
lp15@63130
  1122
    and t :: "'a set"
lp15@63130
  1123
  assumes "convex s" "compact s" "interior s \<noteq> {}"
lp15@63130
  1124
    and "convex t" "compact t" "interior t \<noteq> {}"
lp15@63130
  1125
  shows "s homeomorphic t"
lp15@63130
  1126
  using assms
lp15@63130
  1127
  by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)
lp15@63130
  1128
lp15@63301
  1129
subsection\<open>Covering spaces and lifting results for them\<close>
lp15@63301
  1130
lp15@63301
  1131
definition covering_space
lp15@63301
  1132
           :: "'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
lp15@63301
  1133
  where
lp15@63301
  1134
  "covering_space c p s \<equiv>
lp15@63301
  1135
       continuous_on c p \<and> p ` c = s \<and>
lp15@63301
  1136
       (\<forall>x \<in> s. \<exists>t. x \<in> t \<and> openin (subtopology euclidean s) t \<and>
lp15@63301
  1137
                    (\<exists>v. \<Union>v = {x. x \<in> c \<and> p x \<in> t} \<and>
lp15@63301
  1138
                        (\<forall>u \<in> v. openin (subtopology euclidean c) u) \<and>
lp15@63301
  1139
                        pairwise disjnt v \<and>
lp15@63301
  1140
                        (\<forall>u \<in> v. \<exists>q. homeomorphism u t p q)))"
lp15@63301
  1141
lp15@63301
  1142
lemma covering_space_imp_continuous: "covering_space c p s \<Longrightarrow> continuous_on c p"
lp15@63301
  1143
  by (simp add: covering_space_def)
lp15@63301
  1144
lp15@63301
  1145
lemma covering_space_imp_surjective: "covering_space c p s \<Longrightarrow> p ` c = s"
lp15@63301
  1146
  by (simp add: covering_space_def)
lp15@63301
  1147
lp15@63301
  1148
lemma homeomorphism_imp_covering_space: "homeomorphism s t f g \<Longrightarrow> covering_space s f t"
lp15@63301
  1149
  apply (simp add: homeomorphism_def covering_space_def, clarify)
lp15@63301
  1150
  apply (rule_tac x=t in exI, simp)
lp15@63301
  1151
  apply (rule_tac x="{s}" in exI, auto)
lp15@63301
  1152
  done
lp15@63301
  1153
lp15@63301
  1154
lemma covering_space_local_homeomorphism:
lp15@63301
  1155
  assumes "covering_space c p s" "x \<in> c"
lp15@63301
  1156
  obtains t u q where "x \<in> t" "openin (subtopology euclidean c) t"
lp15@63301
  1157
                      "p x \<in> u" "openin (subtopology euclidean s) u"
lp15@63301
  1158
                      "homeomorphism t u p q"
lp15@63301
  1159
using assms
lp15@63301
  1160
apply (simp add: covering_space_def, clarify)
lp15@63301
  1161
apply (drule_tac x="p x" in bspec, force)
lp15@63301
  1162
by (metis (no_types, lifting) Union_iff mem_Collect_eq)
lp15@63301
  1163
lp15@63301
  1164
lp15@63301
  1165
lemma covering_space_local_homeomorphism_alt:
lp15@63301
  1166
  assumes p: "covering_space c p s" and "y \<in> s"
lp15@63301
  1167
  obtains x t u q where "p x = y"
lp15@63301
  1168
                        "x \<in> t" "openin (subtopology euclidean c) t"
lp15@63301
  1169
                        "y \<in> u" "openin (subtopology euclidean s) u"
lp15@63301
  1170
                          "homeomorphism t u p q"
lp15@63301
  1171
proof -
lp15@63301
  1172
  obtain x where "p x = y" "x \<in> c"
lp15@63301
  1173
    using assms covering_space_imp_surjective by blast
lp15@63301
  1174
  show ?thesis
lp15@63301
  1175
    apply (rule covering_space_local_homeomorphism [OF p \<open>x \<in> c\<close>])
lp15@63301
  1176
    using that \<open>p x = y\<close> by blast
lp15@63301
  1177
qed
lp15@63301
  1178
lp15@63301
  1179
proposition covering_space_open_map:
lp15@63301
  1180
  fixes s :: "'a :: metric_space set" and t :: "'b :: metric_space set"
lp15@63301
  1181
  assumes p: "covering_space c p s" and t: "openin (subtopology euclidean c) t"
lp15@63301
  1182
    shows "openin (subtopology euclidean s) (p ` t)"
lp15@63301
  1183
proof -
lp15@63301
  1184
  have pce: "p ` c = s"
lp15@63301
  1185
   and covs:
lp15@63301
  1186
       "\<And>x. x \<in> s \<Longrightarrow>
lp15@63301
  1187
            \<exists>X VS. x \<in> X \<and> openin (subtopology euclidean s) X \<and>
lp15@63301
  1188
                  \<Union>VS = {x. x \<in> c \<and> p x \<in> X} \<and>
lp15@63301
  1189
                  (\<forall>u \<in> VS. openin (subtopology euclidean c) u) \<and>
lp15@63301
  1190
                  pairwise disjnt VS \<and>
lp15@63301
  1191
                  (\<forall>u \<in> VS. \<exists>q. homeomorphism u X p q)"
lp15@63301
  1192
    using p by (auto simp: covering_space_def)
lp15@63301
  1193
  have "t \<subseteq> c"  by (metis openin_euclidean_subtopology_iff t)
lp15@63301
  1194
  have "\<exists>T. openin (subtopology euclidean s) T \<and> y \<in> T \<and> T \<subseteq> p ` t"
lp15@63301
  1195
          if "y \<in> p ` t" for y
lp15@63301
  1196
  proof -
lp15@63301
  1197
    have "y \<in> s" using \<open>t \<subseteq> c\<close> pce that by blast
lp15@63301
  1198
    obtain U VS where "y \<in> U" and U: "openin (subtopology euclidean s) U"
lp15@63301
  1199
                  and VS: "\<Union>VS = {x. x \<in> c \<and> p x \<in> U}"
lp15@63301
  1200
                  and openVS: "\<forall>V \<in> VS. openin (subtopology euclidean c) V"
lp15@63301
  1201
                  and homVS: "\<And>V. V \<in> VS \<Longrightarrow> \<exists>q. homeomorphism V U p q"
lp15@63301
  1202
      using covs [OF \<open>y \<in> s\<close>] by auto
lp15@63301
  1203
    obtain x where "x \<in> c" "p x \<in> U" "x \<in> t" "p x = y"
lp15@63301
  1204
      apply simp
lp15@63301
  1205
      using t [unfolded openin_euclidean_subtopology_iff] \<open>y \<in> U\<close> \<open>y \<in> p ` t\<close> by blast
lp15@63301
  1206
    with VS obtain V where "x \<in> V" "V \<in> VS" by auto
lp15@63301
  1207
    then obtain q where q: "homeomorphism V U p q" using homVS by blast
lp15@63301
  1208
    then have ptV: "p ` (t \<inter> V) = U \<inter> {z. q z \<in> (t \<inter> V)}"
lp15@63301
  1209
      using VS \<open>V \<in> VS\<close> by (auto simp: homeomorphism_def)
lp15@63301
  1210
    have ocv: "openin (subtopology euclidean c) V"
lp15@63301
  1211
      by (simp add: \<open>V \<in> VS\<close> openVS)
lp15@63301
  1212
    have "openin (subtopology euclidean U) {z \<in> U. q z \<in> t \<inter> V}"
lp15@63301
  1213
      apply (rule continuous_on_open [THEN iffD1, rule_format])
lp15@63301
  1214
       using homeomorphism_def q apply blast
lp15@63301
  1215
      using openin_subtopology_Int_subset [of c] q t unfolding homeomorphism_def
lp15@63301
  1216
      by (metis inf.absorb_iff2 Int_commute ocv openin_euclidean_subtopology_iff)
lp15@63301
  1217
    then have os: "openin (subtopology euclidean s) (U \<inter> {z. q z \<in> t \<inter> V})"
lp15@63301
  1218
      using openin_trans [of U] by (simp add: Collect_conj_eq U)
lp15@63301
  1219
    show ?thesis
lp15@63301
  1220
      apply (rule_tac x = "p ` (t \<inter> V)" in exI)
lp15@63301
  1221
      apply (rule conjI)
lp15@63301
  1222
      apply (simp only: ptV os)
lp15@63301
  1223
      using \<open>p x = y\<close> \<open>x \<in> V\<close> \<open>x \<in> t\<close> apply blast
lp15@63301
  1224
      done
lp15@63301
  1225
  qed
lp15@63301
  1226
  with openin_subopen show ?thesis by blast
lp15@63301
  1227
qed
lp15@63301
  1228
lp15@63301
  1229
lemma covering_space_lift_unique_gen:
lp15@63301
  1230
  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
lp15@63301
  1231
  fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
lp15@63301
  1232
  assumes cov: "covering_space c p s"
lp15@63301
  1233
      and eq: "g1 a = g2 a"
lp15@63301
  1234
      and f: "continuous_on t f"  "f ` t \<subseteq> s"
lp15@63301
  1235
      and g1: "continuous_on t g1"  "g1 ` t \<subseteq> c"
lp15@63301
  1236
      and fg1: "\<And>x. x \<in> t \<Longrightarrow> f x = p(g1 x)"
lp15@63301
  1237
      and g2: "continuous_on t g2"  "g2 ` t \<subseteq> c"
lp15@63301
  1238
      and fg2: "\<And>x. x \<in> t \<Longrightarrow> f x = p(g2 x)"
lp15@63301
  1239
      and u_compt: "u \<in> components t" and "a \<in> u" "x \<in> u"
lp15@63301
  1240
    shows "g1 x = g2 x"
lp15@63301
  1241
proof -
lp15@63301
  1242
  have "u \<subseteq> t" by (rule in_components_subset [OF u_compt])
lp15@63301
  1243
  def G12 \<equiv> "{x \<in> u. g1 x - g2 x = 0}"
lp15@63301
  1244
  have "connected u" by (rule in_components_connected [OF u_compt])
lp15@63301
  1245
  have contu: "continuous_on u g1" "continuous_on u g2"
lp15@63301
  1246
       using \<open>u \<subseteq> t\<close> continuous_on_subset g1 g2 by blast+
lp15@63301
  1247
  have o12: "openin (subtopology euclidean u) G12"
lp15@63301
  1248
  unfolding G12_def
lp15@63301
  1249
  proof (subst openin_subopen, clarify)
lp15@63301
  1250
    fix z
lp15@63301
  1251
    assume z: "z \<in> u" "g1 z - g2 z = 0"
lp15@63301
  1252
    obtain v w q where "g1 z \<in> v" and ocv: "openin (subtopology euclidean c) v"
lp15@63301
  1253
                   and "p (g1 z) \<in> w" and osw: "openin (subtopology euclidean s) w"
lp15@63301
  1254
                   and hom: "homeomorphism v w p q"
lp15@63301
  1255
      apply (rule_tac x = "g1 z" in covering_space_local_homeomorphism [OF cov])
lp15@63301
  1256
       using \<open>u \<subseteq> t\<close> \<open>z \<in> u\<close> g1(2) apply blast+
lp15@63301
  1257
      done
lp15@63301
  1258
    have "g2 z \<in> v" using \<open>g1 z \<in> v\<close> z by auto
lp15@63301
  1259
    have gg: "{x \<in> u. g x \<in> v} = {x \<in> u. g x \<in> (v \<inter> g ` u)}" for g
lp15@63301
  1260
      by auto
lp15@63301
  1261
    have "openin (subtopology euclidean (g1 ` u)) (v \<inter> g1 ` u)"
lp15@63301
  1262
      using ocv \<open>u \<subseteq> t\<close> g1 by (fastforce simp add: openin_open)
lp15@63301
  1263
    then have 1: "openin (subtopology euclidean u) {x \<in> u. g1 x \<in> v}"
lp15@63301
  1264
      unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
lp15@63301
  1265
    have "openin (subtopology euclidean (g2 ` u)) (v \<inter> g2 ` u)"
lp15@63301
  1266
      using ocv \<open>u \<subseteq> t\<close> g2 by (fastforce simp add: openin_open)
lp15@63301
  1267
    then have 2: "openin (subtopology euclidean u) {x \<in> u. g2 x \<in> v}"
lp15@63301
  1268
      unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
lp15@63301
  1269
    show "\<exists>T. openin (subtopology euclidean u) T \<and>
lp15@63301
  1270
              z \<in> T \<and> T \<subseteq> {z \<in> u. g1 z - g2 z = 0}"
lp15@63301
  1271
      using z
lp15@63301
  1272
      apply (rule_tac x = "{x. x \<in> u \<and> g1 x \<in> v} \<inter> {x. x \<in> u \<and> g2 x \<in> v}" in exI)
lp15@63301
  1273
      apply (intro conjI)
lp15@63301
  1274
      apply (rule openin_Int [OF 1 2])
lp15@63301
  1275
      using \<open>g1 z \<in> v\<close>  \<open>g2 z \<in> v\<close>  apply (force simp:, clarify)
lp15@63301
  1276
      apply (metis \<open>u \<subseteq> t\<close> subsetD eq_iff_diff_eq_0 fg1 fg2 hom homeomorphism_def)
lp15@63301
  1277
      done
lp15@63301
  1278
  qed
lp15@63301
  1279
  have c12: "closedin (subtopology euclidean u) G12"
lp15@63301
  1280
    unfolding G12_def
lp15@63301
  1281
    by (intro continuous_intros continuous_closedin_preimage_constant contu)
lp15@63301
  1282
  have "G12 = {} \<or> G12 = u"
lp15@63301
  1283
    by (intro connected_clopen [THEN iffD1, rule_format] \<open>connected u\<close> conjI o12 c12)
lp15@63301
  1284
  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
  1285
  then show ?thesis
lp15@63301
  1286
    using \<open>x \<in> u\<close> by force
lp15@63301
  1287
qed
lp15@63301
  1288
lp15@63301
  1289
proposition covering_space_lift_unique:
lp15@63301
  1290
  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
lp15@63301
  1291
  fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
lp15@63301
  1292
  assumes "covering_space c p s"
lp15@63301
  1293
          "g1 a = g2 a"
lp15@63301
  1294
          "continuous_on t f"  "f ` t \<subseteq> s"
lp15@63301
  1295
          "continuous_on t g1"  "g1 ` t \<subseteq> c"  "\<And>x. x \<in> t \<Longrightarrow> f x = p(g1 x)"
lp15@63301
  1296
          "continuous_on t g2"  "g2 ` t \<subseteq> c"  "\<And>x. x \<in> t \<Longrightarrow> f x = p(g2 x)"
lp15@63301
  1297
          "connected t"  "a \<in> t"   "x \<in> t"
lp15@63301
  1298
   shows "g1 x = g2 x"
lp15@63301
  1299
using covering_space_lift_unique_gen [of c p s] in_components_self assms ex_in_conv by blast
lp15@63301
  1300
lp15@63130
  1301
end