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