src/HOL/Homology/Invariance_of_Domain.thy
author paulson <lp15@cam.ac.uk>
Thu Apr 11 15:26:04 2019 +0100 (6 months ago)
changeset 70125 b601c2c87076
parent 70114 089c17514794
child 70136 f03a01a18c6e
permissions -rw-r--r--
type instantiations for poly_mapping as a real_normed_vector
     1 section\<open>Invariance of Domain\<close>
     2 
     3 theory Invariance_of_Domain
     4   imports Brouwer_Degree "HOL-Analysis.Continuous_Extension" "HOL-Analysis.Homeomorphism"
     5 
     6 begin
     7 
     8 subsection\<open>Degree invariance mod 2 for map between pairs\<close>
     9 
    10 theorem Borsuk_odd_mapping_degree_step:
    11   assumes cmf: "continuous_map (nsphere n) (nsphere n) f"
    12     and f: "\<And>x. x \<in> topspace(nsphere n) \<Longrightarrow> (f \<circ> (\<lambda>x i. -x i)) x = ((\<lambda>x i. -x i) \<circ> f) x"
    13     and fim: "f ` (topspace(nsphere(n - Suc 0))) \<subseteq> topspace(nsphere(n - Suc 0))"
    14   shows "even (Brouwer_degree2 n f - Brouwer_degree2 (n - Suc 0) f)"
    15 proof (cases "n = 0")
    16   case False
    17   define neg where "neg \<equiv> \<lambda>x::nat\<Rightarrow>real. \<lambda>i. -x i"
    18   define upper where "upper \<equiv> \<lambda>n. {x::nat\<Rightarrow>real. x n \<ge> 0}"
    19   define lower where "lower \<equiv> \<lambda>n. {x::nat\<Rightarrow>real. x n \<le> 0}"
    20   define equator where "equator \<equiv> \<lambda>n. {x::nat\<Rightarrow>real. x n = 0}"
    21   define usphere where "usphere \<equiv> \<lambda>n. subtopology (nsphere n) (upper n)"
    22   define lsphere where "lsphere \<equiv> \<lambda>n. subtopology (nsphere n) (lower n)"
    23   have [simp]: "neg x i = -x i" for x i
    24     by (force simp: neg_def)
    25   have equator_upper: "equator n \<subseteq> upper n"
    26     by (force simp: equator_def upper_def)
    27   have upper_usphere: "subtopology (nsphere n) (upper n) = usphere n"
    28     by (simp add: usphere_def)
    29   let ?rhgn = "relative_homology_group n (nsphere n)"
    30   let ?hi_ee = "hom_induced n (nsphere n) (equator n) (nsphere n) (equator n)"
    31   interpret GE: comm_group "?rhgn (equator n)"
    32     by simp
    33   interpret HB: group_hom "?rhgn (equator n)"
    34                           "homology_group (int n - 1) (subtopology (nsphere n) (equator n))"
    35                           "hom_boundary n (nsphere n) (equator n)"
    36     by (simp add: group_hom_axioms_def group_hom_def hom_boundary_hom)
    37   interpret HIU: group_hom "?rhgn (equator n)"
    38                            "?rhgn (upper n)"
    39                            "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id"
    40     by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom)
    41   have subt_eq: "subtopology (nsphere n) {x. x n = 0} = nsphere (n - Suc 0)"
    42     by (metis False Suc_pred le_zero_eq not_le subtopology_nsphere_equator)
    43   then have equ: "subtopology (nsphere n) (equator n) = nsphere(n - Suc 0)"
    44     "subtopology (lsphere n) (equator n) = nsphere(n - Suc 0)"
    45     "subtopology (usphere n) (equator n) = nsphere(n - Suc 0)"
    46     using False by (auto simp: lsphere_def usphere_def equator_def lower_def upper_def subtopology_subtopology simp flip: Collect_conj_eq cong: rev_conj_cong)
    47   have cmr: "continuous_map (nsphere(n - Suc 0)) (nsphere(n - Suc 0)) f"
    48     by (metis (no_types, lifting) IntE cmf fim continuous_map_from_subtopology continuous_map_in_subtopology equ(1) image_subset_iff topspace_subtopology)
    49 
    50   have "f x n = 0" if "x \<in> topspace (nsphere n)" "x n = 0" for x
    51   proof -
    52     have "x \<in> topspace (nsphere (n - Suc 0))"
    53       by (simp add: that topspace_nsphere_minus1)
    54     moreover have "topspace (nsphere n) \<inter> {f. f n = 0} = topspace (nsphere (n - Suc 0))"
    55       by (metis subt_eq topspace_subtopology)
    56     ultimately show ?thesis
    57       using cmr continuous_map_def by fastforce
    58   qed
    59   then have fimeq: "f ` (topspace (nsphere n) \<inter> equator n) \<subseteq> topspace (nsphere n) \<inter> equator n"
    60     using fim cmf by (auto simp: equator_def continuous_map_def image_subset_iff)
    61   have "\<And>k. continuous_map (powertop_real UNIV) euclideanreal (\<lambda>x. - x k)"
    62     by (metis UNIV_I continuous_map_product_projection continuous_map_minus)
    63   then have cm_neg: "continuous_map (nsphere m) (nsphere m) neg" for m
    64     by (force simp: nsphere continuous_map_in_subtopology neg_def continuous_map_componentwise_UNIV intro: continuous_map_from_subtopology)
    65   then have cm_neg_lu: "continuous_map (lsphere n) (usphere n) neg"
    66       by (auto simp: lsphere_def usphere_def lower_def upper_def continuous_map_from_subtopology continuous_map_in_subtopology)
    67   have neg_in_top_iff: "neg x \<in> topspace(nsphere m) \<longleftrightarrow> x \<in> topspace(nsphere m)" for m x
    68     by (simp add: nsphere_def neg_def topspace_Euclidean_space)
    69   obtain z where zcarr: "z \<in> carrier (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))"
    70     and zeq: "subgroup_generated (reduced_homology_group (int n - 1) (nsphere (n - Suc 0))) {z}
    71               = reduced_homology_group (int n - 1) (nsphere (n - Suc 0))"
    72     using cyclic_reduced_homology_group_nsphere [of "int n - 1" "n - Suc 0"] by (auto simp: cyclic_group_def)
    73   have "hom_boundary n (subtopology (nsphere n) {x. x n \<le> 0}) {x. x n = 0}
    74       \<in> Group.iso (relative_homology_group n
    75                      (subtopology (nsphere n) {x. x n \<le> 0}) {x. x n = 0})
    76                   (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))"
    77     using iso_lower_hemisphere_reduced_homology_group [of "int n - 1" "n - Suc 0"] False by simp
    78   then obtain gp where g: "group_isomorphisms
    79                           (relative_homology_group n (subtopology (nsphere n) {x. x n \<le> 0}) {x. x n = 0})
    80                           (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))
    81                           (hom_boundary n (subtopology (nsphere n) {x. x n \<le> 0}) {x. x n = 0})
    82                           gp"
    83     by (auto simp: group.iso_iff_group_isomorphisms)
    84   then interpret gp: group_hom "reduced_homology_group (int n - 1) (nsphere (n - Suc 0))"
    85     "relative_homology_group n (subtopology (nsphere n) {x. x n \<le> 0}) {x. x n = 0}" gp
    86     by (simp add: group_hom_axioms_def group_hom_def group_isomorphisms_def)
    87   obtain zp where zpcarr: "zp \<in> carrier(relative_homology_group n (lsphere n) (equator n))"
    88     and zp_z: "hom_boundary n (lsphere n) (equator n) zp = z"
    89     and zp_sg: "subgroup_generated (relative_homology_group n (lsphere n) (equator n)) {zp}
    90                 = relative_homology_group n (lsphere n) (equator n)"
    91   proof
    92     show "gp z \<in> carrier (relative_homology_group n (lsphere n) (equator n))"
    93       "hom_boundary n (lsphere n) (equator n) (gp z) = z"
    94       using g zcarr by (auto simp: lsphere_def equator_def lower_def group_isomorphisms_def)
    95     have giso: "gp \<in> Group.iso (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))
    96                      (relative_homology_group n (subtopology (nsphere n) {x. x n \<le> 0}) {x. x n = 0})"
    97       by (metis (mono_tags, lifting) g group_isomorphisms_imp_iso group_isomorphisms_sym)
    98     show "subgroup_generated (relative_homology_group n (lsphere n) (equator n)) {gp z} =
    99         relative_homology_group n (lsphere n) (equator n)"
   100       apply (rule monoid.equality)
   101       using giso gp.subgroup_generated_by_image [of "{z}"] zcarr
   102       by (auto simp: lsphere_def equator_def lower_def zeq gp.iso_iff)
   103   qed
   104   have hb_iso: "hom_boundary n (subtopology (nsphere n) {x. x n \<ge> 0}) {x. x n = 0}
   105             \<in> iso (relative_homology_group n (subtopology (nsphere n) {x. x n \<ge> 0}) {x. x n = 0})
   106                   (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))"
   107     using iso_upper_hemisphere_reduced_homology_group [of "int n - 1" "n - Suc 0"] False by simp
   108   then obtain gn where g: "group_isomorphisms
   109                           (relative_homology_group n (subtopology (nsphere n) {x. x n \<ge> 0}) {x. x n = 0})
   110                           (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))
   111                           (hom_boundary n (subtopology (nsphere n) {x. x n \<ge> 0}) {x. x n = 0})
   112                           gn"
   113     by (auto simp: group.iso_iff_group_isomorphisms)
   114   then interpret gn: group_hom "reduced_homology_group (int n - 1) (nsphere (n - Suc 0))"
   115     "relative_homology_group n (subtopology (nsphere n) {x. x n \<ge> 0}) {x. x n = 0}" gn
   116     by (simp add: group_hom_axioms_def group_hom_def group_isomorphisms_def)
   117   obtain zn where zncarr: "zn \<in> carrier(relative_homology_group n (usphere n) (equator n))"
   118     and zn_z: "hom_boundary n (usphere n) (equator n) zn = z"
   119     and zn_sg: "subgroup_generated (relative_homology_group n (usphere n) (equator n)) {zn}
   120                  = relative_homology_group n (usphere n) (equator n)"
   121   proof
   122     show "gn z \<in> carrier (relative_homology_group n (usphere n) (equator n))"
   123       "hom_boundary n (usphere n) (equator n) (gn z) = z"
   124       using g zcarr by (auto simp: usphere_def equator_def upper_def group_isomorphisms_def)
   125     have giso: "gn \<in> Group.iso (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))
   126                      (relative_homology_group n (subtopology (nsphere n) {x. x n \<ge> 0}) {x. x n = 0})"
   127       by (metis (mono_tags, lifting) g group_isomorphisms_imp_iso group_isomorphisms_sym)
   128     show "subgroup_generated (relative_homology_group n (usphere n) (equator n)) {gn z} =
   129         relative_homology_group n (usphere n) (equator n)"
   130       apply (rule monoid.equality)
   131       using giso gn.subgroup_generated_by_image [of "{z}"] zcarr
   132       by (auto simp: usphere_def equator_def upper_def zeq gn.iso_iff)
   133   qed
   134   let ?hi_lu = "hom_induced n (lsphere n) (equator n) (nsphere n) (upper n) id"
   135   interpret gh_lu: group_hom "relative_homology_group n (lsphere n) (equator n)" "?rhgn (upper n)" ?hi_lu
   136     by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom)
   137   interpret gh_eef: group_hom "?rhgn (equator n)" "?rhgn (equator n)" "?hi_ee f"
   138     by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom)
   139   define wp where "wp \<equiv> ?hi_lu zp"
   140   then have wpcarr: "wp \<in> carrier(?rhgn (upper n))"
   141     by (simp add: hom_induced_carrier)
   142   have "hom_induced n (nsphere n) {} (nsphere n) {x. x n \<ge> 0} id
   143       \<in> iso (reduced_homology_group n (nsphere n))
   144             (?rhgn {x. x n \<ge> 0})"
   145     using iso_reduced_homology_group_upper_hemisphere [of n n n] by auto
   146   then have "carrier(?rhgn {x. x n \<ge> 0})
   147           \<subseteq> (hom_induced n (nsphere n) {} (nsphere n) {x. x n \<ge> 0} id)
   148                          ` carrier(reduced_homology_group n (nsphere n))"
   149     by (simp add: iso_iff)
   150   then obtain vp where vpcarr: "vp \<in> carrier(reduced_homology_group n (nsphere n))"
   151     and eqwp: "hom_induced n (nsphere n) {} (nsphere n) (upper n) id vp = wp"
   152     using wpcarr by (auto simp: upper_def)
   153   define wn where "wn \<equiv> hom_induced n (usphere n) (equator n) (nsphere n) (lower n) id zn"
   154   then have wncarr: "wn \<in> carrier(?rhgn (lower n))"
   155     by (simp add: hom_induced_carrier)
   156   have "hom_induced n (nsphere n) {} (nsphere n) {x. x n \<le> 0} id
   157       \<in> iso (reduced_homology_group n (nsphere n))
   158             (?rhgn {x. x n \<le> 0})"
   159     using iso_reduced_homology_group_lower_hemisphere [of n n n] by auto
   160   then have "carrier(?rhgn {x. x n \<le> 0})
   161           \<subseteq> (hom_induced n (nsphere n) {} (nsphere n) {x. x n \<le> 0} id)
   162                          ` carrier(reduced_homology_group n (nsphere n))"
   163     by (simp add: iso_iff)
   164   then obtain vn where vpcarr: "vn \<in> carrier(reduced_homology_group n (nsphere n))"
   165     and eqwp: "hom_induced n (nsphere n) {} (nsphere n) (lower n) id vn = wn"
   166     using wncarr by (auto simp: lower_def)
   167   define up where "up \<equiv> hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id zp"
   168   then have upcarr: "up \<in> carrier(?rhgn (equator n))"
   169     by (simp add: hom_induced_carrier)
   170   define un where "un \<equiv> hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id zn"
   171   then have uncarr: "un \<in> carrier(?rhgn (equator n))"
   172     by (simp add: hom_induced_carrier)
   173   have *: "(\<lambda>(x, y).
   174             hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id x
   175           \<otimes>\<^bsub>?rhgn (equator n)\<^esub>
   176             hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id y)
   177         \<in> Group.iso
   178             (relative_homology_group n (lsphere n) (equator n) \<times>\<times>
   179              relative_homology_group n (usphere n) (equator n))
   180             (?rhgn (equator n))"
   181   proof (rule conjunct1 [OF exact_sequence_sum_lemma [OF abelian_relative_homology_group]])
   182     show "hom_induced n (lsphere n) (equator n) (nsphere n) (upper n) id
   183         \<in> Group.iso (relative_homology_group n (lsphere n) (equator n))
   184             (?rhgn (upper n))"
   185       apply (simp add: lsphere_def usphere_def equator_def lower_def upper_def)
   186       using iso_relative_homology_group_lower_hemisphere by blast
   187     show "hom_induced n (usphere n) (equator n) (nsphere n) (lower n) id
   188         \<in> Group.iso (relative_homology_group n (usphere n) (equator n))
   189             (?rhgn (lower n))"
   190       apply (simp_all add: lsphere_def usphere_def equator_def lower_def upper_def)
   191       using iso_relative_homology_group_upper_hemisphere by blast+
   192     show "exact_seq
   193          ([?rhgn (lower n),
   194            ?rhgn (equator n),
   195            relative_homology_group n (lsphere n) (equator n)],
   196           [hom_induced n (nsphere n) (equator n) (nsphere n) (lower n) id,
   197            hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id])"
   198       unfolding lsphere_def usphere_def equator_def lower_def upper_def
   199       by (rule homology_exactness_triple_3) force
   200     show "exact_seq
   201          ([?rhgn (upper n),
   202            ?rhgn (equator n),
   203            relative_homology_group n (usphere n) (equator n)],
   204           [hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id,
   205            hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id])"
   206       unfolding lsphere_def usphere_def equator_def lower_def upper_def
   207       by (rule homology_exactness_triple_3) force
   208   next
   209     fix x
   210     assume "x \<in> carrier (relative_homology_group n (lsphere n) (equator n))"
   211     show "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id
   212          (hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id x) =
   213         hom_induced n (lsphere n) (equator n) (nsphere n) (upper n) id x"
   214       by (simp add: hom_induced_compose' subset_iff lsphere_def usphere_def equator_def lower_def upper_def)
   215   next
   216     fix x
   217     assume "x \<in> carrier (relative_homology_group n (usphere n) (equator n))"
   218     show "hom_induced n (nsphere n) (equator n) (nsphere n) (lower n) id
   219          (hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id x) =
   220         hom_induced n (usphere n) (equator n) (nsphere n) (lower n) id x"
   221       by (simp add: hom_induced_compose' subset_iff lsphere_def usphere_def equator_def lower_def upper_def)
   222   qed
   223   then have sb: "carrier (?rhgn (equator n))
   224              \<subseteq> (\<lambda>(x, y).
   225             hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id x
   226           \<otimes>\<^bsub>?rhgn (equator n)\<^esub>
   227             hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id y)
   228                ` carrier (relative_homology_group n (lsphere n) (equator n) \<times>\<times>
   229              relative_homology_group n (usphere n) (equator n))"
   230     by (simp add: iso_iff)
   231   obtain a b::int
   232     where up_ab: "?hi_ee f up
   233              = up [^]\<^bsub>?rhgn (equator n)\<^esub> a\<otimes>\<^bsub>?rhgn (equator n)\<^esub> un [^]\<^bsub>?rhgn (equator n)\<^esub> b"
   234   proof -
   235     have hiupcarr: "?hi_ee f up \<in> carrier(?rhgn (equator n))"
   236       by (simp add: hom_induced_carrier)
   237     obtain u v where u: "u \<in> carrier (relative_homology_group n (lsphere n) (equator n))"
   238       and v: "v \<in> carrier (relative_homology_group n (usphere n) (equator n))"
   239       and eq: "?hi_ee f up =
   240                 hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id u
   241                 \<otimes>\<^bsub>?rhgn (equator n)\<^esub>
   242                 hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id v"
   243       using subsetD [OF sb hiupcarr] by auto
   244     have "u \<in> carrier (subgroup_generated (relative_homology_group n (lsphere n) (equator n)) {zp})"
   245       by (simp_all add: u zp_sg)
   246     then obtain a::int where a: "u = zp [^]\<^bsub>relative_homology_group n (lsphere n) (equator n)\<^esub> a"
   247       by (metis group.carrier_subgroup_generated_by_singleton group_relative_homology_group rangeE zpcarr)
   248     have ae: "hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id
   249             (pow (relative_homology_group n (lsphere n) (equator n)) zp a)
   250           = pow (?rhgn (equator n)) (hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id zp) a"
   251       by (meson group_hom.hom_int_pow group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced zpcarr)
   252     have "v \<in> carrier (subgroup_generated (relative_homology_group n (usphere n) (equator n)) {zn})"
   253       by (simp_all add: v zn_sg)
   254     then obtain b::int where b: "v = zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> b"
   255       by (metis group.carrier_subgroup_generated_by_singleton group_relative_homology_group rangeE zncarr)
   256     have be: "hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id
   257            (zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> b)
   258         = hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id
   259            zn [^]\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub> b"
   260       by (meson group_hom.hom_int_pow group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced zncarr)
   261     show thesis
   262     proof
   263       show "?hi_ee f up
   264          = up [^]\<^bsub>?rhgn (equator n)\<^esub> a \<otimes>\<^bsub>?rhgn (equator n)\<^esub> un [^]\<^bsub>?rhgn (equator n)\<^esub> b"
   265         using a ae b be eq local.up_def un_def by auto
   266     qed
   267   qed
   268   have "(hom_boundary n (nsphere n) (equator n)
   269        \<circ> hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id) zp = z"
   270     using zp_z equ apply (simp add: lsphere_def naturality_hom_induced)
   271     by (metis hom_boundary_carrier hom_induced_id)
   272   then have up_z: "hom_boundary n (nsphere n) (equator n) up = z"
   273     by (simp add: up_def)
   274   have "(hom_boundary n (nsphere n) (equator n)
   275        \<circ> hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id) zn = z"
   276     using zn_z equ apply (simp add: usphere_def naturality_hom_induced)
   277     by (metis hom_boundary_carrier hom_induced_id)
   278   then have un_z: "hom_boundary n (nsphere n) (equator n) un = z"
   279     by (simp add: un_def)
   280   have Bd_ab: "Brouwer_degree2 (n - Suc 0) f = a + b"
   281   proof (rule Brouwer_degree2_unique_generator; use False int_ops in simp_all)
   282     show "continuous_map (nsphere (n - Suc 0)) (nsphere (n - Suc 0)) f"
   283       using cmr by auto
   284     show "subgroup_generated (reduced_homology_group (int n - 1) (nsphere (n - Suc 0))) {z} =
   285         reduced_homology_group (int n - 1) (nsphere (n - Suc 0))"
   286       using zeq by blast
   287     have "(hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} f
   288            \<circ> hom_boundary n (nsphere n) (equator n)) up
   289         = (hom_boundary n (nsphere n) (equator n) \<circ>
   290            ?hi_ee f) up"
   291       using naturality_hom_induced [OF cmf fimeq, of n, symmetric]
   292       by (simp add: subtopology_restrict equ fun_eq_iff)
   293     also have "\<dots> = hom_boundary n (nsphere n) (equator n)
   294                        (up [^]\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub>
   295                         a \<otimes>\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub>
   296                         un [^]\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub> b)"
   297       by (simp add: o_def up_ab)
   298     also have "\<dots> = z [^]\<^bsub>reduced_homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> (a + b)"
   299       using zcarr
   300       apply (simp add: HB.hom_int_pow reduced_homology_group_def group.int_pow_subgroup_generated upcarr uncarr)
   301       by (metis equ(1) group.int_pow_mult group_relative_homology_group hom_boundary_carrier un_z up_z)
   302   finally show "hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} f z =
   303         z [^]\<^bsub>reduced_homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> (a + b)"
   304       by (simp add: up_z)
   305   qed
   306   define u where "u \<equiv> up \<otimes>\<^bsub>?rhgn (equator n)\<^esub> inv\<^bsub>?rhgn (equator n)\<^esub> un"
   307   have ucarr: "u \<in> carrier (?rhgn (equator n))"
   308     by (simp add: u_def uncarr upcarr)
   309   then have "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f = u [^]\<^bsub>?rhgn (equator n)\<^esub> (a - b)
   310              \<longleftrightarrow> (GE.ord u) dvd a - b - Brouwer_degree2 n f"
   311     by (simp add: GE.int_pow_eq)
   312   moreover
   313   have "GE.ord u = 0"
   314   proof (clarsimp simp add: GE.ord_eq_0 ucarr)
   315     fix d :: nat
   316     assume "0 < d"
   317       and "u [^]\<^bsub>?rhgn (equator n)\<^esub> d = singular_relboundary_set n (nsphere n) (equator n)"
   318     then have "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id u [^]\<^bsub>?rhgn (upper n)\<^esub> d
   319                = \<one>\<^bsub>?rhgn (upper n)\<^esub>"
   320       by (metis HIU.hom_one HIU.hom_nat_pow one_relative_homology_group ucarr)
   321     moreover
   322     have "?hi_lu
   323         = hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id \<circ>
   324           hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id"
   325       by (simp add: lsphere_def image_subset_iff equator_upper flip: hom_induced_compose)
   326     then have p: "wp = hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id up"
   327       by (simp add: local.up_def wp_def)
   328     have n: "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id un = \<one>\<^bsub>?rhgn (upper n)\<^esub>"
   329       using homology_exactness_triple_3 [OF equator_upper, of n "nsphere n"]
   330       using un_def zncarr by (auto simp: upper_usphere kernel_def)
   331     have "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id u = wp"
   332       unfolding u_def
   333       using p n HIU.inv_one HIU.r_one uncarr upcarr by auto
   334     ultimately have "(wp [^]\<^bsub>?rhgn (upper n)\<^esub> d) = \<one>\<^bsub>?rhgn (upper n)\<^esub>"
   335       by simp
   336     moreover have "infinite (carrier (subgroup_generated (?rhgn (upper n)) {wp}))"
   337     proof -
   338       have "?rhgn (upper n) \<cong> reduced_homology_group n (nsphere n)"
   339         unfolding upper_def
   340         using iso_reduced_homology_group_upper_hemisphere [of n n n]
   341         by (blast intro: group.iso_sym group_reduced_homology_group is_isoI)
   342       also have "\<dots> \<cong> integer_group"
   343         by (simp add: reduced_homology_group_nsphere)
   344       finally have iso: "?rhgn (upper n) \<cong> integer_group" .
   345       have "carrier (subgroup_generated (?rhgn (upper n)) {wp}) = carrier (?rhgn (upper n))"
   346         using gh_lu.subgroup_generated_by_image [of "{zp}"] zpcarr HIU.carrier_subgroup_generated_subset
   347           gh_lu.iso_iff iso_relative_homology_group_lower_hemisphere zp_sg
   348         by (auto simp: lower_def lsphere_def upper_def equator_def wp_def)
   349       then show ?thesis
   350         using infinite_UNIV_int iso_finite [OF iso] by simp
   351     qed
   352     ultimately show False
   353       using HIU.finite_cyclic_subgroup \<open>0 < d\<close> wpcarr by blast
   354   qed
   355   ultimately have iff: "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f = u [^]\<^bsub>?rhgn (equator n)\<^esub> (a - b)
   356                    \<longleftrightarrow> Brouwer_degree2 n f = a - b"
   357     by auto
   358   have "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f = ?hi_ee f u"
   359   proof -
   360     have ne: "topspace (nsphere n) \<inter> equator n \<noteq> {}"
   361       by (metis equ(1) nonempty_nsphere topspace_subtopology)
   362     have eq1: "hom_boundary n (nsphere n) (equator n) u
   363                = \<one>\<^bsub>reduced_homology_group (int n - 1) (subtopology (nsphere n) (equator n))\<^esub>"
   364       using one_reduced_homology_group u_def un_z uncarr up_z upcarr by force
   365     then have uhom: "u \<in> hom_induced n (nsphere n) {} (nsphere n) (equator n) id `
   366                          carrier (reduced_homology_group (int n) (nsphere n))"
   367       using homology_exactness_reduced_1 [OF ne, of n] eq1 ucarr by (auto simp: kernel_def)
   368     then obtain v where vcarr: "v \<in> carrier (reduced_homology_group (int n) (nsphere n))"
   369                   and ueq: "u = hom_induced n (nsphere n) {} (nsphere n) (equator n) id v"
   370       by blast
   371     interpret GH_hi: group_hom "homology_group n (nsphere n)"
   372                         "?rhgn (equator n)"
   373                         "hom_induced n (nsphere n) {} (nsphere n) (equator n) id"
   374       by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom)
   375     have poweq: "pow (homology_group n (nsphere n)) x i = pow (reduced_homology_group n (nsphere n)) x i"
   376       for x and i::int
   377       by (simp add: False un_reduced_homology_group)
   378     have vcarr': "v \<in> carrier (homology_group n (nsphere n))"
   379       using carrier_reduced_homology_group_subset vcarr by blast
   380     have "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f
   381           = hom_induced n (nsphere n) {} (nsphere n) (equator n) f v"
   382       using vcarr vcarr'
   383       by (simp add: ueq poweq hom_induced_compose' cmf flip: GH_hi.hom_int_pow Brouwer_degree2)
   384     also have "\<dots> = hom_induced n (nsphere n) (topspace(nsphere n) \<inter> equator n) (nsphere n) (equator n) f
   385                      (hom_induced n (nsphere n) {} (nsphere n) (topspace(nsphere n) \<inter> equator n) id v)"
   386       using fimeq by (simp add: hom_induced_compose' cmf)
   387     also have "\<dots> = ?hi_ee f u"
   388       by (metis hom_induced inf.left_idem ueq)
   389     finally show ?thesis .
   390   qed
   391   moreover
   392   interpret gh_een: group_hom "?rhgn (equator n)" "?rhgn (equator n)" "?hi_ee neg"
   393     by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom)
   394   have hi_up_eq_un: "?hi_ee neg up = un [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg"
   395   proof -
   396     have "?hi_ee neg (hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id zp)
   397          = hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) (neg \<circ> id) zp"
   398       by (intro hom_induced_compose') (auto simp: lsphere_def equator_def cm_neg)
   399     also have "\<dots> = hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id
   400             (hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp)"
   401       by (subst hom_induced_compose' [OF cm_neg_lu]) (auto simp: usphere_def equator_def)
   402     also have "hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp
   403              = zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg"
   404     proof -
   405       let ?hb = "hom_boundary n (usphere n) (equator n)"
   406       have eq: "subtopology (nsphere n) {x. x n \<ge> 0} = usphere n \<and> {x. x n = 0} = equator n"
   407         by (auto simp: usphere_def upper_def equator_def)
   408       with hb_iso have inj: "inj_on (?hb) (carrier (relative_homology_group n (usphere n) (equator n)))"
   409         by (simp add: iso_iff)
   410       interpret hb_hom: group_hom "relative_homology_group n (usphere n) (equator n)"
   411                                   "reduced_homology_group (int n - 1) (nsphere (n - Suc 0))"
   412                                   "?hb"
   413         using hb_iso iso_iff eq group_hom_axioms_def group_hom_def by fastforce
   414       show ?thesis
   415       proof (rule inj_onD [OF inj])
   416         have *: "hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} neg z
   417                  = z [^]\<^bsub>homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> Brouwer_degree2 (n - Suc 0) neg"
   418           using Brouwer_degree2 [of z "n - Suc 0" neg] False zcarr
   419           by (simp add: int_ops group.int_pow_subgroup_generated reduced_homology_group_def)
   420         have "?hb \<circ>
   421               hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg
   422             = hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} neg \<circ>
   423               hom_boundary n (lsphere n) (equator n)"
   424           apply (subst naturality_hom_induced [OF cm_neg_lu])
   425            apply (force simp: equator_def neg_def)
   426           by (simp add: equ)
   427         then have "?hb
   428                     (hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp)
   429             = (z [^]\<^bsub>homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> Brouwer_degree2 (n - Suc 0) neg)"
   430           by (metis "*" comp_apply zp_z)
   431         also have "\<dots> = ?hb (zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub>
   432           Brouwer_degree2 (n - Suc 0) neg)"
   433           by (metis group.int_pow_subgroup_generated group_relative_homology_group hb_hom.hom_int_pow reduced_homology_group_def zcarr zn_z zncarr)
   434         finally show "?hb (hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp) =
   435         ?hb (zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub>
   436           Brouwer_degree2 (n - Suc 0) neg)" by simp
   437       qed (auto simp: hom_induced_carrier group.int_pow_closed zncarr)
   438     qed
   439     finally show ?thesis
   440       by (metis (no_types, lifting) group_hom.hom_int_pow group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced local.up_def un_def zncarr)
   441   qed
   442   have "continuous_map (nsphere (n - Suc 0)) (nsphere (n - Suc 0)) neg"
   443     using cm_neg by blast
   444   then have "homeomorphic_map (nsphere (n - Suc 0)) (nsphere (n - Suc 0)) neg"
   445     apply (auto simp: homeomorphic_map_maps homeomorphic_maps_def)
   446     apply (rule_tac x=neg in exI, auto)
   447     done
   448   then have Brouwer_degree2_21: "Brouwer_degree2 (n - Suc 0) neg ^ 2 = 1"
   449     using Brouwer_degree2_homeomorphic_map power2_eq_1_iff by force
   450   have hi_un_eq_up: "?hi_ee neg un = up [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg" (is "?f un = ?y")
   451   proof -
   452     have [simp]: "neg \<circ> neg = id"
   453       by force
   454     have "?f (?f ?y) = ?y"
   455       apply (subst hom_induced_compose' [OF cm_neg _ cm_neg])
   456        apply(force simp: equator_def)
   457       apply (simp add: upcarr hom_induced_id_gen)
   458       done
   459     moreover have "?f ?y = un"
   460       using upcarr apply (simp only: gh_een.hom_int_pow hi_up_eq_un)
   461       by (metis (no_types, lifting) Brouwer_degree2_21 GE.group_l_invI GE.l_inv_ex group.int_pow_1 group.int_pow_pow power2_eq_1_iff uncarr zmult_eq_1_iff)
   462     ultimately show "?f un = ?y"
   463       by simp
   464   qed
   465   have "?hi_ee f un = un [^]\<^bsub>?rhgn (equator n)\<^esub> a \<otimes>\<^bsub>?rhgn (equator n)\<^esub> up [^]\<^bsub>?rhgn (equator n)\<^esub> b"
   466   proof -
   467     let ?TE = "topspace (nsphere n) \<inter> equator n"
   468     have fneg: "(f \<circ> neg) x = (neg \<circ> f) x" if "x \<in> topspace (nsphere n)" for x
   469       using f [OF that] by (force simp: neg_def)
   470     have neg_im: "neg ` (topspace (nsphere n) \<inter> equator n) \<subseteq> topspace (nsphere n) \<inter> equator n"
   471       by (metis cm_neg continuous_map_image_subset_topspace equ(1) topspace_subtopology)
   472     have 1: "hom_induced n (nsphere n) ?TE (nsphere n) ?TE f \<circ> hom_induced n (nsphere n) ?TE (nsphere n) ?TE neg
   473            = hom_induced n (nsphere n) ?TE (nsphere n) ?TE neg \<circ> hom_induced n (nsphere n) ?TE (nsphere n) ?TE f"
   474       using neg_im fimeq cm_neg cmf
   475       apply (simp add: flip: hom_induced_compose del: hom_induced_restrict)
   476       using fneg by (auto intro: hom_induced_eq)
   477     have "(un [^]\<^bsub>?rhgn (equator n)\<^esub> a) \<otimes>\<^bsub>?rhgn (equator n)\<^esub> (up [^]\<^bsub>?rhgn (equator n)\<^esub> b)
   478         = un [^]\<^bsub>?rhgn (equator n)\<^esub> (Brouwer_degree2 (n - 1) neg * a * Brouwer_degree2 (n - 1) neg)
   479           \<otimes>\<^bsub>?rhgn (equator n)\<^esub>
   480           up [^]\<^bsub>?rhgn (equator n)\<^esub> (Brouwer_degree2 (n - 1) neg * b * Brouwer_degree2 (n - 1) neg)"
   481     proof -
   482       have "Brouwer_degree2 (n - Suc 0) neg = 1 \<or> Brouwer_degree2 (n - Suc 0) neg = - 1"
   483         using Brouwer_degree2_21 power2_eq_1_iff by blast
   484       then show ?thesis
   485         by fastforce
   486     qed
   487     also have "\<dots> = ((un [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - 1) neg) [^]\<^bsub>?rhgn (equator n)\<^esub> a \<otimes>\<^bsub>?rhgn (equator n)\<^esub>
   488            (up [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - 1) neg) [^]\<^bsub>?rhgn (equator n)\<^esub> b) [^]\<^bsub>?rhgn (equator n)\<^esub>
   489           Brouwer_degree2 (n - 1) neg"
   490       by (simp add: GE.int_pow_distrib GE.int_pow_pow uncarr upcarr)
   491     also have "\<dots> = ?hi_ee neg (?hi_ee f up) [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg"
   492       by (simp add: gh_een.hom_int_pow hi_un_eq_up hi_up_eq_un uncarr up_ab upcarr)
   493     finally have 2: "(un [^]\<^bsub>?rhgn (equator n)\<^esub> a) \<otimes>\<^bsub>?rhgn (equator n)\<^esub> (up [^]\<^bsub>?rhgn (equator n)\<^esub> b)
   494              = ?hi_ee neg (?hi_ee f up) [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg" .
   495     have "un = ?hi_ee neg up [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg"
   496       by (metis (no_types, hide_lams) Brouwer_degree2_21 GE.int_pow_1 GE.int_pow_pow hi_up_eq_un power2_eq_1_iff uncarr zmult_eq_1_iff)
   497     moreover have "?hi_ee f ((?hi_ee neg up) [^]\<^bsub>?rhgn (equator n)\<^esub> (Brouwer_degree2 (n - Suc 0) neg))
   498                  = un [^]\<^bsub>?rhgn (equator n)\<^esub> a \<otimes>\<^bsub>?rhgn (equator n)\<^esub> up [^]\<^bsub>?rhgn (equator n)\<^esub> b"
   499       using 1 2 by (simp add: hom_induced_carrier gh_eef.hom_int_pow fun_eq_iff)
   500     ultimately show ?thesis
   501       by blast
   502   qed
   503   then have "?hi_ee f u = u [^]\<^bsub>?rhgn (equator n)\<^esub> (a - b)"
   504     by (simp add: u_def upcarr uncarr up_ab GE.int_pow_diff GE.m_ac GE.int_pow_distrib GE.int_pow_inv GE.inv_mult_group)
   505   ultimately
   506   have "Brouwer_degree2 n f = a - b"
   507     using iff by blast
   508   with Bd_ab show ?thesis
   509     by simp
   510 qed simp
   511 
   512 
   513 subsection \<open>General Jordan-Brouwer separation theorem and invariance of dimension\<close>
   514 
   515 proposition relative_homology_group_Euclidean_complement_step:
   516   assumes "closedin (Euclidean_space n) S"
   517   shows "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S)
   518       \<cong> relative_homology_group (p + k) (Euclidean_space (n+k)) (topspace(Euclidean_space (n+k)) - S)"
   519 proof -
   520   have *: "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S)
   521            \<cong> relative_homology_group (p + 1) (Euclidean_space (Suc n)) (topspace(Euclidean_space (Suc n)) - {x \<in> S. x n = 0})"
   522     (is "?lhs \<cong> ?rhs")
   523     if clo: "closedin (Euclidean_space (Suc n)) S" and cong: "\<And>x y. \<lbrakk>x \<in> S; \<And>i. i \<noteq> n \<Longrightarrow> x i = y i\<rbrakk> \<Longrightarrow> y \<in> S"
   524       for p n S
   525   proof -
   526     have Ssub: "S \<subseteq> topspace (Euclidean_space (Suc n))"
   527       by (meson clo closedin_def)
   528     define lo where "lo \<equiv> {x \<in> topspace(Euclidean_space (Suc n)). x n < (if x \<in> S then 0 else 1)}"
   529     define hi where "hi = {x \<in> topspace(Euclidean_space (Suc n)). x n > (if x \<in> S then 0 else -1)}"
   530     have lo_hi_Int: "lo \<inter> hi = {x \<in> topspace(Euclidean_space (Suc n)) - S. x n \<in> {-1<..<1}}"
   531       by (auto simp: hi_def lo_def)
   532     have lo_hi_Un: "lo \<union> hi = topspace(Euclidean_space (Suc n)) - {x \<in> S. x n = 0}"
   533       by (auto simp: hi_def lo_def)
   534     define ret where "ret \<equiv> \<lambda>c::real. \<lambda>x i. if i = n then c else x i"
   535     have cm_ret: "continuous_map (powertop_real UNIV) (powertop_real UNIV) (ret t)" for t
   536       by (auto simp: ret_def continuous_map_componentwise_UNIV intro: continuous_map_product_projection)
   537     let ?ST = "\<lambda>t. subtopology (Euclidean_space (Suc n)) {x. x n = t}"
   538     define squashable where
   539       "squashable \<equiv> \<lambda>t S. \<forall>x t'. x \<in> S \<and> (x n \<le> t' \<and> t' \<le> t \<or> t \<le> t' \<and> t' \<le> x n) \<longrightarrow> ret t' x \<in> S"
   540     have squashable: "squashable t (topspace(Euclidean_space(Suc n)))" for t
   541       by (simp add: squashable_def topspace_Euclidean_space ret_def)
   542     have squashableD: "\<lbrakk>squashable t S; x \<in> S; x n \<le> t' \<and> t' \<le> t \<or> t \<le> t' \<and> t' \<le> x n\<rbrakk> \<Longrightarrow> ret t' x \<in> S" for x t' t S
   543       by (auto simp: squashable_def)
   544     have "squashable 1 hi"
   545       by (force simp: squashable_def hi_def ret_def topspace_Euclidean_space intro: cong)
   546     have "squashable t UNIV" for t
   547       by (force simp: squashable_def hi_def ret_def topspace_Euclidean_space intro: cong)
   548     have squashable_0_lohi: "squashable 0 (lo \<inter> hi)"
   549       using Ssub
   550       by (auto simp: squashable_def hi_def lo_def ret_def topspace_Euclidean_space intro: cong)
   551     have rm_ret: "retraction_maps (subtopology (Euclidean_space (Suc n)) U)
   552                                   (subtopology (Euclidean_space (Suc n)) {x. x \<in> U \<and> x n = t})
   553                                   (ret t) id"
   554       if "squashable t U" for t U
   555       unfolding retraction_maps_def
   556     proof (intro conjI ballI)
   557       show "continuous_map (subtopology (Euclidean_space (Suc n)) U)
   558              (subtopology (Euclidean_space (Suc n)) {x \<in> U. x n = t}) (ret t)"
   559         apply (simp add: cm_ret continuous_map_in_subtopology continuous_map_from_subtopology Euclidean_space_def)
   560         using that by (fastforce simp: squashable_def ret_def)
   561     next
   562       show "continuous_map (subtopology (Euclidean_space (Suc n)) {x \<in> U. x n = t})
   563                            (subtopology (Euclidean_space (Suc n)) U) id"
   564         using continuous_map_in_subtopology by fastforce
   565       show "ret t (id x) = x"
   566         if "x \<in> topspace (subtopology (Euclidean_space (Suc n)) {x \<in> U. x n = t})" for x
   567         using that by (simp add: topspace_Euclidean_space ret_def fun_eq_iff)
   568     qed
   569     have cm_snd: "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (powertop_real UNIV) S))
   570                               euclideanreal (\<lambda>x. snd x k)" for k::nat and S
   571       using continuous_map_componentwise_UNIV continuous_map_into_fulltopology continuous_map_snd by fastforce
   572     have cm_fstsnd: "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (powertop_real UNIV) S))
   573                               euclideanreal (\<lambda>x. fst x * snd x k)" for k::nat and S
   574       by (intro continuous_intros continuous_map_into_fulltopology [OF continuous_map_fst] cm_snd)
   575     have hw_sub: "homotopic_with (\<lambda>k. k ` V \<subseteq> V) (subtopology (Euclidean_space (Suc n)) U)
   576                                  (subtopology (Euclidean_space (Suc n)) U) (ret t) id"
   577       if "squashable t U" "squashable t V" for U V t
   578       unfolding homotopic_with_def
   579     proof (intro exI conjI allI ballI)
   580       let ?h = "\<lambda>(z,x). ret ((1 - z) * t + z * x n) x"
   581       show "(\<lambda>x. ?h (u, x)) ` V \<subseteq> V" if "u \<in> {0..1}" for u
   582         using that
   583         by clarsimp (metis squashableD [OF \<open>squashable t V\<close>] convex_bound_le diff_ge_0_iff_ge eq_diff_eq' le_cases less_eq_real_def segment_bound_lemma)
   584       have 1: "?h ` ({0..1} \<times> ({x. \<forall>i\<ge>Suc n. x i = 0} \<inter> U)) \<subseteq> U"
   585         by clarsimp (metis squashableD [OF \<open>squashable t U\<close>] convex_bound_le diff_ge_0_iff_ge eq_diff_eq' le_cases less_eq_real_def segment_bound_lemma)
   586       show "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (Euclidean_space (Suc n)) U))
   587                            (subtopology (Euclidean_space (Suc n)) U) ?h"
   588         apply (simp add: continuous_map_in_subtopology Euclidean_space_def subtopology_subtopology 1)
   589         apply (auto simp: case_prod_unfold ret_def continuous_map_componentwise_UNIV)
   590          apply (intro continuous_map_into_fulltopology [OF continuous_map_fst] cm_snd continuous_intros)
   591         by (auto simp: cm_snd)
   592     qed (auto simp: ret_def)
   593     have cs_hi: "contractible_space(subtopology (Euclidean_space(Suc n)) hi)"
   594     proof -
   595       have "homotopic_with (\<lambda>x. True) (?ST 1) (?ST 1) id (\<lambda>x. (\<lambda>i. if i = n then 1 else 0))"
   596         apply (subst homotopic_with_sym)
   597         apply (simp add: homotopic_with)
   598         apply (rule_tac x="(\<lambda>(z,x) i. if i=n then 1 else z * x i)" in exI)
   599         apply (auto simp: Euclidean_space_def subtopology_subtopology continuous_map_in_subtopology case_prod_unfold continuous_map_componentwise_UNIV cm_fstsnd)
   600         done
   601       then have "contractible_space (?ST 1)"
   602         unfolding contractible_space_def by metis
   603       moreover have "?thesis = contractible_space (?ST 1)"
   604       proof (intro deformation_retract_imp_homotopy_equivalent_space homotopy_equivalent_space_contractibility)
   605         have "{x. \<forall>i\<ge>Suc n. x i = 0} \<inter> {x \<in> hi. x n = 1} = {x. \<forall>i\<ge>Suc n. x i = 0} \<inter> {x. x n = 1}"
   606           by (auto simp: hi_def topspace_Euclidean_space)
   607         then have eq: "subtopology (Euclidean_space (Suc n)) {x. x \<in> hi \<and> x n = 1} = ?ST 1"
   608           by (simp add: Euclidean_space_def subtopology_subtopology)
   609         show "homotopic_with (\<lambda>x. True) (subtopology (Euclidean_space (Suc n)) hi) (subtopology (Euclidean_space (Suc n)) hi) (ret 1) id"
   610           using hw_sub [OF \<open>squashable 1 hi\<close> \<open>squashable 1 UNIV\<close>] eq by simp
   611         show "retraction_maps (subtopology (Euclidean_space (Suc n)) hi) (?ST 1) (ret 1) id"
   612           using rm_ret [OF \<open>squashable 1 hi\<close>] eq by simp
   613       qed
   614       ultimately show ?thesis by metis
   615     qed
   616     have "?lhs \<cong> relative_homology_group p (Euclidean_space (Suc n)) (lo \<inter> hi)"
   617     proof (rule group.iso_sym [OF _ deformation_retract_imp_isomorphic_relative_homology_groups])
   618       have "{x. \<forall>i\<ge>Suc n. x i = 0} \<inter> {x. x n = 0} = {x. \<forall>i\<ge>n. x i = (0::real)}"
   619         by auto (metis le_less_Suc_eq not_le)
   620       then have "?ST 0 = Euclidean_space n"
   621         by (simp add: Euclidean_space_def subtopology_subtopology)
   622       then show "retraction_maps (Euclidean_space (Suc n)) (Euclidean_space n) (ret 0) id"
   623         using rm_ret [OF \<open>squashable 0 UNIV\<close>] by auto
   624       then have "ret 0 x \<in> topspace (Euclidean_space n)"
   625         if "x \<in> topspace (Euclidean_space (Suc n))" "-1 < x n" "x n < 1" for x
   626         using that by (simp add: continuous_map_def retraction_maps_def)
   627       then show "(ret 0) ` (lo \<inter> hi) \<subseteq> topspace (Euclidean_space n) - S"
   628         by (auto simp: local.cong ret_def hi_def lo_def)
   629       show "homotopic_with (\<lambda>h. h ` (lo \<inter> hi) \<subseteq> lo \<inter> hi) (Euclidean_space (Suc n)) (Euclidean_space (Suc n)) (ret 0) id"
   630         using hw_sub [OF squashable squashable_0_lohi] by simp
   631     qed (auto simp: lo_def hi_def Euclidean_space_def)
   632     also have "\<dots> \<cong> relative_homology_group p (subtopology (Euclidean_space (Suc n)) hi) (lo \<inter> hi)"
   633     proof (rule group.iso_sym [OF _ isomorphic_relative_homology_groups_inclusion_contractible])
   634       show "contractible_space (subtopology (Euclidean_space (Suc n)) hi)"
   635         by (simp add: cs_hi)
   636       show "topspace (Euclidean_space (Suc n)) \<inter> hi \<noteq> {}"
   637         apply (simp add: hi_def topspace_Euclidean_space set_eq_iff)
   638         apply (rule_tac x="\<lambda>i. if i = n then 1 else 0" in exI, auto)
   639         done
   640     qed auto
   641     also have "\<dots> \<cong> relative_homology_group p (subtopology (Euclidean_space (Suc n)) (lo \<union> hi)) lo"
   642     proof -
   643       have oo: "openin (Euclidean_space (Suc n)) {x \<in> topspace (Euclidean_space (Suc n)). x n \<in> A}"
   644         if "open A" for A
   645       proof (rule openin_continuous_map_preimage)
   646         show "continuous_map (Euclidean_space (Suc n)) euclideanreal (\<lambda>x. x n)"
   647         proof -
   648           have "\<forall>n f. continuous_map (product_topology f UNIV) (f (n::nat)) (\<lambda>f. f n::real)"
   649             by (simp add: continuous_map_product_projection)
   650           then show ?thesis
   651             using Euclidean_space_def continuous_map_from_subtopology
   652             by (metis (mono_tags))
   653         qed
   654       qed (auto intro: that)
   655       have "openin (Euclidean_space(Suc n)) lo"
   656         apply (simp add: openin_subopen [of _ lo])
   657         apply (simp add: lo_def, safe)
   658          apply (force intro: oo [of "lessThan 0", simplified] open_Collect_less)
   659         apply (rule_tac x="{x \<in> topspace(Euclidean_space(Suc n)). x n < 1}
   660                             \<inter> (topspace(Euclidean_space(Suc n)) - S)" in exI)
   661         using clo apply (force intro: oo [of "lessThan 1", simplified] open_Collect_less)
   662         done
   663       moreover have "openin (Euclidean_space(Suc n)) hi"
   664         apply (simp add: openin_subopen [of _ hi])
   665         apply (simp add: hi_def, safe)
   666          apply (force intro: oo [of "greaterThan 0", simplified] open_Collect_less)
   667         apply (rule_tac x="{x \<in> topspace(Euclidean_space(Suc n)). x n > -1}
   668                                 \<inter> (topspace(Euclidean_space(Suc n)) - S)" in exI)
   669         using clo apply (force intro: oo [of "greaterThan (-1)", simplified] open_Collect_less)
   670         done
   671       ultimately
   672       have *: "subtopology (Euclidean_space (Suc n)) (lo \<union> hi) closure_of
   673                    (topspace (subtopology (Euclidean_space (Suc n)) (lo \<union> hi)) - hi)
   674                    \<subseteq> subtopology (Euclidean_space (Suc n)) (lo \<union> hi) interior_of lo"
   675         by (metis (no_types, lifting) Diff_idemp Diff_subset_conv Un_commute Un_upper2 closure_of_interior_of interior_of_closure_of interior_of_complement interior_of_eq lo_hi_Un openin_Un openin_open_subtopology topspace_subtopology_subset)
   676       have eq: "((lo \<union> hi) \<inter> (lo \<union> hi - (topspace (Euclidean_space (Suc n)) \<inter> (lo \<union> hi) - hi))) = hi"
   677         "(lo - (topspace (Euclidean_space (Suc n)) \<inter> (lo \<union> hi) - hi)) = lo \<inter> hi"
   678         by (auto simp: lo_def hi_def Euclidean_space_def)
   679       show ?thesis
   680         using homology_excision_axiom [OF *, of "lo \<union> hi" p]
   681         by (force simp: subtopology_subtopology eq is_iso_def)
   682     qed
   683     also have "\<dots> \<cong> relative_homology_group (p + 1 - 1) (subtopology (Euclidean_space (Suc n)) (lo \<union> hi)) lo"
   684       by simp
   685     also have "\<dots> \<cong> relative_homology_group (p + 1) (Euclidean_space (Suc n)) (lo \<union> hi)"
   686     proof (rule group.iso_sym [OF _ isomorphic_relative_homology_groups_relboundary_contractible])
   687       have proj: "continuous_map (powertop_real UNIV) euclideanreal (\<lambda>f. f n)"
   688         by (metis UNIV_I continuous_map_product_projection)
   689       have hilo: "\<And>x. x \<in> hi \<Longrightarrow> (\<lambda>i. if i = n then - x i else x i) \<in> lo"
   690                  "\<And>x. x \<in> lo \<Longrightarrow> (\<lambda>i. if i = n then - x i else x i) \<in> hi"
   691         using local.cong
   692         by (auto simp: hi_def lo_def topspace_Euclidean_space split: if_split_asm)
   693       have "subtopology (Euclidean_space (Suc n)) hi homeomorphic_space subtopology (Euclidean_space (Suc n)) lo"
   694         unfolding homeomorphic_space_def
   695         apply (rule_tac x="\<lambda>x i. if i = n then -(x i) else x i" in exI)+
   696         using proj
   697         apply (auto simp: homeomorphic_maps_def Euclidean_space_def continuous_map_in_subtopology
   698                           hilo continuous_map_componentwise_UNIV continuous_map_from_subtopology continuous_map_minus
   699                     intro: continuous_map_from_subtopology continuous_map_product_projection)
   700         done
   701       then have "contractible_space(subtopology (Euclidean_space(Suc n)) hi)
   702              \<longleftrightarrow> contractible_space (subtopology (Euclidean_space (Suc n)) lo)"
   703         by (rule homeomorphic_space_contractibility)
   704       then show "contractible_space (subtopology (Euclidean_space (Suc n)) lo)"
   705         using cs_hi by auto
   706       show "topspace (Euclidean_space (Suc n)) \<inter> lo \<noteq> {}"
   707         apply (simp add: lo_def Euclidean_space_def set_eq_iff)
   708         apply (rule_tac x="\<lambda>i. if i = n then -1 else 0" in exI, auto)
   709         done
   710     qed auto
   711     also have "\<dots> \<cong> ?rhs"
   712       by (simp flip: lo_hi_Un)
   713     finally show ?thesis .
   714   qed
   715   show ?thesis
   716   proof (induction k)
   717     case (Suc m)
   718     with assms obtain T where cloT: "closedin (powertop_real UNIV) T"
   719                          and SeqT: "S = T \<inter> {x. \<forall>i\<ge>n. x i = 0}"
   720       by (auto simp: Euclidean_space_def closedin_subtopology)
   721     then have "closedin (Euclidean_space (m + n)) S"
   722       apply (simp add: Euclidean_space_def closedin_subtopology)
   723       apply (rule_tac x="T \<inter> topspace(Euclidean_space n)" in exI)
   724       using closedin_Euclidean_space topspace_Euclidean_space by force
   725     moreover have "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - S)
   726                 \<cong> relative_homology_group (p + 1) (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - S)"
   727       if "closedin (Euclidean_space n) S" for p n
   728     proof -
   729       define S' where "S' \<equiv> {x \<in> topspace(Euclidean_space(Suc n)). (\<lambda>i. if i < n then x i else 0) \<in> S}"
   730       have Ssub_n: "S \<subseteq> topspace (Euclidean_space n)"
   731         by (meson that closedin_def)
   732       have "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S')
   733            \<cong> relative_homology_group (p + 1) (Euclidean_space (Suc n)) (topspace(Euclidean_space (Suc n)) - {x \<in> S'. x n = 0})"
   734       proof (rule *)
   735         have cm: "continuous_map (powertop_real UNIV) euclideanreal (\<lambda>f. f u)" for u
   736           by (metis UNIV_I continuous_map_product_projection)
   737         have "continuous_map (subtopology (powertop_real UNIV) {x. \<forall>i>n. x i = 0}) euclideanreal
   738                 (\<lambda>x. if k \<le> n then x k else 0)" for k
   739           by (simp add: continuous_map_from_subtopology [OF cm])
   740         moreover have "\<forall>i\<ge>n. (if i < n then x i else 0) = 0"
   741           if "x \<in> topspace (subtopology (powertop_real UNIV) {x. \<forall>i>n. x i = 0})" for x
   742           using that by simp
   743         ultimately have "continuous_map (Euclidean_space (Suc n)) (Euclidean_space n) (\<lambda>x i. if i < n then x i else 0)"
   744           by (simp add: Euclidean_space_def continuous_map_in_subtopology continuous_map_componentwise_UNIV
   745                         continuous_map_from_subtopology [OF cm] image_subset_iff)
   746         then show "closedin (Euclidean_space (Suc n)) S'"
   747           unfolding S'_def using that by (rule closedin_continuous_map_preimage)
   748       next
   749         fix x y
   750         assume xy: "\<And>i. i \<noteq> n \<Longrightarrow> x i = y i" "x \<in> S'"
   751         then have "(\<lambda>i. if i < n then x i else 0) = (\<lambda>i. if i < n then y i else 0)"
   752           by (simp add: S'_def Euclidean_space_def fun_eq_iff)
   753         with xy show "y \<in> S'"
   754           by (simp add: S'_def Euclidean_space_def)
   755       qed
   756       moreover
   757       have abs_eq: "(\<lambda>i. if i < n then x i else 0) = x" if "\<And>i. i \<ge> n \<Longrightarrow> x i = 0" for x :: "nat \<Rightarrow> real" and n
   758         using that by auto
   759       then have "topspace (Euclidean_space n) - S' = topspace (Euclidean_space n) - S"
   760         by (simp add: S'_def Euclidean_space_def set_eq_iff cong: conj_cong)
   761       moreover
   762       have "topspace (Euclidean_space (Suc n)) - {x \<in> S'. x n = 0} = topspace (Euclidean_space (Suc n)) - S"
   763         using Ssub_n
   764         apply (auto simp: S'_def subset_iff Euclidean_space_def set_eq_iff abs_eq  cong: conj_cong)
   765         by (metis abs_eq le_antisym not_less_eq_eq)
   766       ultimately show ?thesis
   767         by simp
   768     qed
   769     ultimately have "relative_homology_group (p + m)(Euclidean_space (m + n))(topspace (Euclidean_space (m + n)) - S)
   770             \<cong> relative_homology_group (p + m + 1) (Euclidean_space (Suc (m + n))) (topspace (Euclidean_space (Suc (m + n))) - S)"
   771       by (metis \<open>closedin (Euclidean_space (m + n)) S\<close>)
   772     then show ?case
   773       using Suc.IH iso_trans by (force simp: algebra_simps)
   774   qed (simp add: iso_refl)
   775 qed
   776 
   777 lemma iso_Euclidean_complements_lemma1:
   778   assumes S: "closedin (Euclidean_space m) S" and cmf: "continuous_map(subtopology (Euclidean_space m) S) (Euclidean_space n) f"
   779   obtains g where "continuous_map (Euclidean_space m) (Euclidean_space n) g"
   780                   "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
   781 proof -
   782   have cont: "continuous_on (topspace (Euclidean_space m) \<inter> S) (\<lambda>x. f x i)" for i
   783     by (metis (no_types) continuous_on_product_then_coordinatewise
   784             cm_Euclidean_space_iff_continuous_on cmf topspace_subtopology)
   785   have "f ` (topspace (Euclidean_space m) \<inter> S) \<subseteq> topspace (Euclidean_space n)"
   786     using cmf continuous_map_image_subset_topspace by fastforce
   787   then
   788   have "\<exists>g. continuous_on (topspace (Euclidean_space m)) g \<and> (\<forall>x \<in> S. g x = f x i)" for i
   789     using S Tietze_unbounded [OF cont [of i]]
   790     by (metis closedin_Euclidean_space_iff closedin_closed_Int topspace_subtopology topspace_subtopology_subset)
   791   then obtain g where cmg: "\<And>i. continuous_map (Euclidean_space m) euclideanreal (g i)"
   792     and gf: "\<And>i x. x \<in> S \<Longrightarrow> g i x = f x i"
   793     unfolding continuous_map_Euclidean_space_iff by metis
   794   let ?GG = "\<lambda>x i. if i < n then g i x else 0"
   795   show thesis
   796   proof
   797     show "continuous_map (Euclidean_space m) (Euclidean_space n) ?GG"
   798       unfolding Euclidean_space_def [of n]
   799       by (auto simp: continuous_map_in_subtopology continuous_map_componentwise cmg)
   800     show "?GG x = f x" if "x \<in> S" for x
   801     proof -
   802       have "S \<subseteq> topspace (Euclidean_space m)"
   803         by (meson S closedin_def)
   804       then have "f x \<in> topspace (Euclidean_space n)"
   805         using cmf that unfolding continuous_map_def topspace_subtopology by blast
   806       then show ?thesis
   807         by (force simp: topspace_Euclidean_space gf that)
   808     qed
   809   qed
   810 qed
   811 
   812 
   813 lemma iso_Euclidean_complements_lemma2:
   814   assumes S: "closedin (Euclidean_space m) S"
   815       and T: "closedin (Euclidean_space n) T"
   816       and hom: "homeomorphic_map (subtopology (Euclidean_space m) S) (subtopology (Euclidean_space n) T) f"
   817   obtains g where "homeomorphic_map (prod_topology (Euclidean_space m) (Euclidean_space n))
   818                                     (prod_topology (Euclidean_space n) (Euclidean_space m)) g"
   819                   "\<And>x. x \<in> S \<Longrightarrow> g(x,(\<lambda>i. 0)) = (f x,(\<lambda>i. 0))"
   820 proof -
   821   obtain g where cmf: "continuous_map (subtopology (Euclidean_space m) S) (subtopology (Euclidean_space n) T) f"
   822            and cmg: "continuous_map (subtopology (Euclidean_space n) T) (subtopology (Euclidean_space m) S) g"
   823            and gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
   824            and fg: "\<And>y. y \<in> T \<Longrightarrow> f (g y) = y"
   825     using hom S T closedin_subset unfolding homeomorphic_map_maps homeomorphic_maps_def
   826     by fastforce
   827   obtain f' where cmf': "continuous_map (Euclidean_space m) (Euclidean_space n) f'"
   828              and f'f: "\<And>x. x \<in> S \<Longrightarrow> f' x = f x"
   829     using iso_Euclidean_complements_lemma1 S cmf continuous_map_into_fulltopology by metis
   830   obtain g' where cmg': "continuous_map (Euclidean_space n) (Euclidean_space m) g'"
   831              and g'g: "\<And>x. x \<in> T \<Longrightarrow> g' x = g x"
   832     using iso_Euclidean_complements_lemma1 T cmg continuous_map_into_fulltopology by metis
   833   define p  where "p \<equiv> \<lambda>(x,y). (x,(\<lambda>i. y i + f' x i))"
   834   define p' where "p' \<equiv> \<lambda>(x,y). (x,(\<lambda>i. y i - f' x i))"
   835   define q  where "q \<equiv> \<lambda>(x,y). (x,(\<lambda>i. y i + g' x i))"
   836   define q' where "q' \<equiv> \<lambda>(x,y). (x,(\<lambda>i. y i - g' x i))"
   837   have "homeomorphic_maps (prod_topology (Euclidean_space m) (Euclidean_space n))
   838                           (prod_topology (Euclidean_space m) (Euclidean_space n))
   839                           p p'"
   840        "homeomorphic_maps (prod_topology (Euclidean_space n) (Euclidean_space m))
   841                           (prod_topology (Euclidean_space n) (Euclidean_space m))
   842                           q q'"
   843        "homeomorphic_maps (prod_topology (Euclidean_space m) (Euclidean_space n))
   844                           (prod_topology (Euclidean_space n) (Euclidean_space m)) (\<lambda>(x,y). (y,x)) (\<lambda>(x,y). (y,x))"
   845     apply (simp_all add: p_def p'_def q_def q'_def homeomorphic_maps_def continuous_map_pairwise)
   846     apply (force simp: case_prod_unfold continuous_map_of_fst [unfolded o_def] cmf' cmg' intro: continuous_intros)+
   847     done
   848   then have "homeomorphic_maps (prod_topology (Euclidean_space m) (Euclidean_space n))
   849                           (prod_topology (Euclidean_space n) (Euclidean_space m))
   850                           (q' \<circ> (\<lambda>(x,y). (y,x)) \<circ> p) (p' \<circ> ((\<lambda>(x,y). (y,x)) \<circ> q))"
   851     using homeomorphic_maps_compose homeomorphic_maps_sym by (metis (no_types, lifting))
   852   moreover
   853   have "\<And>x. x \<in> S \<Longrightarrow> (q' \<circ> (\<lambda>(x,y). (y,x)) \<circ> p) (x, \<lambda>i. 0) = (f x, \<lambda>i. 0)"
   854     apply (simp add: q'_def p_def f'f)
   855     apply (simp add: fun_eq_iff)
   856     by (metis S T closedin_subset g'g gf hom homeomorphic_imp_surjective_map image_eqI topspace_subtopology_subset)
   857   ultimately
   858   show thesis
   859     using homeomorphic_map_maps that by blast
   860 qed
   861 
   862 
   863 proposition isomorphic_relative_homology_groups_Euclidean_complements:
   864   assumes S: "closedin (Euclidean_space n) S" and T: "closedin (Euclidean_space n) T"
   865    and hom: "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)"
   866    shows "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S)
   867           \<cong> relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - T)"
   868 proof -
   869   have subST: "S \<subseteq> topspace(Euclidean_space n)" "T \<subseteq> topspace(Euclidean_space n)"
   870     by (meson S T closedin_def)+
   871   have "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - S)
   872         \<cong> relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - S)"
   873     using relative_homology_group_Euclidean_complement_step [OF S] by blast
   874   moreover have "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - T)
   875         \<cong> relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - T)"
   876     using relative_homology_group_Euclidean_complement_step [OF T] by blast
   877   moreover have "relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - S)
   878                \<cong> relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - T)"
   879   proof -
   880     obtain f where f: "homeomorphic_map (subtopology (Euclidean_space n) S)
   881                                         (subtopology (Euclidean_space n) T) f"
   882       using hom unfolding homeomorphic_space by blast
   883     obtain g where g: "homeomorphic_map (prod_topology (Euclidean_space n) (Euclidean_space n))
   884                                         (prod_topology (Euclidean_space n) (Euclidean_space n)) g"
   885               and gf: "\<And>x. x \<in> S \<Longrightarrow> g(x,(\<lambda>i. 0)) = (f x,(\<lambda>i. 0))"
   886       using S T f iso_Euclidean_complements_lemma2 by blast
   887     define h where "h \<equiv> \<lambda>x::nat \<Rightarrow>real. ((\<lambda>i. if i < n then x i else 0), (\<lambda>j. if j < n then x(n + j) else 0))"
   888     define k where "k \<equiv> \<lambda>(x,y) i. if i < 2 * n then if i < n then x i else y(i - n) else (0::real)"
   889     have hk: "homeomorphic_maps (Euclidean_space(2 * n)) (prod_topology (Euclidean_space n) (Euclidean_space n)) h k"
   890       unfolding homeomorphic_maps_def
   891     proof safe
   892       show "continuous_map (Euclidean_space (2 * n))
   893                            (prod_topology (Euclidean_space n) (Euclidean_space n)) h"
   894         apply (simp add: h_def continuous_map_pairwise o_def continuous_map_componentwise_Euclidean_space)
   895         unfolding Euclidean_space_def
   896         by (metis (mono_tags) UNIV_I continuous_map_from_subtopology continuous_map_product_projection)
   897       have "continuous_map (prod_topology (Euclidean_space n) (Euclidean_space n)) euclideanreal (\<lambda>p. fst p i)" for i
   898         using Euclidean_space_def continuous_map_into_fulltopology continuous_map_fst by fastforce
   899       moreover
   900       have "continuous_map (prod_topology (Euclidean_space n) (Euclidean_space n)) euclideanreal (\<lambda>p. snd p (i - n))" for i
   901         using Euclidean_space_def continuous_map_into_fulltopology continuous_map_snd by fastforce
   902       ultimately
   903       show "continuous_map (prod_topology (Euclidean_space n) (Euclidean_space n))
   904                            (Euclidean_space (2 * n)) k"
   905         by (simp add: k_def continuous_map_pairwise o_def continuous_map_componentwise_Euclidean_space case_prod_unfold)
   906     qed (auto simp: k_def h_def fun_eq_iff topspace_Euclidean_space)
   907     define kgh where "kgh \<equiv> k \<circ> g \<circ> h"
   908     let ?i = "hom_induced (p + n) (Euclidean_space(2 * n)) (topspace(Euclidean_space(2 * n)) - S)
   909                                  (Euclidean_space(2 * n)) (topspace(Euclidean_space(2 * n)) - T) kgh"
   910     have "?i \<in> iso (relative_homology_group (p + int n) (Euclidean_space (2 * n))
   911                     (topspace (Euclidean_space (2 * n)) - S))
   912                    (relative_homology_group (p + int n) (Euclidean_space (2 * n))
   913                     (topspace (Euclidean_space (2 * n)) - T))"
   914     proof (rule homeomorphic_map_relative_homology_iso)
   915       show hm: "homeomorphic_map (Euclidean_space (2 * n)) (Euclidean_space (2 * n)) kgh"
   916         unfolding kgh_def by (meson hk g homeomorphic_map_maps homeomorphic_maps_compose homeomorphic_maps_sym)
   917       have Teq: "T = f ` S"
   918         using f homeomorphic_imp_surjective_map subST(1) subST(2) topspace_subtopology_subset by blast
   919       have khf: "\<And>x. x \<in> S \<Longrightarrow> k(h(f x)) = f x"
   920         by (metis (no_types, lifting) Teq hk homeomorphic_maps_def image_subset_iff le_add1 mult_2 subST(2) subsetD subset_Euclidean_space)
   921       have gh: "g(h x) = h(f x)" if "x \<in> S" for x
   922       proof -
   923         have [simp]: "(\<lambda>i. if i < n then x i else 0) = x"
   924           using subST(1) that topspace_Euclidean_space by (auto simp: fun_eq_iff)
   925         have "f x \<in> topspace(Euclidean_space n)"
   926           using Teq subST(2) that by blast
   927         moreover have "(\<lambda>j. if j < n then x (n + j) else 0) = (\<lambda>j. 0::real)"
   928           using Euclidean_space_def subST(1) that by force
   929         ultimately show ?thesis
   930           by (simp add: topspace_Euclidean_space h_def gf \<open>x \<in> S\<close> fun_eq_iff)
   931       qed
   932       have *: "\<lbrakk>S \<subseteq> U; T \<subseteq> U; kgh ` U = U; inj_on kgh U; kgh ` S = T\<rbrakk> \<Longrightarrow> kgh ` (U - S) = U - T" for U
   933         unfolding inj_on_def set_eq_iff by blast
   934       show "kgh ` (topspace (Euclidean_space (2 * n)) - S) = topspace (Euclidean_space (2 * n)) - T"
   935       proof (rule *)
   936         show "kgh ` topspace (Euclidean_space (2 * n)) = topspace (Euclidean_space (2 * n))"
   937           by (simp add: hm homeomorphic_imp_surjective_map)
   938         show "inj_on kgh (topspace (Euclidean_space (2 * n)))"
   939           using hm homeomorphic_map_def by auto
   940         show "kgh ` S = T"
   941           by (simp add: Teq kgh_def gh khf)
   942       qed (use subST topspace_Euclidean_space in \<open>fastforce+\<close>)
   943     qed auto
   944     then show ?thesis
   945       by (simp add: is_isoI mult_2)
   946   qed
   947   ultimately show ?thesis
   948     by (meson group.iso_sym iso_trans group_relative_homology_group)
   949 qed
   950 
   951 lemma lemma_iod:
   952   assumes "S \<subseteq> T" "S \<noteq> {}" and Tsub: "T \<subseteq> topspace(Euclidean_space n)"
   953       and S: "\<And>a b u. \<lbrakk>a \<in> S; b \<in> T; 0 < u; u < 1\<rbrakk> \<Longrightarrow> (\<lambda>i. (1 - u) * a i + u * b i) \<in> S"
   954     shows "path_connectedin (Euclidean_space n) T"
   955 proof -
   956   obtain a where "a \<in> S"
   957     using assms by blast
   958   have "path_component_of (subtopology (Euclidean_space n) T) a b" if "b \<in> T" for b
   959     unfolding path_component_of_def
   960   proof (intro exI conjI)
   961     have [simp]: "\<forall>i\<ge>n. a i = 0"
   962       using Tsub \<open>a \<in> S\<close> assms(1) topspace_Euclidean_space by auto
   963     have [simp]: "\<forall>i\<ge>n. b i = 0"
   964       using Tsub that topspace_Euclidean_space by auto
   965     have inT: "(\<lambda>i. (1 - x) * a i + x * b i) \<in> T" if "0 \<le> x" "x \<le> 1" for x
   966     proof (cases "x = 0 \<or> x = 1")
   967       case True
   968       with \<open>a \<in> S\<close> \<open>b \<in> T\<close> \<open>S \<subseteq> T\<close> show ?thesis
   969         by force
   970     next
   971       case False
   972       then show ?thesis
   973         using subsetD [OF \<open>S \<subseteq> T\<close> S] \<open>a \<in> S\<close> \<open>b \<in> T\<close> that by auto
   974     qed
   975     have "continuous_on {0..1} (\<lambda>x. (1 - x) * a k + x * b k)" for k
   976       by (intro continuous_intros)
   977     then show "pathin (subtopology (Euclidean_space n) T) (\<lambda>t i. (1 - t) * a i + t * b i)"
   978       apply (simp add: Euclidean_space_def subtopology_subtopology pathin_subtopology)
   979       apply (simp add: pathin_def continuous_map_componentwise_UNIV inT)
   980       done
   981   qed auto
   982   then have "path_connected_space (subtopology (Euclidean_space n) T)"
   983     by (metis Tsub path_component_of_equiv path_connected_space_iff_path_component topspace_subtopology_subset)
   984   then show ?thesis
   985     by (simp add: Tsub path_connectedin_def)
   986 qed
   987 
   988 
   989 lemma invariance_of_dimension_closedin_Euclidean_space:
   990   assumes "closedin (Euclidean_space n) S"
   991   shows "subtopology (Euclidean_space n) S homeomorphic_space Euclidean_space n
   992          \<longleftrightarrow> S = topspace(Euclidean_space n)"
   993          (is "?lhs = ?rhs")
   994 proof
   995   assume L: ?lhs
   996   have Ssub: "S \<subseteq> topspace (Euclidean_space n)"
   997     by (meson assms closedin_def)
   998   moreover have False if "a \<notin> S" and "a \<in> topspace (Euclidean_space n)" for a
   999   proof -
  1000     have cl_n: "closedin (Euclidean_space (Suc n)) (topspace(Euclidean_space n))"
  1001       using Euclidean_space_def closedin_Euclidean_space closedin_subtopology by fastforce
  1002     then have sub: "subtopology (Euclidean_space(Suc n)) (topspace(Euclidean_space n)) = Euclidean_space n"
  1003       by (metis (no_types, lifting) Euclidean_space_def closedin_subset subtopology_subtopology topspace_Euclidean_space topspace_subtopology topspace_subtopology_subset)
  1004     then have cl_S: "closedin (Euclidean_space(Suc n)) S"
  1005       using cl_n assms closedin_closed_subtopology by fastforce
  1006     have sub_SucS: "subtopology (Euclidean_space (Suc n)) S = subtopology (Euclidean_space n) S"
  1007       by (metis Ssub sub subtopology_subtopology topspace_subtopology topspace_subtopology_subset)
  1008     have non0: "{y. \<exists>x::nat\<Rightarrow>real. (\<forall>i\<ge>Suc n. x i = 0) \<and> (\<exists>i\<ge>n. x i \<noteq> 0) \<and> y = x n} = -{0}"
  1009     proof safe
  1010       show "False" if "\<forall>i\<ge>Suc n. f i = 0" "0 = f n" "n \<le> i" "f i \<noteq> 0" for f::"nat\<Rightarrow>real" and i
  1011         by (metis that le_antisym not_less_eq_eq)
  1012       show "\<exists>f::nat\<Rightarrow>real. (\<forall>i\<ge>Suc n. f i = 0) \<and> (\<exists>i\<ge>n. f i \<noteq> 0) \<and> a = f n" if "a \<noteq> 0" for a
  1013         by (rule_tac x="(\<lambda>i. 0)(n:= a)" in exI) (force simp: that)
  1014     qed
  1015     have "homology_group 0 (subtopology (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - S))
  1016           \<cong> homology_group 0 (subtopology (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n)))"
  1017     proof (rule isomorphic_relative_contractible_space_imp_homology_groups)
  1018       show "(topspace (Euclidean_space (Suc n)) - S = {}) =
  1019             (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n) = {})"
  1020         using cl_n closedin_subset that by auto
  1021     next
  1022       fix p
  1023       show "relative_homology_group p (Euclidean_space (Suc n))
  1024          (topspace (Euclidean_space (Suc n)) - S) \<cong>
  1025         relative_homology_group p (Euclidean_space (Suc n))
  1026          (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n))"
  1027         by (simp add: L sub_SucS cl_S cl_n isomorphic_relative_homology_groups_Euclidean_complements sub)
  1028     qed (auto simp: L)
  1029     moreover
  1030     have "continuous_map (powertop_real UNIV) euclideanreal (\<lambda>x. x n)"
  1031       by (metis (no_types) UNIV_I continuous_map_product_projection)
  1032     then have cm: "continuous_map (subtopology (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n)))
  1033                                   euclideanreal (\<lambda>x. x n)"
  1034       by (simp add: Euclidean_space_def continuous_map_from_subtopology)
  1035     have False if "path_connected_space
  1036                       (subtopology (Euclidean_space (Suc n))
  1037                        (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n)))"
  1038       using path_connectedin_continuous_map_image [OF cm that [unfolded path_connectedin_topspace [symmetric]]]
  1039             bounded_path_connected_Compl_real [of "{0}"]
  1040       by (simp add: topspace_Euclidean_space image_def Bex_def non0 flip: path_connectedin_topspace)
  1041     moreover
  1042     have eq: "T = T \<inter> {x. x n \<le> 0} \<union> T \<inter> {x. x n \<ge> 0}" for T :: "(nat \<Rightarrow> real) set"
  1043       by auto
  1044     have "path_connectedin (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - S)"
  1045     proof (subst eq, rule path_connectedin_Un)
  1046       have "topspace(Euclidean_space(Suc n)) \<inter> {x. x n = 0} = topspace(Euclidean_space n)"
  1047         apply (auto simp: topspace_Euclidean_space)
  1048         by (metis Suc_leI inf.absorb_iff2 inf.orderE leI)
  1049       let ?S = "topspace(Euclidean_space(Suc n)) \<inter> {x. x n < 0}"
  1050       show "path_connectedin (Euclidean_space (Suc n))
  1051               ((topspace (Euclidean_space (Suc n)) - S) \<inter> {x. x n \<le> 0})"
  1052       proof (rule lemma_iod)
  1053         show "?S \<subseteq> (topspace (Euclidean_space (Suc n)) - S) \<inter> {x. x n \<le> 0}"
  1054           using Ssub topspace_Euclidean_space by auto
  1055         show "?S \<noteq> {}"
  1056           apply (simp add: topspace_Euclidean_space set_eq_iff)
  1057           apply (rule_tac x="(\<lambda>i. 0)(n:= -1)" in exI)
  1058           apply auto
  1059           done
  1060         fix a b and u::real
  1061         assume
  1062           "a \<in> ?S" "0 < u" "u < 1"
  1063           "b \<in> (topspace (Euclidean_space (Suc n)) - S) \<inter> {x. x n \<le> 0}"
  1064         then show "(\<lambda>i. (1 - u) * a i + u * b i) \<in> ?S"
  1065           by (simp add: topspace_Euclidean_space add_neg_nonpos less_eq_real_def mult_less_0_iff)
  1066       qed (simp add: topspace_Euclidean_space subset_iff)
  1067       let ?T = "topspace(Euclidean_space(Suc n)) \<inter> {x. x n > 0}"
  1068       show "path_connectedin (Euclidean_space (Suc n))
  1069               ((topspace (Euclidean_space (Suc n)) - S) \<inter> {x. 0 \<le> x n})"
  1070       proof (rule lemma_iod)
  1071         show "?T \<subseteq> (topspace (Euclidean_space (Suc n)) - S) \<inter> {x. 0 \<le> x n}"
  1072           using Ssub topspace_Euclidean_space by auto
  1073         show "?T \<noteq> {}"
  1074           apply (simp add: topspace_Euclidean_space set_eq_iff)
  1075           apply (rule_tac x="(\<lambda>i. 0)(n:= 1)" in exI)
  1076           apply auto
  1077           done
  1078         fix a b and u::real
  1079         assume  "a \<in> ?T" "0 < u" "u < 1" "b \<in> (topspace (Euclidean_space (Suc n)) - S) \<inter> {x. 0 \<le> x n}"
  1080         then show "(\<lambda>i. (1 - u) * a i + u * b i) \<in> ?T"
  1081           by (simp add: topspace_Euclidean_space add_pos_nonneg)
  1082       qed (simp add: topspace_Euclidean_space subset_iff)
  1083       show "(topspace (Euclidean_space (Suc n)) - S) \<inter> {x. x n \<le> 0} \<inter>
  1084             ((topspace (Euclidean_space (Suc n)) - S) \<inter> {x. 0 \<le> x n}) \<noteq> {}"
  1085         using that
  1086         apply (auto simp: Set.set_eq_iff topspace_Euclidean_space)
  1087         by (metis Suc_leD order_refl)
  1088     qed
  1089     then have "path_connected_space (subtopology (Euclidean_space (Suc n))
  1090                                          (topspace (Euclidean_space (Suc n)) - S))"
  1091       apply (simp add: path_connectedin_subtopology flip: path_connectedin_topspace)
  1092       by (metis Int_Diff inf_idem)
  1093     ultimately
  1094     show ?thesis
  1095       using isomorphic_homology_imp_path_connectedness by blast
  1096   qed
  1097   ultimately show ?rhs
  1098     by blast
  1099 qed (simp add: homeomorphic_space_refl)
  1100 
  1101 
  1102 
  1103 lemma isomorphic_homology_groups_Euclidean_complements:
  1104   assumes "closedin (Euclidean_space n) S" "closedin (Euclidean_space n) T"
  1105            "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)"
  1106   shows "homology_group p (subtopology (Euclidean_space n) (topspace(Euclidean_space n) - S))
  1107          \<cong> homology_group p (subtopology (Euclidean_space n) (topspace(Euclidean_space n) - T))"
  1108 proof (rule isomorphic_relative_contractible_space_imp_homology_groups)
  1109   show "topspace (Euclidean_space n) - S \<subseteq> topspace (Euclidean_space n)"
  1110     using assms homeomorphic_space_sym invariance_of_dimension_closedin_Euclidean_space subtopology_superset by fastforce
  1111   show "topspace (Euclidean_space n) - T \<subseteq> topspace (Euclidean_space n)"
  1112     using assms invariance_of_dimension_closedin_Euclidean_space subtopology_superset by force
  1113   show "(topspace (Euclidean_space n) - S = {}) = (topspace (Euclidean_space n) - T = {})"
  1114     by (metis Diff_eq_empty_iff assms closedin_subset homeomorphic_space_sym invariance_of_dimension_closedin_Euclidean_space subset_antisym subtopology_topspace)
  1115   show "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - S) \<cong>
  1116         relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - T)" for p
  1117     using assms isomorphic_relative_homology_groups_Euclidean_complements by blast
  1118 qed auto
  1119 
  1120 lemma eqpoll_path_components_Euclidean_complements:
  1121   assumes "closedin (Euclidean_space n) S" "closedin (Euclidean_space n) T"
  1122           "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)"
  1123  shows "path_components_of
  1124              (subtopology (Euclidean_space n)
  1125                           (topspace(Euclidean_space n) - S))
  1126       \<approx> path_components_of
  1127              (subtopology (Euclidean_space n)
  1128                           (topspace(Euclidean_space n) - T))"
  1129   by (simp add: assms isomorphic_homology_groups_Euclidean_complements isomorphic_homology_imp_path_components)
  1130 
  1131 lemma path_connectedin_Euclidean_complements:
  1132   assumes "closedin (Euclidean_space n) S" "closedin (Euclidean_space n) T"
  1133           "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)"
  1134   shows "path_connectedin (Euclidean_space n) (topspace(Euclidean_space n) - S)
  1135          \<longleftrightarrow> path_connectedin (Euclidean_space n) (topspace(Euclidean_space n) - T)"
  1136   by (meson Diff_subset assms isomorphic_homology_groups_Euclidean_complements isomorphic_homology_imp_path_connectedness path_connectedin_def)
  1137 
  1138 lemma eqpoll_connected_components_Euclidean_complements:
  1139   assumes S: "closedin (Euclidean_space n) S" and T: "closedin (Euclidean_space n) T"
  1140      and ST: "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)"
  1141   shows "connected_components_of
  1142              (subtopology (Euclidean_space n)
  1143                           (topspace(Euclidean_space n) - S))
  1144         \<approx> connected_components_of
  1145              (subtopology (Euclidean_space n)
  1146                           (topspace(Euclidean_space n) - T))"
  1147   using eqpoll_path_components_Euclidean_complements [OF assms]
  1148   by (metis S T closedin_def locally_path_connected_Euclidean_space locally_path_connected_space_open_subset path_components_eq_connected_components_of)
  1149 
  1150 lemma connected_in_Euclidean_complements:
  1151   assumes "closedin (Euclidean_space n) S" "closedin (Euclidean_space n) T"
  1152           "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)"
  1153   shows "connectedin (Euclidean_space n) (topspace(Euclidean_space n) - S)
  1154      \<longleftrightarrow> connectedin (Euclidean_space n) (topspace(Euclidean_space n) - T)"
  1155   apply (simp add: connectedin_def connected_space_iff_components_subset_singleton subset_singleton_iff_lepoll)
  1156   using eqpoll_connected_components_Euclidean_complements [OF assms]
  1157   by (meson eqpoll_sym lepoll_trans1)
  1158 
  1159 
  1160 theorem invariance_of_dimension_Euclidean_space:
  1161    "Euclidean_space m homeomorphic_space Euclidean_space n \<longleftrightarrow> m = n"
  1162 proof (cases m n rule: linorder_cases)
  1163   case less
  1164   then have *: "topspace (Euclidean_space m) \<subseteq> topspace (Euclidean_space n)"
  1165     by (meson le_cases not_le subset_Euclidean_space)
  1166   then have "Euclidean_space m = subtopology (Euclidean_space n) (topspace(Euclidean_space m))"
  1167     by (simp add: Euclidean_space_def inf.absorb_iff2 subtopology_subtopology)
  1168   then show ?thesis
  1169     by (metis (no_types, lifting) * Euclidean_space_def closedin_Euclidean_space closedin_closed_subtopology eq_iff invariance_of_dimension_closedin_Euclidean_space subset_Euclidean_space topspace_Euclidean_space)
  1170 next
  1171   case equal
  1172   then show ?thesis
  1173     by (simp add: homeomorphic_space_refl)
  1174 next
  1175   case greater
  1176   then have *: "topspace (Euclidean_space n) \<subseteq> topspace (Euclidean_space m)"
  1177     by (meson le_cases not_le subset_Euclidean_space)
  1178   then have "Euclidean_space n = subtopology (Euclidean_space m) (topspace(Euclidean_space n))"
  1179     by (simp add: Euclidean_space_def inf.absorb_iff2 subtopology_subtopology)
  1180   then show ?thesis
  1181     by (metis (no_types, lifting) "*" Euclidean_space_def closedin_Euclidean_space closedin_closed_subtopology eq_iff homeomorphic_space_sym invariance_of_dimension_closedin_Euclidean_space subset_Euclidean_space topspace_Euclidean_space)
  1182 qed
  1183 
  1184 
  1185 
  1186 lemma biglemma:
  1187   assumes "n \<noteq> 0" and S: "compactin (Euclidean_space n) S"
  1188       and cmh: "continuous_map (subtopology (Euclidean_space n) S) (Euclidean_space n) h"
  1189       and "inj_on h S"
  1190     shows "path_connectedin (Euclidean_space n) (topspace(Euclidean_space n) - h ` S)
  1191        \<longleftrightarrow> path_connectedin (Euclidean_space n) (topspace(Euclidean_space n) - S)"
  1192 proof (rule path_connectedin_Euclidean_complements)
  1193   have hS_sub: "h ` S \<subseteq> topspace(Euclidean_space n)"
  1194     by (metis (no_types) S cmh compactin_subspace continuous_map_image_subset_topspace topspace_subtopology_subset)
  1195   show clo_S: "closedin (Euclidean_space n) S"
  1196     using assms by (simp add: continuous_map_in_subtopology Hausdorff_Euclidean_space compactin_imp_closedin)
  1197   show clo_hS: "closedin (Euclidean_space n) (h ` S)"
  1198     using Hausdorff_Euclidean_space S cmh compactin_absolute compactin_imp_closedin image_compactin by blast
  1199   have "homeomorphic_map (subtopology (Euclidean_space n) S) (subtopology (Euclidean_space n) (h ` S)) h"
  1200   proof (rule continuous_imp_homeomorphic_map)
  1201     show "compact_space (subtopology (Euclidean_space n) S)"
  1202       by (simp add: S compact_space_subtopology)
  1203     show "Hausdorff_space (subtopology (Euclidean_space n) (h ` S))"
  1204       using hS_sub
  1205       by (simp add: Hausdorff_Euclidean_space Hausdorff_space_subtopology)
  1206     show "continuous_map (subtopology (Euclidean_space n) S) (subtopology (Euclidean_space n) (h ` S)) h"
  1207       using cmh continuous_map_in_subtopology by fastforce
  1208     show "h ` topspace (subtopology (Euclidean_space n) S) = topspace (subtopology (Euclidean_space n) (h ` S))"
  1209       using clo_hS clo_S closedin_subset by auto
  1210     show "inj_on h (topspace (subtopology (Euclidean_space n) S))"
  1211       by (metis \<open>inj_on h S\<close> clo_S closedin_def topspace_subtopology_subset)
  1212   qed
  1213   then show "subtopology (Euclidean_space n) (h ` S) homeomorphic_space subtopology (Euclidean_space n) S"
  1214     using homeomorphic_space homeomorphic_space_sym by blast
  1215 qed
  1216 
  1217 
  1218 lemma lemmaIOD:
  1219   assumes
  1220     "\<exists>T. T \<in> U \<and> c \<subseteq> T" "\<exists>T. T \<in> U \<and> d \<subseteq> T" "\<Union>U = c \<union> d" "\<And>T. T \<in> U \<Longrightarrow> T \<noteq> {}"
  1221     "pairwise disjnt U" "~(\<exists>T. U \<subseteq> {T})"
  1222   shows "c \<in> U"
  1223   using assms
  1224   apply safe
  1225   subgoal for C' D'
  1226   proof (cases "C'=D'")
  1227     show "c \<in> U"
  1228       if UU: "\<Union> U = c \<union> d"
  1229         and U: "\<And>T. T \<in> U \<Longrightarrow> T \<noteq> {}" "disjoint U" and "\<nexists>T. U \<subseteq> {T}" "c \<subseteq> C'" "D' \<in> U" "d \<subseteq> D'" "C' = D'"
  1230     proof -
  1231       have "c \<union> d = D'"
  1232         using Union_upper sup_mono UU that(5) that(6) that(7) that(8) by auto
  1233       then have "\<Union>U = D'"
  1234         by (simp add: UU)
  1235       with U have "U = {D'}"
  1236         by (metis (no_types, lifting) disjnt_Union1 disjnt_self_iff_empty insertCI pairwiseD subset_iff that(4) that(6))
  1237       then show ?thesis
  1238         using that(4) by auto
  1239     qed
  1240     show "c \<in> U"
  1241       if "\<Union> U = c \<union> d""disjoint U" "C' \<in> U" "c \<subseteq> C'""D' \<in> U" "d \<subseteq> D'" "C' \<noteq> D'"
  1242     proof -
  1243       have "C' \<inter> D' = {}"
  1244         using \<open>disjoint U\<close> \<open>C' \<in> U\<close> \<open>D' \<in> U\<close> \<open>C' \<noteq> D'\<close>unfolding disjnt_iff pairwise_def
  1245         by blast
  1246       then show ?thesis
  1247         using subset_antisym that(1) \<open>C' \<in> U\<close> \<open>c \<subseteq> C'\<close> \<open>d \<subseteq> D'\<close> by fastforce
  1248     qed
  1249   qed
  1250   done
  1251 
  1252 
  1253 
  1254 
  1255 theorem invariance_of_domain_Euclidean_space:
  1256   assumes U: "openin (Euclidean_space n) U"
  1257     and cmf: "continuous_map (subtopology (Euclidean_space n) U) (Euclidean_space n) f"
  1258     and "inj_on f U"
  1259   shows "openin (Euclidean_space n) (f ` U)"   (is "openin ?E (f ` U)")
  1260 proof (cases "n = 0")
  1261   case True
  1262   have [simp]: "Euclidean_space 0 = discrete_topology {\<lambda>i. 0}"
  1263     by (auto simp: subtopology_eq_discrete_topology_sing topspace_Euclidean_space)
  1264   show ?thesis
  1265     using cmf True U by auto
  1266 next
  1267   case False
  1268   define enorm where "enorm \<equiv> \<lambda>x. sqrt(\<Sum>i<n. x i ^ 2)"
  1269   have enorm_if [simp]: "enorm (\<lambda>i. if i = k then d else 0) = (if k < n then \<bar>d\<bar> else 0)" for k d
  1270     using \<open>n \<noteq> 0\<close> by (auto simp:  enorm_def power2_eq_square if_distrib [of "\<lambda>x. x * _"] cong: if_cong)
  1271   define zero::"nat\<Rightarrow>real" where "zero \<equiv> \<lambda>i. 0"
  1272   have zero_in [simp]: "zero \<in> topspace ?E"
  1273     using False by (simp add: zero_def topspace_Euclidean_space)
  1274   have enorm_eq_0 [simp]: "enorm x = 0 \<longleftrightarrow> x = zero"
  1275     if "x \<in> topspace(Euclidean_space n)" for x
  1276     using that unfolding zero_def enorm_def
  1277     apply (simp add: sum_nonneg_eq_0_iff fun_eq_iff topspace_Euclidean_space)
  1278     using le_less_linear by blast
  1279   have [simp]: "enorm zero = 0"
  1280     by (simp add: zero_def enorm_def)
  1281   have cm_enorm: "continuous_map ?E euclideanreal enorm"
  1282     unfolding enorm_def
  1283   proof (intro continuous_intros)
  1284     show "continuous_map ?E euclideanreal (\<lambda>x. x i)"
  1285       if "i \<in> {..<n}" for i
  1286       using that by (auto simp: Euclidean_space_def intro: continuous_map_product_projection continuous_map_from_subtopology)
  1287   qed auto
  1288   have enorm_ge0: "0 \<le> enorm x" for x
  1289     by (auto simp: enorm_def sum_nonneg)
  1290   have le_enorm: "\<bar>x i\<bar> \<le> enorm x" if "i < n" for i x
  1291   proof -
  1292     have "\<bar>x i\<bar> \<le> sqrt (\<Sum>k\<in>{i}. (x k)\<^sup>2)"
  1293       by auto
  1294     also have "\<dots> \<le> sqrt (\<Sum>k<n. (x k)\<^sup>2)"
  1295       by (rule real_sqrt_le_mono [OF sum_mono2]) (use that in auto)
  1296     finally show ?thesis
  1297       by (simp add: enorm_def)
  1298   qed
  1299   define B where "B \<equiv> \<lambda>r. {x \<in> topspace ?E. enorm x < r}"
  1300   define C where "C \<equiv> \<lambda>r. {x \<in> topspace ?E. enorm x \<le> r}"
  1301   define S where "S \<equiv> \<lambda>r. {x \<in> topspace ?E. enorm x = r}"
  1302   have BC: "B r \<subseteq> C r" and SC: "S r \<subseteq> C r" and disjSB: "disjnt (S r) (B r)" and eqC: "B r \<union> S r = C r" for r
  1303     by (auto simp: B_def C_def S_def disjnt_def)
  1304   consider "n = 1" | "n \<ge> 2"
  1305     using False by linarith
  1306   then have **: "openin ?E (h ` (B r))"
  1307     if "r > 0" and cmh: "continuous_map(subtopology ?E (C r)) ?E h" and injh: "inj_on h (C r)" for r h
  1308   proof cases
  1309     case 1
  1310     define e :: "[real,nat]\<Rightarrow>real" where "e \<equiv> \<lambda>x i. if i = 0 then x else 0"
  1311     define e' :: "(nat\<Rightarrow>real)\<Rightarrow>real" where "e' \<equiv> \<lambda>x. x 0"
  1312     have "continuous_map euclidean euclideanreal (\<lambda>f. f (0::nat))"
  1313       by auto
  1314     then have "continuous_map (subtopology (powertop_real UNIV) {f. \<forall>n\<ge>Suc 0. f n = 0}) euclideanreal (\<lambda>f. f 0)"
  1315       by (metis (mono_tags) continuous_map_from_subtopology euclidean_product_topology)
  1316     then have hom_ee': "homeomorphic_maps euclideanreal (Euclidean_space 1) e e'"
  1317       by (auto simp: homeomorphic_maps_def e_def e'_def continuous_map_in_subtopology Euclidean_space_def)
  1318     have eBr: "e ` {-r<..<r} = B r"
  1319       unfolding B_def e_def C_def
  1320       by(force simp: "1" topspace_Euclidean_space enorm_def power2_eq_square if_distrib [of "\<lambda>x. x * _"] cong: if_cong)
  1321     have in_Cr: "\<And>x. \<lbrakk>-r < x; x < r\<rbrakk> \<Longrightarrow> (\<lambda>i. if i = 0 then x else 0) \<in> C r"
  1322       using \<open>n \<noteq> 0\<close> by (auto simp: C_def topspace_Euclidean_space)
  1323     have inj: "inj_on (e' \<circ> h \<circ> e) {- r<..<r}"
  1324     proof (clarsimp simp: inj_on_def e_def e'_def)
  1325       show "(x::real) = y"
  1326         if f: "h (\<lambda>i. if i = 0 then x else 0) 0 = h (\<lambda>i. if i = 0 then y else 0) 0"
  1327           and "-r < x" "x < r" "-r < y" "y < r"
  1328         for x y :: real
  1329       proof -
  1330         have x: "(\<lambda>i. if i = 0 then x else 0) \<in> C r" and y: "(\<lambda>i. if i = 0 then y else 0) \<in> C r"
  1331           by (blast intro: inj_onD [OF \<open>inj_on h (C r)\<close>] that in_Cr)+
  1332         have "continuous_map (subtopology (Euclidean_space (Suc 0)) (C r)) (Euclidean_space (Suc 0)) h"
  1333           using cmh by (simp add: 1)
  1334         then have "h ` ({x. \<forall>i\<ge>Suc 0. x i = 0} \<inter> C r) \<subseteq> {x. \<forall>i\<ge>Suc 0. x i = 0}"
  1335           by (force simp: Euclidean_space_def subtopology_subtopology continuous_map_def)
  1336         have "h (\<lambda>i. if i = 0 then x else 0) j = h (\<lambda>i. if i = 0 then y else 0) j" for j
  1337         proof (cases j)
  1338           case (Suc j')
  1339           have "h ` ({x. \<forall>i\<ge>Suc 0. x i = 0} \<inter> C r) \<subseteq> {x. \<forall>i\<ge>Suc 0. x i = 0}"
  1340             using continuous_map_image_subset_topspace [OF cmh]
  1341             by (simp add: 1 Euclidean_space_def subtopology_subtopology)
  1342           with Suc f x y show ?thesis
  1343             by (simp add: "1" image_subset_iff)
  1344         qed (use f in blast)
  1345         then have "(\<lambda>i. if i = 0 then x else 0) = (\<lambda>i::nat. if i = 0 then y else 0)"
  1346           by (blast intro: inj_onD [OF \<open>inj_on h (C r)\<close>] that in_Cr)
  1347         then show ?thesis
  1348           by (simp add: fun_eq_iff) presburger
  1349       qed
  1350     qed
  1351     have hom_e': "homeomorphic_map (Euclidean_space 1) euclideanreal e'"
  1352       using hom_ee' homeomorphic_maps_map by blast
  1353     have "openin (Euclidean_space n) (h ` e ` {- r<..<r})"
  1354       unfolding 1
  1355     proof (subst homeomorphic_map_openness [OF hom_e', symmetric])
  1356       show "h ` e ` {- r<..<r} \<subseteq> topspace (Euclidean_space 1)"
  1357         using "1" C_def \<open>\<And>r. B r \<subseteq> C r\<close> cmh continuous_map_image_subset_topspace eBr by fastforce
  1358       have cont: "continuous_on {- r<..<r} (e' \<circ> h \<circ> e)"
  1359       proof (intro continuous_on_compose)
  1360         have "\<And>i. continuous_on {- r<..<r} (\<lambda>x. if i = 0 then x else 0)"
  1361           by (auto simp: continuous_on_topological)
  1362         then show "continuous_on {- r<..<r} e"
  1363           by (force simp: e_def intro: continuous_on_coordinatewise_then_product)
  1364         have subCr: "e ` {- r<..<r} \<subseteq> topspace (subtopology ?E (C r))"
  1365           by (auto simp: eBr \<open>\<And>r. B r \<subseteq> C r\<close>) (auto simp: B_def)
  1366         with cmh show "continuous_on (e ` {- r<..<r}) h"
  1367           by (meson cm_Euclidean_space_iff_continuous_on continuous_on_subset)
  1368         have "h ` (e ` {- r<..<r}) \<subseteq> topspace ?E"
  1369           using subCr cmh by (simp add: continuous_map_def image_subset_iff)
  1370         moreover have "continuous_on (topspace ?E) e'"
  1371           by (metis "1" continuous_map_Euclidean_space_iff hom_ee' homeomorphic_maps_def)
  1372         ultimately show "continuous_on (h ` e ` {- r<..<r}) e'"
  1373           by (simp add: e'_def continuous_on_subset)
  1374       qed
  1375       show "openin euclideanreal (e' ` h ` e ` {- r<..<r})"
  1376         using injective_eq_1d_open_map_UNIV [OF cont] inj by (simp add: image_image is_interval_1)
  1377     qed
  1378     then show ?thesis
  1379       by (simp flip: eBr)
  1380   next
  1381     case 2
  1382     have cloC: "\<And>r. closedin (Euclidean_space n) (C r)"
  1383       unfolding C_def
  1384       by (rule closedin_continuous_map_preimage [OF cm_enorm, of concl:  "{.._}", simplified])
  1385     have cloS: "\<And>r. closedin (Euclidean_space n) (S r)"
  1386       unfolding S_def
  1387       by (rule closedin_continuous_map_preimage [OF cm_enorm, of concl:  "{_}", simplified])
  1388     have C_subset: "C r \<subseteq> UNIV \<rightarrow>\<^sub>E {- \<bar>r\<bar>..\<bar>r\<bar>}"
  1389       using le_enorm \<open>r > 0\<close>
  1390       apply (auto simp: C_def topspace_Euclidean_space abs_le_iff)
  1391        apply (metis add.inverse_neutral le_cases less_minus_iff not_le order_trans)
  1392       by (metis enorm_ge0 not_le order.trans)
  1393     have compactinC: "compactin (Euclidean_space n) (C r)"
  1394       unfolding Euclidean_space_def compactin_subtopology
  1395     proof
  1396       show "compactin (powertop_real UNIV) (C r)"
  1397       proof (rule closed_compactin [OF _ C_subset])
  1398         show "closedin (powertop_real UNIV) (C r)"
  1399           by (metis Euclidean_space_def cloC closedin_Euclidean_space closedin_closed_subtopology topspace_Euclidean_space)
  1400       qed (simp add: compactin_PiE)
  1401     qed (auto simp: C_def topspace_Euclidean_space)
  1402     have compactinS: "compactin (Euclidean_space n) (S r)"
  1403       unfolding Euclidean_space_def compactin_subtopology
  1404     proof
  1405       show "compactin (powertop_real UNIV) (S r)"
  1406       proof (rule closed_compactin)
  1407         show "S r \<subseteq> UNIV \<rightarrow>\<^sub>E {- \<bar>r\<bar>..\<bar>r\<bar>}"
  1408           using C_subset \<open>\<And>r. S r \<subseteq> C r\<close> by blast
  1409         show "closedin (powertop_real UNIV) (S r)"
  1410           by (metis Euclidean_space_def cloS closedin_Euclidean_space closedin_closed_subtopology topspace_Euclidean_space)
  1411       qed (simp add: compactin_PiE)
  1412     qed (auto simp: S_def topspace_Euclidean_space)
  1413     have h_if_B: "\<And>y. y \<in> B r \<Longrightarrow> h y \<in> topspace ?E"
  1414       using B_def \<open>\<And>r. B r \<union> S r = C r\<close> cmh continuous_map_image_subset_topspace by fastforce
  1415     have com_hSr: "compactin (Euclidean_space n) (h ` S r)"
  1416       by (meson \<open>\<And>r. S r \<subseteq> C r\<close> cmh compactinS compactin_subtopology image_compactin)
  1417     have ope_comp_hSr: "openin (Euclidean_space n) (topspace (Euclidean_space n) - h ` S r)"
  1418     proof (rule openin_diff)
  1419       show "closedin (Euclidean_space n) (h ` S r)"
  1420         using Hausdorff_Euclidean_space com_hSr compactin_imp_closedin by blast
  1421     qed auto
  1422     have h_pcs: "h ` (B r) \<in> path_components_of (subtopology ?E (topspace ?E - h ` (S r)))"
  1423     proof (rule lemmaIOD)
  1424       have pc_interval: "path_connectedin (Euclidean_space n) {x \<in> topspace(Euclidean_space n). enorm x \<in> T}"
  1425         if T: "is_interval T" for T
  1426       proof -
  1427         define mul :: "[real, nat \<Rightarrow> real, nat] \<Rightarrow> real" where "mul \<equiv> \<lambda>a x i. a * x i"
  1428         let ?neg = "mul (-1)"
  1429         have neg_neg [simp]: "?neg (?neg x) = x" for x
  1430           by (simp add: mul_def)
  1431         have enorm_mul [simp]: "enorm(mul a x) = abs a * enorm x" for a x
  1432           by (simp add: enorm_def mul_def power_mult_distrib) (metis real_sqrt_abs real_sqrt_mult sum_distrib_left)
  1433         have mul_in_top: "mul a x \<in> topspace ?E"
  1434             if "x \<in> topspace ?E" for a x
  1435           using mul_def that topspace_Euclidean_space by auto
  1436         have neg_in_S: "?neg x \<in> S r"
  1437             if "x \<in> S r" for x r
  1438           using that topspace_Euclidean_space S_def by simp (simp add: mul_def)
  1439         have *: "path_connectedin ?E (S d)"
  1440           if "d \<ge> 0" for d
  1441         proof (cases "d = 0")
  1442           let ?ES = "subtopology ?E (S d)"
  1443           case False
  1444           then have "d > 0"
  1445             using that by linarith
  1446           moreover have "path_connected_space ?ES"
  1447             unfolding path_connected_space_iff_path_component
  1448           proof clarify
  1449             have **: "path_component_of ?ES x y"
  1450               if x: "x \<in> topspace ?ES" and y: "y \<in> topspace ?ES" "x \<noteq> ?neg y" for x y
  1451             proof -
  1452               show ?thesis
  1453                 unfolding path_component_of_def pathin_def S_def
  1454               proof (intro exI conjI)
  1455                 let ?g = "(\<lambda>x. mul (d / enorm x) x) \<circ> (\<lambda>t i. (1 - t) * x i + t * y i)"
  1456                 show "continuous_map (top_of_set {0::real..1}) (subtopology ?E {x \<in> topspace ?E. enorm x = d}) ?g"
  1457                 proof (rule continuous_map_compose)
  1458                   let ?Y = "subtopology ?E (- {zero})"
  1459                   have **: False
  1460                     if eq0: "\<And>j. (1 - r) * x j + r * y j = 0"
  1461                       and ne: "x i \<noteq> - y i"
  1462                       and d: "enorm x = d" "enorm y = d"
  1463                       and r: "0 \<le> r" "r \<le> 1"
  1464                     for i r
  1465                   proof -
  1466                     have "mul (1-r) x = ?neg (mul r y)"
  1467                       using eq0 by (simp add: mul_def fun_eq_iff algebra_simps)
  1468                     then have "enorm (mul (1-r) x) = enorm (?neg (mul r y))"
  1469                       by metis
  1470                     with r have "(1-r) * enorm x = r * enorm y"
  1471                       by simp
  1472                     then have r12: "r = 1/2"
  1473                       using \<open>d \<noteq> 0\<close> d by auto
  1474                     show ?thesis
  1475                       using ne eq0 [of i] unfolding r12 by (simp add: algebra_simps)
  1476                   qed
  1477                   show "continuous_map (top_of_set {0..1}) ?Y (\<lambda>t i. (1 - t) * x i + t * y i)"
  1478                     using x y
  1479                     unfolding continuous_map_componentwise_UNIV Euclidean_space_def continuous_map_in_subtopology
  1480                     apply (intro conjI allI continuous_intros)
  1481                           apply (auto simp: zero_def mul_def S_def Euclidean_space_def fun_eq_iff)
  1482                     using ** by blast
  1483                   have cm_enorm': "continuous_map (subtopology (powertop_real UNIV) A) euclideanreal enorm" for A
  1484                     unfolding enorm_def by (intro continuous_intros) auto
  1485                   have "continuous_map ?Y (subtopology ?E {x. enorm x = d}) (\<lambda>x. mul (d / enorm x) x)"
  1486                     unfolding continuous_map_in_subtopology
  1487                   proof (intro conjI)
  1488                     show "continuous_map ?Y (Euclidean_space n) (\<lambda>x. mul (d / enorm x) x)"
  1489                       unfolding continuous_map_in_subtopology Euclidean_space_def mul_def zero_def subtopology_subtopology continuous_map_componentwise_UNIV
  1490                     proof (intro conjI allI cm_enorm' continuous_intros)
  1491                       show "enorm x \<noteq> 0"
  1492                         if "x \<in> topspace (subtopology (powertop_real UNIV) ({x. \<forall>i\<ge>n. x i = 0} \<inter> - {\<lambda>i. 0}))" for x
  1493                         using that by simp (metis abs_le_zero_iff le_enorm not_less)
  1494                     qed auto
  1495                   qed (use \<open>d > 0\<close> enorm_ge0 in auto)
  1496                   moreover have "subtopology ?E {x \<in> topspace ?E. enorm x = d} = subtopology ?E {x. enorm x = d}"
  1497                     by (simp add: subtopology_restrict Collect_conj_eq)
  1498                   ultimately show "continuous_map ?Y (subtopology (Euclidean_space n) {x \<in> topspace (Euclidean_space n). enorm x = d}) (\<lambda>x. mul (d / enorm x) x)"
  1499                     by metis
  1500                 qed
  1501                 show "?g (0::real) = x" "?g (1::real) = y"
  1502                   using that by (auto simp: S_def zero_def mul_def fun_eq_iff)
  1503               qed
  1504             qed
  1505             obtain a b where a: "a \<in> topspace ?ES" and b: "b \<in> topspace ?ES"
  1506               and "a \<noteq> b" and negab: "?neg a \<noteq> b"
  1507             proof
  1508               let ?v = "\<lambda>j i::nat. if i = j then d else 0"
  1509               show "?v 0 \<in> topspace (subtopology ?E (S d))" "?v 1 \<in> topspace (subtopology ?E (S d))"
  1510                 using \<open>n \<ge> 2\<close> \<open>d \<ge> 0\<close> by (auto simp: S_def topspace_Euclidean_space)
  1511               show "?v 0 \<noteq> ?v 1" "?neg (?v 0) \<noteq> (?v 1)"
  1512                 using \<open>d > 0\<close> by (auto simp: mul_def fun_eq_iff)
  1513             qed
  1514             show "path_component_of ?ES x y"
  1515               if x: "x \<in> topspace ?ES" and y: "y \<in> topspace ?ES"
  1516               for x y
  1517             proof -
  1518               have "path_component_of ?ES x (?neg x)"
  1519               proof -
  1520                 have "path_component_of ?ES x a"
  1521                   by (metis (no_types, hide_lams) ** a b \<open>a \<noteq> b\<close> negab path_component_of_trans path_component_of_sym x)
  1522                 moreover
  1523                 have pa_ab: "path_component_of ?ES a b" using "**" a b negab neg_neg by blast
  1524                 then have "path_component_of ?ES a (?neg x)"
  1525                   by (metis "**" \<open>a \<noteq> b\<close> cloS closedin_def neg_in_S path_component_of_equiv topspace_subtopology_subset x)
  1526                 ultimately show ?thesis
  1527                   by (meson path_component_of_trans)
  1528               qed
  1529               then show ?thesis
  1530                 using "**" x y by force
  1531             qed
  1532           qed
  1533           ultimately show ?thesis
  1534             by (simp add: cloS closedin_subset path_connectedin_def)
  1535         qed (simp add: S_def cong: conj_cong)
  1536         have "path_component_of (subtopology ?E {x \<in> topspace ?E. enorm x \<in> T}) x y"
  1537           if "enorm x = a" "x \<in> topspace ?E" "enorm x \<in> T" "enorm y = b" "y \<in> topspace ?E" "enorm y \<in> T"
  1538           for x y a b
  1539           using that
  1540           proof (induction a b arbitrary: x y rule: linorder_less_wlog)
  1541             case (less a b)
  1542             then have "a \<ge> 0"
  1543               using enorm_ge0 by blast
  1544             with less.hyps have "b > 0"
  1545               by linarith
  1546             show ?case
  1547             proof (rule path_component_of_trans)
  1548               have y'_ts: "mul (a / b) y \<in> topspace ?E"
  1549                 using \<open>y \<in> topspace ?E\<close> mul_in_top by blast
  1550               moreover have "enorm (mul (a / b) y) = a"
  1551                 unfolding enorm_mul using \<open>0 < b\<close> \<open>0 \<le> a\<close> less.prems by simp
  1552               ultimately have y'_S: "mul (a / b) y \<in> S a"
  1553                 using S_def by blast
  1554               have "x \<in> S a"
  1555                 using S_def less.prems by blast
  1556               with \<open>x \<in> topspace ?E\<close> y'_ts y'_S
  1557               have "path_component_of (subtopology ?E (S a)) x (mul (a / b) y)"
  1558                 by (metis * [OF \<open>a \<ge> 0\<close>] path_connected_space_iff_path_component path_connectedin_def topspace_subtopology_subset)
  1559               moreover
  1560               have "{f \<in> topspace ?E. enorm f = a} \<subseteq> {f \<in> topspace ?E. enorm f \<in> T}"
  1561                 using \<open>enorm x = a\<close> \<open>enorm x \<in> T\<close> by force
  1562               ultimately
  1563               show "path_component_of (subtopology ?E {x. x \<in> topspace ?E \<and> enorm x \<in> T}) x (mul (a / b) y)"
  1564                 by (simp add: S_def path_component_of_mono)
  1565               have "pathin ?E (\<lambda>t. mul (((1 - t) * b + t * a) / b) y)"
  1566                 using \<open>b > 0\<close> \<open>y \<in> topspace ?E\<close>
  1567                 unfolding pathin_def Euclidean_space_def mul_def continuous_map_in_subtopology continuous_map_componentwise_UNIV
  1568                 by (intro allI conjI continuous_intros) auto
  1569               moreover have "mul (((1 - t) * b + t * a) / b) y \<in> topspace ?E"
  1570                 if "t \<in> {0..1}" for t
  1571                 using \<open>y \<in> topspace ?E\<close> mul_in_top by blast
  1572                 moreover have "enorm (mul (((1 - t) * b + t * a) / b) y) \<in> T"
  1573                   if "t \<in> {0..1}" for t
  1574                 proof -
  1575                   have "a \<in> T" "b \<in> T"
  1576                     using less.prems by auto
  1577                   then have "\<bar>(1 - t) * b + t * a\<bar> \<in> T"
  1578                   proof (rule mem_is_interval_1_I [OF T])
  1579                     show "a \<le> \<bar>(1 - t) * b + t * a\<bar>"
  1580                       using that \<open>a \<ge> 0\<close> less.hyps segment_bound_lemma by auto
  1581                     show "\<bar>(1 - t) * b + t * a\<bar> \<le> b"
  1582                       using that \<open>a \<ge> 0\<close> less.hyps by (auto intro: convex_bound_le)
  1583                   qed
  1584                 then show ?thesis
  1585                   unfolding enorm_mul \<open>enorm y = b\<close> using that \<open>b > 0\<close> by simp
  1586               qed
  1587               ultimately have pa: "pathin (subtopology ?E {x \<in> topspace ?E. enorm x \<in> T})
  1588                                           (\<lambda>t. mul (((1 - t) * b + t * a) / b) y)"
  1589                 by (auto simp: pathin_subtopology)
  1590               have ex_pathin: "\<exists>g. pathin (subtopology ?E {x \<in> topspace ?E. enorm x \<in> T}) g \<and>
  1591                                    g 0 = y \<and> g 1 = mul (a / b) y"
  1592                 apply (rule_tac x="\<lambda>t. mul (((1 - t) * b + t * a) / b) y" in exI)
  1593                 using \<open>b > 0\<close> pa by (auto simp: mul_def)
  1594               show "path_component_of (subtopology ?E {x. x \<in> topspace ?E \<and> enorm x \<in> T}) (mul (a / b) y) y"
  1595                 by (rule path_component_of_sym) (simp add: path_component_of_def ex_pathin)
  1596             qed
  1597           next
  1598             case (refl a)
  1599             then have pc: "path_component_of (subtopology ?E (S (enorm u))) u v"
  1600               if "u \<in> topspace ?E \<inter> S (enorm x)" "v \<in> topspace ?E \<inter> S (enorm u)" for u v
  1601               using * [of a] enorm_ge0 that
  1602               by (auto simp: path_connectedin_def path_connected_space_iff_path_component S_def)
  1603             have sub: "{u \<in> topspace ?E. enorm u = enorm x} \<subseteq> {u \<in> topspace ?E. enorm u \<in> T}"
  1604               using \<open>enorm x \<in> T\<close> by auto
  1605             show ?case
  1606               using pc [of x y] refl by (auto simp: S_def path_component_of_mono [OF _ sub])
  1607           next
  1608             case (sym a b)
  1609             then show ?case
  1610               by (blast intro: path_component_of_sym)
  1611           qed
  1612         then show ?thesis
  1613           by (simp add: path_connectedin_def path_connected_space_iff_path_component)
  1614       qed
  1615       have "h ` S r \<subseteq> topspace ?E"
  1616         by (meson SC cmh compact_imp_compactin_subtopology compactinS compactin_subset_topspace image_compactin)
  1617       moreover
  1618       have "\<not> compact_space ?E "
  1619         by (metis compact_Euclidean_space \<open>n \<noteq> 0\<close>)
  1620       then have "\<not> compactin ?E (topspace ?E)"
  1621         by (simp add: compact_space_def topspace_Euclidean_space)
  1622       then have "h ` S r \<noteq> topspace ?E"
  1623         using com_hSr by auto
  1624       ultimately have top_hSr_ne: "topspace (subtopology ?E (topspace ?E - h ` S r)) \<noteq> {}"
  1625         by auto
  1626       show pc1: "\<exists>T. T \<in> path_components_of (subtopology ?E (topspace ?E - h ` S r)) \<and> h ` B r \<subseteq> T"
  1627       proof (rule exists_path_component_of_superset [OF _ top_hSr_ne])
  1628         have "path_connectedin ?E (h ` B r)"
  1629         proof (rule path_connectedin_continuous_map_image)
  1630           show "continuous_map (subtopology ?E (C r)) ?E h"
  1631             by (simp add: cmh)
  1632           have "path_connectedin ?E (B r)"
  1633             using pc_interval[of "{..<r}"] is_interval_convex_1 unfolding B_def by auto
  1634             then show "path_connectedin (subtopology ?E (C r)) (B r)"
  1635               by (simp add: path_connectedin_subtopology BC)
  1636           qed
  1637           moreover have "h ` B r \<subseteq> topspace ?E - h ` S r"
  1638             apply (auto simp: h_if_B)
  1639             by (metis BC SC disjSB disjnt_iff inj_onD [OF injh] subsetD)
  1640         ultimately show "path_connectedin (subtopology ?E (topspace ?E - h ` S r)) (h ` B r)"
  1641           by (simp add: path_connectedin_subtopology)
  1642       qed metis
  1643       show "\<exists>T. T \<in> path_components_of (subtopology ?E (topspace ?E - h ` S r)) \<and> topspace ?E - h ` (C r) \<subseteq> T"
  1644       proof (rule exists_path_component_of_superset [OF _ top_hSr_ne])
  1645         have eq: "topspace ?E - {x \<in> topspace ?E. enorm x \<le> r} = {x \<in> topspace ?E. r < enorm x}"
  1646           by auto
  1647         have "path_connectedin ?E (topspace ?E - C r)"
  1648           using pc_interval[of "{r<..}"] is_interval_convex_1 unfolding C_def eq by auto
  1649         then have "path_connectedin ?E (topspace ?E - h ` C r)"
  1650           by (metis biglemma [OF \<open>n \<noteq> 0\<close> compactinC cmh injh])
  1651         then show "path_connectedin (subtopology ?E (topspace ?E - h ` S r)) (topspace ?E - h ` C r)"
  1652           by (simp add: Diff_mono SC image_mono path_connectedin_subtopology)
  1653       qed metis
  1654       have "topspace ?E \<inter> (topspace ?E - h ` S r) = h ` B r \<union> (topspace ?E - h ` C r)"         (is "?lhs = ?rhs")
  1655       proof
  1656         show "?lhs \<subseteq> ?rhs"
  1657           using \<open>\<And>r. B r \<union> S r = C r\<close> by auto
  1658         have "h ` B r \<inter> h ` S r = {}"
  1659           by (metis Diff_triv \<open>\<And>r. B r \<union> S r = C r\<close> \<open>\<And>r. disjnt (S r) (B r)\<close> disjnt_def inf_commute inj_on_Un injh)
  1660         then show "?rhs \<subseteq> ?lhs"
  1661           using path_components_of_subset pc1 \<open>\<And>r. B r \<union> S r = C r\<close>
  1662           by (fastforce simp add: h_if_B)
  1663       qed
  1664       then show "\<Union> (path_components_of (subtopology ?E (topspace ?E - h ` S r))) = h ` B r \<union> (topspace ?E - h ` (C r))"
  1665         by (simp add: Union_path_components_of)
  1666       show "T \<noteq> {}"
  1667         if "T \<in> path_components_of (subtopology ?E (topspace ?E - h ` S r))" for T
  1668         using that by (simp add: nonempty_path_components_of)
  1669       show "disjoint (path_components_of (subtopology ?E (topspace ?E - h ` S r)))"
  1670         by (simp add: pairwise_disjoint_path_components_of)
  1671       have "\<not> path_connectedin ?E (topspace ?E - h ` S r)"
  1672       proof (subst biglemma [OF \<open>n \<noteq> 0\<close> compactinS])
  1673         show "continuous_map (subtopology ?E (S r)) ?E h"
  1674           by (metis Un_commute Un_upper1 cmh continuous_map_from_subtopology_mono eqC)
  1675         show "inj_on h (S r)"
  1676           using SC inj_on_subset injh by blast
  1677         show "\<not> path_connectedin ?E (topspace ?E - S r)"
  1678         proof
  1679           have "topspace ?E - S r = {x \<in> topspace ?E. enorm x \<noteq> r}"
  1680             by (auto simp: S_def)
  1681           moreover have "enorm ` {x \<in> topspace ?E. enorm x \<noteq> r} = {0..} - {r}"
  1682           proof
  1683             have "\<exists>x. x \<in> topspace ?E \<and> enorm x \<noteq> r \<and> d = enorm x"
  1684               if "d \<noteq> r" "d \<ge> 0" for d
  1685             proof (intro exI conjI)
  1686               show "(\<lambda>i. if i = 0 then d else 0) \<in> topspace ?E"
  1687                 using \<open>n \<noteq> 0\<close> by (auto simp: Euclidean_space_def)
  1688               show "enorm (\<lambda>i. if i = 0 then d else 0) \<noteq> r"  "d = enorm (\<lambda>i. if i = 0 then d else 0)"
  1689                 using \<open>n \<noteq> 0\<close> that by simp_all
  1690             qed
  1691             then show "{0..} - {r} \<subseteq> enorm ` {x \<in> topspace ?E. enorm x \<noteq> r}"
  1692               by (auto simp: image_def)
  1693           qed (auto simp: enorm_ge0)
  1694           ultimately have non_r: "enorm ` (topspace ?E - S r) = {0..} - {r}"
  1695             by simp
  1696           have "\<exists>x\<ge>0. x \<noteq> r \<and> r \<le> x"
  1697             by (metis gt_ex le_cases not_le order_trans)
  1698           then have "\<not> is_interval ({0..} - {r})"
  1699             unfolding is_interval_1
  1700             using  \<open>r > 0\<close> by (auto simp: Bex_def)
  1701           then show False
  1702             if "path_connectedin ?E (topspace ?E - S r)"
  1703             using path_connectedin_continuous_map_image [OF cm_enorm that] by (simp add: is_interval_path_connected_1 non_r)
  1704         qed
  1705       qed
  1706       then have "\<not> path_connected_space (subtopology ?E (topspace ?E - h ` S r))"
  1707         by (simp add: path_connectedin_def)
  1708       then show "\<nexists>T. path_components_of (subtopology ?E (topspace ?E - h ` S r)) \<subseteq> {T}"
  1709         by (simp add: path_components_of_subset_singleton)
  1710     qed
  1711     moreover have "openin ?E A"
  1712       if "A \<in> path_components_of (subtopology ?E (topspace ?E - h ` (S r)))" for A
  1713       using locally_path_connected_Euclidean_space [of n] that ope_comp_hSr
  1714       by (simp add: locally_path_connected_space_open_path_components)
  1715     ultimately show ?thesis by metis
  1716   qed
  1717   have "\<exists>T. openin ?E T \<and> f x \<in> T \<and> T \<subseteq> f ` U"
  1718     if "x \<in> U" for x
  1719   proof -
  1720     have x: "x \<in> topspace ?E"
  1721       by (meson U in_mono openin_subset that)
  1722     obtain V where V: "openin (powertop_real UNIV) V" and Ueq: "U = V \<inter> {x. \<forall>i\<ge>n. x i = 0}"
  1723       using U by (auto simp: openin_subtopology Euclidean_space_def)
  1724     with \<open>x \<in> U\<close> have "x \<in> V" by blast
  1725     then obtain T where Tfin: "finite {i. T i \<noteq> UNIV}" and Topen: "\<And>i. open (T i)"
  1726       and Tx: "x \<in> Pi\<^sub>E UNIV T" and TV: "Pi\<^sub>E UNIV T \<subseteq> V"
  1727       using V by (force simp: openin_product_topology_alt)
  1728     have "\<exists>e>0. \<forall>x'. \<bar>x' - x i\<bar> < e \<longrightarrow> x' \<in> T i" for i
  1729       using Topen [of i] Tx by (auto simp: open_real)
  1730     then obtain \<beta> where B0: "\<And>i. \<beta> i > 0" and BT: "\<And>i x'. \<bar>x' - x i\<bar> < \<beta> i \<Longrightarrow> x' \<in> T i"
  1731       by metis
  1732     define r where "r \<equiv> Min (insert 1 (\<beta> ` {i. T i \<noteq> UNIV}))"
  1733     have "r > 0"
  1734       by (simp add: B0 Tfin r_def)
  1735     have inU: "y \<in> U"
  1736       if y: "y \<in> topspace ?E" and yxr: "\<And>i. i<n \<Longrightarrow> \<bar>y i - x i\<bar> < r" for y
  1737     proof -
  1738       have "y i \<in> T i" for i
  1739       proof (cases "T i = UNIV")
  1740         show "y i \<in> T i" if "T i \<noteq> UNIV"
  1741         proof (cases "i < n")
  1742           case True
  1743           then show ?thesis
  1744             using yxr [OF True] that by (simp add: r_def BT Tfin)
  1745         next
  1746           case False
  1747           then show ?thesis
  1748             using B0 Ueq \<open>x \<in> U\<close> topspace_Euclidean_space y by (force intro: BT)
  1749         qed
  1750       qed auto
  1751       with TV have "y \<in> V" by auto
  1752       then show ?thesis
  1753         using that by (auto simp: Ueq topspace_Euclidean_space)
  1754     qed
  1755     have xinU: "(\<lambda>i. x i + y i) \<in> U" if "y \<in> C(r/2)" for y
  1756     proof (rule inU)
  1757       have y: "y \<in> topspace ?E"
  1758         using C_def that by blast
  1759       show "(\<lambda>i. x i + y i) \<in> topspace ?E"
  1760         using x y by (simp add: topspace_Euclidean_space)
  1761       have "enorm y \<le> r/2"
  1762         using that by (simp add: C_def)
  1763       then show "\<bar>x i + y i - x i\<bar> < r" if "i < n" for i
  1764         using le_enorm enorm_ge0 that \<open>0 < r\<close> leI order_trans by fastforce
  1765     qed
  1766     show ?thesis
  1767     proof (intro exI conjI)
  1768       show "openin ?E ((f \<circ> (\<lambda>y i. x i + y i)) ` B (r/2))"
  1769       proof (rule **)
  1770         have "continuous_map (subtopology ?E (C(r/2))) (subtopology ?E U) (\<lambda>y i. x i + y i)"
  1771           by (auto simp: xinU continuous_map_in_subtopology
  1772               intro!: continuous_intros continuous_map_Euclidean_space_add x)
  1773         then show "continuous_map (subtopology ?E (C(r/2))) ?E (f \<circ> (\<lambda>y i. x i + y i))"
  1774           by (rule continuous_map_compose) (simp add: cmf)
  1775         show "inj_on (f \<circ> (\<lambda>y i. x i + y i)) (C(r/2))"
  1776         proof (clarsimp simp add: inj_on_def C_def topspace_Euclidean_space simp del: divide_const_simps)
  1777           show "y' = y"
  1778             if ey: "enorm y \<le> r / 2" and ey': "enorm y' \<le> r / 2"
  1779               and y0: "\<forall>i\<ge>n. y i = 0" and y'0: "\<forall>i\<ge>n. y' i = 0"
  1780               and feq: "f (\<lambda>i. x i + y' i) = f (\<lambda>i. x i + y i)"
  1781             for y' y :: "nat \<Rightarrow> real"
  1782           proof -
  1783             have "(\<lambda>i. x i + y i) \<in> U"
  1784             proof (rule inU)
  1785               show "(\<lambda>i. x i + y i) \<in> topspace ?E"
  1786                 using topspace_Euclidean_space x y0 by auto
  1787               show "\<bar>x i + y i - x i\<bar> < r" if "i < n" for i
  1788                 using ey le_enorm [of _ y] \<open>r > 0\<close> that by fastforce
  1789             qed
  1790             moreover have "(\<lambda>i. x i + y' i) \<in> U"
  1791             proof (rule inU)
  1792               show "(\<lambda>i. x i + y' i) \<in> topspace ?E"
  1793                 using topspace_Euclidean_space x y'0 by auto
  1794               show "\<bar>x i + y' i - x i\<bar> < r" if "i < n" for i
  1795                 using ey' le_enorm [of _ y'] \<open>r > 0\<close> that by fastforce
  1796             qed
  1797             ultimately have "(\<lambda>i. x i + y' i) = (\<lambda>i. x i + y i)"
  1798               using feq by (meson \<open>inj_on f U\<close> inj_on_def)
  1799             then show ?thesis
  1800               by (auto simp: fun_eq_iff)
  1801           qed
  1802         qed
  1803       qed (simp add: \<open>0 < r\<close>)
  1804       have "x \<in> (\<lambda>y i. x i + y i) ` B (r / 2)"
  1805       proof
  1806         show "x = (\<lambda>i. x i + zero i)"
  1807           by (simp add: zero_def)
  1808       qed (auto simp: B_def \<open>r > 0\<close>)
  1809       then show "f x \<in> (f \<circ> (\<lambda>y i. x i + y i)) ` B (r/2)"
  1810         by (metis image_comp image_eqI)
  1811       show "(f \<circ> (\<lambda>y i. x i + y i)) ` B (r/2) \<subseteq> f ` U"
  1812         using \<open>\<And>r. B r \<subseteq> C r\<close> xinU by fastforce
  1813     qed
  1814   qed
  1815   then show ?thesis
  1816     using openin_subopen by force
  1817 qed
  1818 
  1819 
  1820 corollary invariance_of_domain_Euclidean_space_embedding_map:
  1821   assumes "openin (Euclidean_space n) U"
  1822     and cmf: "continuous_map(subtopology (Euclidean_space n) U) (Euclidean_space n) f"
  1823     and "inj_on f U"
  1824   shows "embedding_map(subtopology (Euclidean_space n) U) (Euclidean_space n) f"
  1825 proof (rule injective_open_imp_embedding_map [OF cmf])
  1826   show "open_map (subtopology (Euclidean_space n) U) (Euclidean_space n) f"
  1827     unfolding open_map_def
  1828     by (meson assms continuous_map_from_subtopology_mono inj_on_subset invariance_of_domain_Euclidean_space openin_imp_subset openin_trans_full)
  1829   show "inj_on f (topspace (subtopology (Euclidean_space n) U))"
  1830     using assms openin_subset topspace_subtopology_subset by fastforce
  1831 qed
  1832 
  1833 corollary invariance_of_domain_Euclidean_space_gen:
  1834   assumes "n \<le> m" and U: "openin (Euclidean_space m) U"
  1835     and cmf: "continuous_map(subtopology (Euclidean_space m) U) (Euclidean_space n) f"
  1836     and "inj_on f U"
  1837   shows "openin (Euclidean_space n) (f ` U)"
  1838 proof -
  1839   have *: "Euclidean_space n = subtopology (Euclidean_space m) (topspace(Euclidean_space n))"
  1840     by (metis Euclidean_space_def \<open>n \<le> m\<close> inf.absorb_iff2 subset_Euclidean_space subtopology_subtopology topspace_Euclidean_space)
  1841   moreover have "U \<subseteq> topspace (subtopology (Euclidean_space m) U)"
  1842     by (metis U inf.absorb_iff2 openin_subset openin_subtopology openin_topspace)
  1843   ultimately show ?thesis
  1844     by (metis (no_types) U \<open>inj_on f U\<close> cmf continuous_map_in_subtopology inf.absorb_iff2
  1845         inf.orderE invariance_of_domain_Euclidean_space openin_imp_subset openin_subtopology openin_topspace)
  1846 qed
  1847 
  1848 corollary invariance_of_domain_Euclidean_space_embedding_map_gen:
  1849   assumes "n \<le> m" and U: "openin (Euclidean_space m) U"
  1850     and cmf: "continuous_map(subtopology (Euclidean_space m) U) (Euclidean_space n) f"
  1851     and "inj_on f U"
  1852   shows "embedding_map(subtopology (Euclidean_space m) U) (Euclidean_space n) f"
  1853   proof (rule injective_open_imp_embedding_map [OF cmf])
  1854   show "open_map (subtopology (Euclidean_space m) U) (Euclidean_space n) f"
  1855     by (meson U \<open>n \<le> m\<close> \<open>inj_on f U\<close> cmf continuous_map_from_subtopology_mono invariance_of_domain_Euclidean_space_gen open_map_def openin_open_subtopology subset_inj_on)
  1856   show "inj_on f (topspace (subtopology (Euclidean_space m) U))"
  1857     using assms openin_subset topspace_subtopology_subset by fastforce
  1858 qed
  1859 
  1860 
  1861 subsection\<open>Relating two variants of Euclidean space, one within product topology.    \<close>
  1862 
  1863 proposition homeomorphic_maps_Euclidean_space_euclidean_gen_OLD:
  1864   fixes B :: "'n::euclidean_space set"
  1865   assumes "finite B" "independent B" and orth: "pairwise orthogonal B" and n: "card B = n"
  1866   obtains f g where "homeomorphic_maps (Euclidean_space n) (top_of_set (span B)) f g"
  1867 proof -
  1868   note representation_basis [OF \<open>independent B\<close>, simp]
  1869   obtain b where injb: "inj_on b {..<n}" and beq: "b ` {..<n} = B"
  1870     using finite_imp_nat_seg_image_inj_on [OF \<open>finite B\<close>]
  1871     by (metis n card_Collect_less_nat card_image lessThan_def)
  1872   then have biB: "\<And>i. i < n \<Longrightarrow> b i \<in> B"
  1873     by force
  1874   have repr: "\<And>v. v \<in> span B \<Longrightarrow> (\<Sum>i<n. representation B v (b i) *\<^sub>R b i) = v"
  1875     using real_vector.sum_representation_eq [OF \<open>independent B\<close> _ \<open>finite B\<close>]
  1876     by (metis (no_types, lifting) injb beq order_refl sum.reindex_cong)
  1877   let ?f = "\<lambda>x. \<Sum>i<n. x i *\<^sub>R b i"
  1878   let ?g = "\<lambda>v i. if i < n then representation B v (b i) else 0"
  1879   show thesis
  1880   proof
  1881     show "homeomorphic_maps (Euclidean_space n) (top_of_set (span B)) ?f ?g"
  1882       unfolding homeomorphic_maps_def
  1883     proof (intro conjI)
  1884       have *: "continuous_map euclidean (top_of_set (span B)) ?f"
  1885         by (metis (mono_tags) biB continuous_map_span_sum lessThan_iff)
  1886       show "continuous_map (Euclidean_space n) (top_of_set (span B)) ?f"
  1887         unfolding Euclidean_space_def
  1888         by (rule continuous_map_from_subtopology) (simp add: euclidean_product_topology *)
  1889       show "continuous_map (top_of_set (span B)) (Euclidean_space n) ?g"
  1890         unfolding Euclidean_space_def
  1891         by (auto simp: continuous_map_in_subtopology continuous_map_componentwise_UNIV continuous_on_representation \<open>independent B\<close> biB orth pairwise_orthogonal_imp_finite)
  1892       have [simp]: "\<And>x i. i<n \<Longrightarrow> x i *\<^sub>R b i \<in> span B"
  1893         by (simp add: biB span_base span_scale)
  1894       have "representation B (?f x) (b j) = x j"
  1895         if 0: "\<forall>i\<ge>n. x i = (0::real)" and "j < n" for x j
  1896       proof -
  1897         have "representation B (?f x) (b j) = (\<Sum>i<n. representation B (x i *\<^sub>R b i) (b j))"
  1898           by (subst real_vector.representation_sum) (auto simp add: \<open>independent B\<close>)
  1899         also have "... = (\<Sum>i<n. x i * representation B (b i) (b j))"
  1900           by (simp add: assms(2) biB representation_scale span_base)
  1901         also have "... = (\<Sum>i<n. if b j = b i then x i else 0)"
  1902           by (simp add: biB if_distrib cong: if_cong)
  1903         also have "... = x j"
  1904           using that inj_on_eq_iff [OF injb] by auto
  1905         finally show ?thesis .
  1906       qed
  1907       then show "\<forall>x\<in>topspace (Euclidean_space n). ?g (?f x) = x"
  1908         by (auto simp: Euclidean_space_def)
  1909       show "\<forall>y\<in>topspace (top_of_set (span B)). ?f (?g y) = y"
  1910         using repr by (auto simp: Euclidean_space_def)
  1911     qed
  1912   qed
  1913 qed
  1914 
  1915 proposition homeomorphic_maps_Euclidean_space_euclidean_gen:
  1916   fixes B :: "'n::euclidean_space set"
  1917   assumes "independent B" and orth: "pairwise orthogonal B" and n: "card B = n"
  1918     and 1: "\<And>u. u \<in> B \<Longrightarrow> norm u = 1"
  1919   obtains f g where "homeomorphic_maps (Euclidean_space n) (top_of_set (span B)) f g"
  1920     and "\<And>x. x \<in> topspace (Euclidean_space n) \<Longrightarrow> (norm (f x))\<^sup>2 = (\<Sum>i<n. (x i)\<^sup>2)"
  1921 proof -
  1922   note representation_basis [OF \<open>independent B\<close>, simp]
  1923   have "finite B"
  1924     using \<open>independent B\<close> finiteI_independent by metis
  1925   obtain b where injb: "inj_on b {..<n}" and beq: "b ` {..<n} = B"
  1926     using finite_imp_nat_seg_image_inj_on [OF \<open>finite B\<close>]
  1927     by (metis n card_Collect_less_nat card_image lessThan_def)
  1928   then have biB: "\<And>i. i < n \<Longrightarrow> b i \<in> B"
  1929     by force
  1930   have "0 \<notin> B"
  1931     using \<open>independent B\<close> dependent_zero by blast
  1932   have [simp]: "b i \<bullet> b j = (if j = i then 1 else 0)"
  1933     if "i < n" "j < n" for i j
  1934   proof (cases "i = j")
  1935     case True
  1936     with 1 that show ?thesis
  1937       by (auto simp: norm_eq_sqrt_inner biB)
  1938   next
  1939     case False
  1940     then have "b i \<noteq> b j"
  1941       by (meson inj_onD injb lessThan_iff that)
  1942     then show ?thesis
  1943       using orth by (auto simp: orthogonal_def pairwise_def norm_eq_sqrt_inner that biB)
  1944   qed
  1945   have [simp]: "\<And>x i. i<n \<Longrightarrow> x i *\<^sub>R b i \<in> span B"
  1946     by (simp add: biB span_base span_scale)
  1947   have repr: "\<And>v. v \<in> span B \<Longrightarrow> (\<Sum>i<n. representation B v (b i) *\<^sub>R b i) = v"
  1948     using real_vector.sum_representation_eq [OF \<open>independent B\<close> _ \<open>finite B\<close>]
  1949     by (metis (no_types, lifting) injb beq order_refl sum.reindex_cong)
  1950     define f where "f \<equiv> \<lambda>x. \<Sum>i<n. x i *\<^sub>R b i"
  1951     define g where "g \<equiv> \<lambda>v i. if i < n then representation B v (b i) else 0"
  1952   show thesis
  1953   proof
  1954     show "homeomorphic_maps (Euclidean_space n) (top_of_set (span B)) f g"
  1955       unfolding homeomorphic_maps_def
  1956     proof (intro conjI)
  1957       have *: "continuous_map euclidean (top_of_set (span B)) f"
  1958         unfolding f_def
  1959         by (rule continuous_map_span_sum) (use biB \<open>0 \<notin> B\<close> in auto)
  1960       show "continuous_map (Euclidean_space n) (top_of_set (span B)) f"
  1961         unfolding Euclidean_space_def
  1962         by (rule continuous_map_from_subtopology) (simp add: euclidean_product_topology *)
  1963       show "continuous_map (top_of_set (span B)) (Euclidean_space n) g"
  1964         unfolding Euclidean_space_def g_def
  1965         by (auto simp: continuous_map_in_subtopology continuous_map_componentwise_UNIV continuous_on_representation \<open>independent B\<close> biB orth pairwise_orthogonal_imp_finite)
  1966       have "representation B (f x) (b j) = x j"
  1967         if 0: "\<forall>i\<ge>n. x i = (0::real)" and "j < n" for x j
  1968       proof -
  1969         have "representation B (f x) (b j) = (\<Sum>i<n. representation B (x i *\<^sub>R b i) (b j))"
  1970           unfolding f_def
  1971           by (subst real_vector.representation_sum) (auto simp add: \<open>independent B\<close>)
  1972         also have "... = (\<Sum>i<n. x i * representation B (b i) (b j))"
  1973           by (simp add: \<open>independent B\<close> biB representation_scale span_base)
  1974         also have "... = (\<Sum>i<n. if b j = b i then x i else 0)"
  1975           by (simp add: biB if_distrib cong: if_cong)
  1976         also have "... = x j"
  1977           using that inj_on_eq_iff [OF injb] by auto
  1978         finally show ?thesis .
  1979       qed
  1980       then show "\<forall>x\<in>topspace (Euclidean_space n). g (f x) = x"
  1981         by (auto simp: Euclidean_space_def f_def g_def)
  1982       show "\<forall>y\<in>topspace (top_of_set (span B)). f (g y) = y"
  1983         using repr by (auto simp: Euclidean_space_def f_def g_def)
  1984     qed
  1985     show normeq: "(norm (f x))\<^sup>2 = (\<Sum>i<n. (x i)\<^sup>2)" if "x \<in> topspace (Euclidean_space n)" for x
  1986       unfolding f_def  dot_square_norm [symmetric]
  1987       by (simp add: power2_eq_square inner_sum_left inner_sum_right if_distrib biB cong: if_cong)
  1988   qed
  1989 qed
  1990 
  1991 corollary homeomorphic_maps_Euclidean_space_euclidean:
  1992   obtains f :: "(nat \<Rightarrow> real) \<Rightarrow> 'n::euclidean_space" and g
  1993   where "homeomorphic_maps (Euclidean_space (DIM('n))) euclidean f g"
  1994   by (force intro: homeomorphic_maps_Euclidean_space_euclidean_gen [OF independent_Basis orthogonal_Basis refl norm_Basis])
  1995 
  1996 lemma homeomorphic_maps_nsphere_euclidean_sphere:
  1997   fixes B :: "'n::euclidean_space set"
  1998   assumes B: "independent B" and orth: "pairwise orthogonal B" and n: "card B = n" and "n \<noteq> 0"
  1999     and 1: "\<And>u. u \<in> B \<Longrightarrow> norm u = 1"
  2000   obtains f :: "(nat \<Rightarrow> real) \<Rightarrow> 'n::euclidean_space" and g
  2001   where "homeomorphic_maps (nsphere(n - 1)) (top_of_set (sphere 0 1 \<inter> span B)) f g"
  2002 proof -
  2003   have "finite B"
  2004     using \<open>independent B\<close> finiteI_independent by metis
  2005   obtain f g where fg: "homeomorphic_maps (Euclidean_space n) (top_of_set (span B)) f g"
  2006     and normf: "\<And>x. x \<in> topspace (Euclidean_space n) \<Longrightarrow> (norm (f x))\<^sup>2 = (\<Sum>i<n. (x i)\<^sup>2)"
  2007     using homeomorphic_maps_Euclidean_space_euclidean_gen [OF B orth n 1]
  2008     by blast
  2009   obtain b where injb: "inj_on b {..<n}" and beq: "b ` {..<n} = B"
  2010     using finite_imp_nat_seg_image_inj_on [OF \<open>finite B\<close>]
  2011     by (metis n card_Collect_less_nat card_image lessThan_def)
  2012   then have biB: "\<And>i. i < n \<Longrightarrow> b i \<in> B"
  2013     by force
  2014   have [simp]: "\<And>i. i < n \<Longrightarrow> b i \<noteq> 0"
  2015     using \<open>independent B\<close> biB dependent_zero by fastforce
  2016   have [simp]: "b i \<bullet> b j = (if j = i then (norm (b i))\<^sup>2 else 0)"
  2017     if "i < n" "j < n" for i j
  2018   proof (cases "i = j")
  2019     case False
  2020     then have "b i \<noteq> b j"
  2021       by (meson inj_onD injb lessThan_iff that)
  2022     then show ?thesis
  2023       using orth by (auto simp: orthogonal_def pairwise_def norm_eq_sqrt_inner that biB)
  2024   qed (auto simp: norm_eq_sqrt_inner)
  2025   have [simp]: "Suc (n - Suc 0) = n"
  2026     using Suc_pred \<open>n \<noteq> 0\<close> by blast
  2027   then have [simp]: "{..card B - Suc 0} = {..<card B}"
  2028     using n by fastforce
  2029   show thesis
  2030   proof
  2031     have 1: "norm (f x) = 1"
  2032       if "(\<Sum>i<card B. (x i)\<^sup>2) = (1::real)" "x \<in> topspace (Euclidean_space n)" for x
  2033     proof -
  2034       have "norm (f x)^2 = 1"
  2035         using normf that by (simp add: n)
  2036       with that show ?thesis
  2037         by (simp add: power2_eq_imp_eq)
  2038     qed
  2039     have "homeomorphic_maps (nsphere (n - 1)) (top_of_set (span B \<inter> sphere 0 1)) f g"
  2040       unfolding nsphere_def subtopology_subtopology [symmetric]
  2041       proof (rule homeomorphic_maps_subtopologies_alt)
  2042   show "homeomorphic_maps (Euclidean_space (Suc (n - 1))) (top_of_set (span B)) f g"
  2043       using fg by (force simp add: )
  2044     show "f ` (topspace (Euclidean_space (Suc (n - 1))) \<inter> {x. (\<Sum>i\<le>n - 1. (x i)\<^sup>2) = 1}) \<subseteq> sphere 0 1"
  2045       using n by (auto simp: image_subset_iff Euclidean_space_def 1)
  2046     have "(\<Sum>i\<le>n - Suc 0. (g u i)\<^sup>2) = 1"
  2047       if "u \<in> span B" and "norm (u::'n) = 1" for u
  2048     proof -
  2049       obtain v where [simp]: "u = f v" "v \<in> topspace (Euclidean_space n)"
  2050         using fg unfolding homeomorphic_maps_map subset_iff
  2051         by (metis \<open>u \<in> span B\<close> homeomorphic_imp_surjective_map image_eqI topspace_euclidean_subtopology)
  2052       then have [simp]: "g (f v) = v"
  2053         by (meson fg homeomorphic_maps_map)
  2054       have fv21: "norm (f v) ^ 2 = 1"
  2055         using that by simp
  2056       show ?thesis
  2057         using that normf fv21 \<open>v \<in> topspace (Euclidean_space n)\<close> n by force
  2058     qed
  2059     then show "g ` (topspace (top_of_set (span B)) \<inter> sphere 0 1) \<subseteq> {x. (\<Sum>i\<le>n - 1. (x i)\<^sup>2) = 1}"
  2060       by auto
  2061   qed
  2062   then show "homeomorphic_maps (nsphere(n - 1)) (top_of_set (sphere 0 1 \<inter> span B)) f g"
  2063     by (simp add: inf_commute)
  2064   qed
  2065 qed
  2066 
  2067 
  2068 subsection\<open> Invariance of dimension and domain\<close>
  2069 
  2070 lemma homeomorphic_maps_iff_homeomorphism [simp]:
  2071    "homeomorphic_maps (top_of_set S) (top_of_set T) f g \<longleftrightarrow> homeomorphism S T f g"
  2072   unfolding homeomorphic_maps_def homeomorphism_def by force
  2073 
  2074 lemma homeomorphic_space_iff_homeomorphic [simp]:
  2075    "(top_of_set S) homeomorphic_space (top_of_set T) \<longleftrightarrow> S homeomorphic T"
  2076   by (simp add: homeomorphic_def homeomorphic_space_def)
  2077 
  2078 lemma homeomorphic_subspace_Euclidean_space:
  2079   fixes S :: "'a::euclidean_space set"
  2080   assumes "subspace S"
  2081   shows "top_of_set S homeomorphic_space Euclidean_space n \<longleftrightarrow> dim S = n"
  2082 proof -
  2083   obtain B where B: "B \<subseteq> S" "independent B" "span B = S" "card B = dim S"
  2084            and orth: "pairwise orthogonal B" and 1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
  2085     by (metis assms orthonormal_basis_subspace)
  2086   then have "finite B"
  2087     by (simp add: pairwise_orthogonal_imp_finite)
  2088   have "top_of_set S homeomorphic_space top_of_set (span B)"
  2089     unfolding homeomorphic_space_iff_homeomorphic
  2090     by (auto simp: assms B intro: homeomorphic_subspaces)
  2091   also have "\<dots> homeomorphic_space Euclidean_space (dim S)"
  2092     unfolding homeomorphic_space_def
  2093     using homeomorphic_maps_Euclidean_space_euclidean_gen [OF \<open>independent B\<close> orth] homeomorphic_maps_sym 1 B
  2094     by metis
  2095   finally have "top_of_set S homeomorphic_space Euclidean_space (dim S)" .
  2096   then show ?thesis
  2097     using homeomorphic_space_sym homeomorphic_space_trans invariance_of_dimension_Euclidean_space by blast
  2098 qed
  2099 
  2100 lemma homeomorphic_subspace_Euclidean_space_dim:
  2101   fixes S :: "'a::euclidean_space set"
  2102   assumes "subspace S"
  2103   shows "top_of_set S homeomorphic_space Euclidean_space (dim S)"
  2104   by (simp add: homeomorphic_subspace_Euclidean_space assms)
  2105 
  2106 lemma homeomorphic_subspaces_eq:
  2107   fixes S T:: "'a::euclidean_space set"
  2108   assumes "subspace S" "subspace T"
  2109   shows "S homeomorphic T \<longleftrightarrow> dim S = dim T"
  2110 proof
  2111   show "dim S = dim T"
  2112     if "S homeomorphic T"
  2113   proof -
  2114     have "Euclidean_space (dim S) homeomorphic_space top_of_set S"
  2115       using \<open>subspace S\<close> homeomorphic_space_sym homeomorphic_subspace_Euclidean_space_dim by blast
  2116     also have "\<dots> homeomorphic_space top_of_set T"
  2117       by (simp add: that)
  2118     also have "\<dots> homeomorphic_space Euclidean_space (dim T)"
  2119       by (simp add: homeomorphic_subspace_Euclidean_space assms)
  2120     finally have "Euclidean_space (dim S) homeomorphic_space Euclidean_space (dim T)" .
  2121     then show ?thesis
  2122       by (simp add: invariance_of_dimension_Euclidean_space)
  2123   qed
  2124 next
  2125   show "S homeomorphic T"
  2126     if "dim S = dim T"
  2127     by (metis that assms homeomorphic_subspaces)
  2128 qed
  2129 
  2130 lemma homeomorphic_affine_Euclidean_space:
  2131   assumes "affine S"
  2132   shows "top_of_set S homeomorphic_space Euclidean_space n \<longleftrightarrow> aff_dim S = n"
  2133    (is "?X homeomorphic_space ?E \<longleftrightarrow> aff_dim S = n")
  2134 proof (cases "S = {}")
  2135   case True
  2136   with assms show ?thesis
  2137     using homeomorphic_empty_space nonempty_Euclidean_space by fastforce
  2138 next
  2139   case False
  2140   then obtain a where "a \<in> S"
  2141     by force
  2142   have "(?X homeomorphic_space ?E)
  2143        = (top_of_set (image (\<lambda>x. -a + x) S) homeomorphic_space ?E)"
  2144   proof
  2145     show "top_of_set ((+) (- a) ` S) homeomorphic_space ?E"
  2146       if "?X homeomorphic_space ?E"
  2147       using that
  2148       by (meson homeomorphic_space_iff_homeomorphic homeomorphic_space_sym homeomorphic_space_trans homeomorphic_translation)
  2149     show "?X homeomorphic_space ?E"
  2150       if "top_of_set ((+) (- a) ` S) homeomorphic_space ?E"
  2151       using that
  2152       by (meson homeomorphic_space_iff_homeomorphic homeomorphic_space_trans homeomorphic_translation)
  2153   qed
  2154   also have "\<dots> \<longleftrightarrow> aff_dim S = n"
  2155     by (metis \<open>a \<in> S\<close> aff_dim_eq_dim affine_diffs_subspace affine_hull_eq assms homeomorphic_subspace_Euclidean_space of_nat_eq_iff)
  2156   finally show ?thesis .
  2157 qed
  2158 
  2159 
  2160 corollary invariance_of_domain_subspaces:
  2161   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  2162   assumes ope: "openin (top_of_set U) S"
  2163       and "subspace U" "subspace V" and VU: "dim V \<le> dim U"
  2164       and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
  2165       and injf: "inj_on f S"
  2166     shows "openin (top_of_set V) (f ` S)"
  2167 proof -
  2168   have "S \<subseteq> U"
  2169     using openin_imp_subset [OF ope] .
  2170   have Uhom: "top_of_set U homeomorphic_space Euclidean_space (dim U)"
  2171    and Vhom: "top_of_set V homeomorphic_space Euclidean_space (dim V)"
  2172     by (simp_all add: assms homeomorphic_subspace_Euclidean_space_dim)
  2173   then obtain \<phi> \<phi>' where hom: "homeomorphic_maps (top_of_set U) (Euclidean_space (dim U)) \<phi> \<phi>'"
  2174     by (auto simp: homeomorphic_space_def)
  2175   obtain \<psi> \<psi>' where \<psi>: "homeomorphic_map (top_of_set V) (Euclidean_space (dim V)) \<psi>"
  2176               and \<psi>'\<psi>: "\<forall>x\<in>V. \<psi>' (\<psi> x) = x"
  2177     using Vhom by (auto simp: homeomorphic_space_def homeomorphic_maps_map)
  2178   have "((\<psi> \<circ> f \<circ> \<phi>') o \<phi>) ` S = (\<psi> o f) ` S"
  2179   proof (rule image_cong [OF refl])
  2180     show "(\<psi> \<circ> f \<circ> \<phi>' \<circ> \<phi>) x = (\<psi> \<circ> f) x" if "x \<in> S" for x
  2181       using that unfolding o_def
  2182       by (metis \<open>S \<subseteq> U\<close> hom homeomorphic_maps_map in_mono topspace_euclidean_subtopology)
  2183   qed
  2184   moreover
  2185   have "openin (Euclidean_space (dim V)) ((\<psi> \<circ> f \<circ> \<phi>') ` \<phi> ` S)"
  2186   proof (rule invariance_of_domain_Euclidean_space_gen [OF VU])
  2187     show "openin (Euclidean_space (dim U)) (\<phi> ` S)"
  2188       using homeomorphic_map_openness_eq hom homeomorphic_maps_map ope by blast
  2189     show "continuous_map (subtopology (Euclidean_space (dim U)) (\<phi> ` S)) (Euclidean_space (dim V)) (\<psi> \<circ> f \<circ> \<phi>')"
  2190     proof (intro continuous_map_compose)
  2191       have "continuous_on ({x. \<forall>i\<ge>dim U. x i = 0} \<inter> \<phi> ` S) \<phi>'"
  2192         if "continuous_on {x. \<forall>i\<ge>dim U. x i = 0} \<phi>'"
  2193         using that by (force elim: continuous_on_subset)
  2194       moreover have "\<phi>' ` ({x. \<forall>i\<ge>dim U. x i = 0} \<inter> \<phi> ` S) \<subseteq> S"
  2195         if "\<forall>x\<in>U. \<phi>' (\<phi> x) = x"
  2196         using that \<open>S \<subseteq> U\<close> by fastforce
  2197       ultimately show "continuous_map (subtopology (Euclidean_space (dim U)) (\<phi> ` S)) (top_of_set S) \<phi>'"
  2198         using hom unfolding homeomorphic_maps_def
  2199         by (simp add:  Euclidean_space_def subtopology_subtopology euclidean_product_topology)
  2200       show "continuous_map (top_of_set S) (top_of_set V) f"
  2201         by (simp add: contf fim)
  2202       show "continuous_map (top_of_set V) (Euclidean_space (dim V)) \<psi>"
  2203         by (simp add: \<psi> homeomorphic_imp_continuous_map)
  2204     qed
  2205     show "inj_on (\<psi> \<circ> f \<circ> \<phi>') (\<phi> ` S)"
  2206       using injf hom
  2207       unfolding inj_on_def homeomorphic_maps_map
  2208       by simp (metis \<open>S \<subseteq> U\<close> \<psi>'\<psi> fim imageI subsetD)
  2209   qed
  2210   ultimately have "openin (Euclidean_space (dim V)) (\<psi> ` f ` S)"
  2211     by (simp add: image_comp)
  2212   then show ?thesis
  2213     by (simp add: fim homeomorphic_map_openness_eq [OF \<psi>])
  2214 qed
  2215 
  2216 lemma invariance_of_domain:
  2217   fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
  2218   assumes "continuous_on S f" "open S" "inj_on f S" shows "open(f ` S)"
  2219   using invariance_of_domain_subspaces [of UNIV S UNIV] assms by (force simp add: )
  2220 
  2221 corollary invariance_of_dimension_subspaces:
  2222   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  2223   assumes ope: "openin (top_of_set U) S"
  2224       and "subspace U" "subspace V"
  2225       and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
  2226       and injf: "inj_on f S" and "S \<noteq> {}"
  2227     shows "dim U \<le> dim V"
  2228 proof -
  2229   have "False" if "dim V < dim U"
  2230   proof -
  2231     obtain T where "subspace T" "T \<subseteq> U" "dim T = dim V"
  2232       using choose_subspace_of_subspace [of "dim V" U]
  2233       by (metis \<open>dim V < dim U\<close> assms(2) order.strict_implies_order span_eq_iff)
  2234     then have "V homeomorphic T"
  2235       by (simp add: \<open>subspace V\<close> homeomorphic_subspaces)
  2236     then obtain h k where homhk: "homeomorphism V T h k"
  2237       using homeomorphic_def  by blast
  2238     have "continuous_on S (h \<circ> f)"
  2239       by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_cont1 homhk)
  2240     moreover have "(h \<circ> f) ` S \<subseteq> U"
  2241       using \<open>T \<subseteq> U\<close> fim homeomorphism_image1 homhk by fastforce
  2242     moreover have "inj_on (h \<circ> f) S"
  2243       apply (clarsimp simp: inj_on_def)
  2244       by (metis fim homeomorphism_apply1 homhk image_subset_iff inj_onD injf)
  2245     ultimately have ope_hf: "openin (top_of_set U) ((h \<circ> f) ` S)"
  2246       using invariance_of_domain_subspaces [OF ope \<open>subspace U\<close> \<open>subspace U\<close>] by blast
  2247     have "(h \<circ> f) ` S \<subseteq> T"
  2248       using fim homeomorphism_image1 homhk by fastforce
  2249     then have "dim ((h \<circ> f) ` S) \<le> dim T"
  2250       by (rule dim_subset)
  2251     also have "dim ((h \<circ> f) ` S) = dim U"
  2252       using \<open>S \<noteq> {}\<close> \<open>subspace U\<close>
  2253       by (blast intro: dim_openin ope_hf)
  2254     finally show False
  2255       using \<open>dim V < dim U\<close> \<open>dim T = dim V\<close> by simp
  2256   qed
  2257   then show ?thesis
  2258     using not_less by blast
  2259 qed
  2260 
  2261 corollary invariance_of_domain_affine_sets:
  2262   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  2263   assumes ope: "openin (top_of_set U) S"
  2264       and aff: "affine U" "affine V" "aff_dim V \<le> aff_dim U"
  2265       and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
  2266       and injf: "inj_on f S"
  2267     shows "openin (top_of_set V) (f ` S)"
  2268 proof (cases "S = {}")
  2269   case False
  2270   obtain a b where "a \<in> S" "a \<in> U" "b \<in> V"
  2271     using False fim ope openin_contains_cball by fastforce
  2272   have "openin (top_of_set ((+) (- b) ` V)) (((+) (- b) \<circ> f \<circ> (+) a) ` (+) (- a) ` S)"
  2273   proof (rule invariance_of_domain_subspaces)
  2274     show "openin (top_of_set ((+) (- a) ` U)) ((+) (- a) ` S)"
  2275       by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois)
  2276     show "subspace ((+) (- a) ` U)"
  2277       by (simp add: \<open>a \<in> U\<close> affine_diffs_subspace_subtract \<open>affine U\<close> cong: image_cong_simp)
  2278     show "subspace ((+) (- b) ` V)"
  2279       by (simp add: \<open>b \<in> V\<close> affine_diffs_subspace_subtract \<open>affine V\<close> cong: image_cong_simp)
  2280     show "dim ((+) (- b) ` V) \<le> dim ((+) (- a) ` U)"
  2281       by (metis \<open>a \<in> U\<close> \<open>b \<in> V\<close> aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
  2282     show "continuous_on ((+) (- a) ` S) ((+) (- b) \<circ> f \<circ> (+) a)"
  2283       by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
  2284     show "((+) (- b) \<circ> f \<circ> (+) a) ` (+) (- a) ` S \<subseteq> (+) (- b) ` V"
  2285       using fim by auto
  2286     show "inj_on ((+) (- b) \<circ> f \<circ> (+) a) ((+) (- a) ` S)"
  2287       by (auto simp: inj_on_def) (meson inj_onD injf)
  2288   qed
  2289   then show ?thesis
  2290     by (metis (no_types, lifting) homeomorphism_imp_open_map homeomorphism_translation image_comp translation_galois)
  2291 qed auto
  2292 
  2293 corollary invariance_of_dimension_affine_sets:
  2294   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  2295   assumes ope: "openin (top_of_set U) S"
  2296       and aff: "affine U" "affine V"
  2297       and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
  2298       and injf: "inj_on f S" and "S \<noteq> {}"
  2299     shows "aff_dim U \<le> aff_dim V"
  2300 proof -
  2301   obtain a b where "a \<in> S" "a \<in> U" "b \<in> V"
  2302     using \<open>S \<noteq> {}\<close> fim ope openin_contains_cball by fastforce
  2303   have "dim ((+) (- a) ` U) \<le> dim ((+) (- b) ` V)"
  2304   proof (rule invariance_of_dimension_subspaces)
  2305     show "openin (top_of_set ((+) (- a) ` U)) ((+) (- a) ` S)"
  2306       by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois)
  2307     show "subspace ((+) (- a) ` U)"
  2308       by (simp add: \<open>a \<in> U\<close> affine_diffs_subspace_subtract \<open>affine U\<close> cong: image_cong_simp)
  2309     show "subspace ((+) (- b) ` V)"
  2310       by (simp add: \<open>b \<in> V\<close> affine_diffs_subspace_subtract \<open>affine V\<close> cong: image_cong_simp)
  2311     show "continuous_on ((+) (- a) ` S) ((+) (- b) \<circ> f \<circ> (+) a)"
  2312       by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
  2313     show "((+) (- b) \<circ> f \<circ> (+) a) ` (+) (- a) ` S \<subseteq> (+) (- b) ` V"
  2314       using fim by auto
  2315     show "inj_on ((+) (- b) \<circ> f \<circ> (+) a) ((+) (- a) ` S)"
  2316       by (auto simp: inj_on_def) (meson inj_onD injf)
  2317   qed (use \<open>S \<noteq> {}\<close> in auto)
  2318   then show ?thesis
  2319     by (metis \<open>a \<in> U\<close> \<open>b \<in> V\<close> aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
  2320 qed
  2321 
  2322 corollary invariance_of_dimension:
  2323   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  2324   assumes contf: "continuous_on S f" and "open S"
  2325       and injf: "inj_on f S" and "S \<noteq> {}"
  2326     shows "DIM('a) \<le> DIM('b)"
  2327   using%unimportant invariance_of_dimension_subspaces [of UNIV S UNIV f] assms
  2328   by auto
  2329 
  2330 corollary continuous_injective_image_subspace_dim_le:
  2331   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  2332   assumes "subspace S" "subspace T"
  2333       and contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
  2334       and injf: "inj_on f S"
  2335     shows "dim S \<le> dim T"
  2336   apply (rule invariance_of_dimension_subspaces [of S S _ f])
  2337   using%unimportant assms by (auto simp: subspace_affine)
  2338 
  2339 lemma invariance_of_dimension_convex_domain:
  2340   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  2341   assumes "convex S"
  2342       and contf: "continuous_on S f" and fim: "f ` S \<subseteq> affine hull T"
  2343       and injf: "inj_on f S"
  2344     shows "aff_dim S \<le> aff_dim T"
  2345 proof (cases "S = {}")
  2346   case True
  2347   then show ?thesis by (simp add: aff_dim_geq)
  2348 next
  2349   case False
  2350   have "aff_dim (affine hull S) \<le> aff_dim (affine hull T)"
  2351   proof (rule invariance_of_dimension_affine_sets)
  2352     show "openin (top_of_set (affine hull S)) (rel_interior S)"
  2353       by (simp add: openin_rel_interior)
  2354     show "continuous_on (rel_interior S) f"
  2355       using contf continuous_on_subset rel_interior_subset by blast
  2356     show "f ` rel_interior S \<subseteq> affine hull T"
  2357       using fim rel_interior_subset by blast
  2358     show "inj_on f (rel_interior S)"
  2359       using inj_on_subset injf rel_interior_subset by blast
  2360     show "rel_interior S \<noteq> {}"
  2361       by (simp add: False \<open>convex S\<close> rel_interior_eq_empty)
  2362   qed auto
  2363   then show ?thesis
  2364     by simp
  2365 qed
  2366 
  2367 lemma homeomorphic_convex_sets_le:
  2368   assumes "convex S" "S homeomorphic T"
  2369   shows "aff_dim S \<le> aff_dim T"
  2370 proof -
  2371   obtain h k where homhk: "homeomorphism S T h k"
  2372     using homeomorphic_def assms  by blast
  2373   show ?thesis
  2374   proof (rule invariance_of_dimension_convex_domain [OF \<open>convex S\<close>])
  2375     show "continuous_on S h"
  2376       using homeomorphism_def homhk by blast
  2377     show "h ` S \<subseteq> affine hull T"
  2378       by (metis homeomorphism_def homhk hull_subset)
  2379     show "inj_on h S"
  2380       by (meson homeomorphism_apply1 homhk inj_on_inverseI)
  2381   qed
  2382 qed
  2383 
  2384 lemma homeomorphic_convex_sets:
  2385   assumes "convex S" "convex T" "S homeomorphic T"
  2386   shows "aff_dim S = aff_dim T"
  2387   by (meson assms dual_order.antisym homeomorphic_convex_sets_le homeomorphic_sym)
  2388 
  2389 lemma homeomorphic_convex_compact_sets_eq:
  2390   assumes "convex S" "compact S" "convex T" "compact T"
  2391   shows "S homeomorphic T \<longleftrightarrow> aff_dim S = aff_dim T"
  2392   by (meson assms homeomorphic_convex_compact_sets homeomorphic_convex_sets)
  2393 
  2394 lemma invariance_of_domain_gen:
  2395   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  2396   assumes "open S" "continuous_on S f" "inj_on f S" "DIM('b) \<le> DIM('a)"
  2397     shows "open(f ` S)"
  2398   using invariance_of_domain_subspaces [of UNIV S UNIV f] assms by auto
  2399 
  2400 lemma injective_into_1d_imp_open_map_UNIV:
  2401   fixes f :: "'a::euclidean_space \<Rightarrow> real"
  2402   assumes "open T" "continuous_on S f" "inj_on f S" "T \<subseteq> S"
  2403     shows "open (f ` T)"
  2404   apply (rule invariance_of_domain_gen [OF \<open>open T\<close>])
  2405   using assms apply (auto simp: elim: continuous_on_subset subset_inj_on)
  2406   done
  2407 
  2408 lemma continuous_on_inverse_open:
  2409   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  2410   assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" and gf: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
  2411     shows "continuous_on (f ` S) g"
  2412 proof (clarsimp simp add: continuous_openin_preimage_eq)
  2413   fix T :: "'a set"
  2414   assume "open T"
  2415   have eq: "f ` S \<inter> g -` T = f ` (S \<inter> T)"
  2416     by (auto simp: gf)
  2417   have "openin (top_of_set (f ` S)) (f ` (S \<inter> T))"
  2418   proof (rule open_openin_trans [OF invariance_of_domain_gen])
  2419     show "inj_on f S"
  2420       using inj_on_inverseI gf by auto
  2421     show "open (f ` (S \<inter> T))"
  2422       by (meson \<open>inj_on f S\<close> \<open>open T\<close> assms(1-3) continuous_on_subset inf_le1 inj_on_subset invariance_of_domain_gen open_Int)
  2423   qed (use assms in auto)
  2424   then show "openin (top_of_set (f ` S)) (f ` S \<inter> g -` T)"
  2425     by (simp add: eq)
  2426 qed
  2427 
  2428 lemma invariance_of_domain_homeomorphism:
  2429   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  2430   assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" "inj_on f S"
  2431   obtains g where "homeomorphism S (f ` S) f g"
  2432 proof
  2433   show "homeomorphism S (f ` S) f (inv_into S f)"
  2434     by (simp add: assms continuous_on_inverse_open homeomorphism_def)
  2435 qed
  2436 
  2437 corollary invariance_of_domain_homeomorphic:
  2438   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  2439   assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" "inj_on f S"
  2440   shows "S homeomorphic (f ` S)"
  2441   using%unimportant invariance_of_domain_homeomorphism [OF assms]
  2442   by%unimportant (meson homeomorphic_def)
  2443 
  2444 lemma continuous_image_subset_interior:
  2445   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  2446   assumes "continuous_on S f" "inj_on f S" "DIM('b) \<le> DIM('a)"
  2447   shows "f ` (interior S) \<subseteq> interior(f ` S)"
  2448 proof (rule interior_maximal)
  2449   show "f ` interior S \<subseteq> f ` S"
  2450     by (simp add: image_mono interior_subset)
  2451   show "open (f ` interior S)"
  2452     using assms
  2453     by (auto simp: subset_inj_on interior_subset continuous_on_subset invariance_of_domain_gen)
  2454 qed
  2455 
  2456 lemma homeomorphic_interiors_same_dimension:
  2457   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  2458   assumes "S homeomorphic T" and dimeq: "DIM('a) = DIM('b)"
  2459   shows "(interior S) homeomorphic (interior T)"
  2460   using assms [unfolded homeomorphic_minimal]
  2461   unfolding homeomorphic_def
  2462 proof (clarify elim!: ex_forward)
  2463   fix f g
  2464   assume S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
  2465      and contf: "continuous_on S f" and contg: "continuous_on T g"
  2466   then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
  2467     by (auto simp: inj_on_def intro: rev_image_eqI) metis+
  2468   have fim: "f ` interior S \<subseteq> interior T"
  2469     using continuous_image_subset_interior [OF contf \<open>inj_on f S\<close>] dimeq fST by simp
  2470   have gim: "g ` interior T \<subseteq> interior S"
  2471     using continuous_image_subset_interior [OF contg \<open>inj_on g T\<close>] dimeq gTS by simp
  2472   show "homeomorphism (interior S) (interior T) f g"
  2473     unfolding homeomorphism_def
  2474   proof (intro conjI ballI)
  2475     show "\<And>x. x \<in> interior S \<Longrightarrow> g (f x) = x"
  2476       by (meson \<open>\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x\<close> subsetD interior_subset)
  2477     have "interior T \<subseteq> f ` interior S"
  2478     proof
  2479       fix x assume "x \<in> interior T"
  2480       then have "g x \<in> interior S"
  2481         using gim by blast
  2482       then show "x \<in> f ` interior S"
  2483         by (metis T \<open>x \<in> interior T\<close> image_iff interior_subset subsetCE)
  2484     qed
  2485     then show "f ` interior S = interior T"
  2486       using fim by blast
  2487     show "continuous_on (interior S) f"
  2488       by (metis interior_subset continuous_on_subset contf)
  2489     show "\<And>y. y \<in> interior T \<Longrightarrow> f (g y) = y"
  2490       by (meson T subsetD interior_subset)
  2491     have "interior S \<subseteq> g ` interior T"
  2492     proof
  2493       fix x assume "x \<in> interior S"
  2494       then have "f x \<in> interior T"
  2495         using fim by blast
  2496       then show "x \<in> g ` interior T"
  2497         by (metis S \<open>x \<in> interior S\<close> image_iff interior_subset subsetCE)
  2498     qed
  2499     then show "g ` interior T = interior S"
  2500       using gim by blast
  2501     show "continuous_on (interior T) g"
  2502       by (metis interior_subset continuous_on_subset contg)
  2503   qed
  2504 qed
  2505 
  2506 lemma homeomorphic_open_imp_same_dimension:
  2507   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  2508   assumes "S homeomorphic T" "open S" "S \<noteq> {}" "open T" "T \<noteq> {}"
  2509   shows "DIM('a) = DIM('b)"
  2510     using assms
  2511     apply (simp add: homeomorphic_minimal)
  2512     apply (rule order_antisym; metis inj_onI invariance_of_dimension)
  2513     done
  2514 
  2515 proposition homeomorphic_interiors:
  2516   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  2517   assumes "S homeomorphic T" "interior S = {} \<longleftrightarrow> interior T = {}"
  2518     shows "(interior S) homeomorphic (interior T)"
  2519 proof (cases "interior T = {}")
  2520   case True
  2521   with assms show ?thesis by auto
  2522 next
  2523   case False
  2524   then have "DIM('a) = DIM('b)"
  2525     using assms
  2526     apply (simp add: homeomorphic_minimal)
  2527     apply (rule order_antisym; metis continuous_on_subset inj_onI inj_on_subset interior_subset invariance_of_dimension open_interior)
  2528     done
  2529   then show ?thesis
  2530     by (rule homeomorphic_interiors_same_dimension [OF \<open>S homeomorphic T\<close>])
  2531 qed
  2532 
  2533 lemma homeomorphic_frontiers_same_dimension:
  2534   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  2535   assumes "S homeomorphic T" "closed S" "closed T" and dimeq: "DIM('a) = DIM('b)"
  2536   shows "(frontier S) homeomorphic (frontier T)"
  2537   using assms [unfolded homeomorphic_minimal]
  2538   unfolding homeomorphic_def
  2539 proof (clarify elim!: ex_forward)
  2540   fix f g
  2541   assume S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
  2542      and contf: "continuous_on S f" and contg: "continuous_on T g"
  2543   then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
  2544     by (auto simp: inj_on_def intro: rev_image_eqI) metis+
  2545   have "g ` interior T \<subseteq> interior S"
  2546     using continuous_image_subset_interior [OF contg \<open>inj_on g T\<close>] dimeq gTS by simp
  2547   then have fim: "f ` frontier S \<subseteq> frontier T"
  2548     apply (simp add: frontier_def)
  2549     using continuous_image_subset_interior assms(2) assms(3) S by auto
  2550   have "f ` interior S \<subseteq> interior T"
  2551     using continuous_image_subset_interior [OF contf \<open>inj_on f S\<close>] dimeq fST by simp
  2552   then have gim: "g ` frontier T \<subseteq> frontier S"
  2553     apply (simp add: frontier_def)
  2554     using continuous_image_subset_interior T assms(2) assms(3) by auto
  2555   show "homeomorphism (frontier S) (frontier T) f g"
  2556     unfolding homeomorphism_def
  2557   proof (intro conjI ballI)
  2558     show gf: "\<And>x. x \<in> frontier S \<Longrightarrow> g (f x) = x"
  2559       by (simp add: S assms(2) frontier_def)
  2560     show fg: "\<And>y. y \<in> frontier T \<Longrightarrow> f (g y) = y"
  2561       by (simp add: T assms(3) frontier_def)
  2562     have "frontier T \<subseteq> f ` frontier S"
  2563     proof
  2564       fix x assume "x \<in> frontier T"
  2565       then have "g x \<in> frontier S"
  2566         using gim by blast
  2567       then show "x \<in> f ` frontier S"
  2568         by (metis fg \<open>x \<in> frontier T\<close> imageI)
  2569     qed
  2570     then show "f ` frontier S = frontier T"
  2571       using fim by blast
  2572     show "continuous_on (frontier S) f"
  2573       by (metis Diff_subset assms(2) closure_eq contf continuous_on_subset frontier_def)
  2574     have "frontier S \<subseteq> g ` frontier T"
  2575     proof
  2576       fix x assume "x \<in> frontier S"
  2577       then have "f x \<in> frontier T"
  2578         using fim by blast
  2579       then show "x \<in> g ` frontier T"
  2580         by (metis gf \<open>x \<in> frontier S\<close> imageI)
  2581     qed
  2582     then show "g ` frontier T = frontier S"
  2583       using gim by blast
  2584     show "continuous_on (frontier T) g"
  2585       by (metis Diff_subset assms(3) closure_closed contg continuous_on_subset frontier_def)
  2586   qed
  2587 qed
  2588 
  2589 lemma homeomorphic_frontiers:
  2590   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  2591   assumes "S homeomorphic T" "closed S" "closed T"
  2592           "interior S = {} \<longleftrightarrow> interior T = {}"
  2593     shows "(frontier S) homeomorphic (frontier T)"
  2594 proof (cases "interior T = {}")
  2595   case True
  2596   then show ?thesis
  2597     by (metis Diff_empty assms closure_eq frontier_def)
  2598 next
  2599   case False
  2600   show ?thesis
  2601     apply (rule homeomorphic_frontiers_same_dimension)
  2602        apply (simp_all add: assms)
  2603     using False assms homeomorphic_interiors homeomorphic_open_imp_same_dimension by blast
  2604 qed
  2605 
  2606 lemma continuous_image_subset_rel_interior:
  2607   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  2608   assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
  2609       and TS: "aff_dim T \<le> aff_dim S"
  2610   shows "f ` (rel_interior S) \<subseteq> rel_interior(f ` S)"
  2611 proof (rule rel_interior_maximal)
  2612   show "f ` rel_interior S \<subseteq> f ` S"
  2613     by(simp add: image_mono rel_interior_subset)
  2614   show "openin (top_of_set (affine hull f ` S)) (f ` rel_interior S)"
  2615   proof (rule invariance_of_domain_affine_sets)
  2616     show "openin (top_of_set (affine hull S)) (rel_interior S)"
  2617       by (simp add: openin_rel_interior)
  2618     show "aff_dim (affine hull f ` S) \<le> aff_dim (affine hull S)"
  2619       by (metis aff_dim_affine_hull aff_dim_subset fim TS order_trans)
  2620     show "f ` rel_interior S \<subseteq> affine hull f ` S"
  2621       by (meson \<open>f ` rel_interior S \<subseteq> f ` S\<close> hull_subset order_trans)
  2622     show "continuous_on (rel_interior S) f"
  2623       using contf continuous_on_subset rel_interior_subset by blast
  2624     show "inj_on f (rel_interior S)"
  2625       using inj_on_subset injf rel_interior_subset by blast
  2626   qed auto
  2627 qed
  2628 
  2629 lemma homeomorphic_rel_interiors_same_dimension:
  2630   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  2631   assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T"
  2632   shows "(rel_interior S) homeomorphic (rel_interior T)"
  2633   using assms [unfolded homeomorphic_minimal]
  2634   unfolding homeomorphic_def
  2635 proof (clarify elim!: ex_forward)
  2636   fix f g
  2637   assume S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
  2638      and contf: "continuous_on S f" and contg: "continuous_on T g"
  2639   then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
  2640     by (auto simp: inj_on_def intro: rev_image_eqI) metis+
  2641   have fim: "f ` rel_interior S \<subseteq> rel_interior T"
  2642     by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl)
  2643   have gim: "g ` rel_interior T \<subseteq> rel_interior S"
  2644     by (metis \<open>inj_on g T\<close> aff contg continuous_image_subset_rel_interior gTS order_refl)
  2645   show "homeomorphism (rel_interior S) (rel_interior T) f g"
  2646     unfolding homeomorphism_def
  2647   proof (intro conjI ballI)
  2648     show gf: "\<And>x. x \<in> rel_interior S \<Longrightarrow> g (f x) = x"
  2649       using S rel_interior_subset by blast
  2650     show fg: "\<And>y. y \<in> rel_interior T \<Longrightarrow> f (g y) = y"
  2651       using T mem_rel_interior_ball by blast
  2652     have "rel_interior T \<subseteq> f ` rel_interior S"
  2653     proof
  2654       fix x assume "x \<in> rel_interior T"
  2655       then have "g x \<in> rel_interior S"
  2656         using gim by blast
  2657       then show "x \<in> f ` rel_interior S"
  2658         by (metis fg \<open>x \<in> rel_interior T\<close> imageI)
  2659     qed
  2660     moreover have "f ` rel_interior S \<subseteq> rel_interior T"
  2661       by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl)
  2662     ultimately show "f ` rel_interior S = rel_interior T"
  2663       by blast
  2664     show "continuous_on (rel_interior S) f"
  2665       using contf continuous_on_subset rel_interior_subset by blast
  2666     have "rel_interior S \<subseteq> g ` rel_interior T"
  2667     proof
  2668       fix x assume "x \<in> rel_interior S"
  2669       then have "f x \<in> rel_interior T"
  2670         using fim by blast
  2671       then show "x \<in> g ` rel_interior T"
  2672         by (metis gf \<open>x \<in> rel_interior S\<close> imageI)
  2673     qed
  2674     then show "g ` rel_interior T = rel_interior S"
  2675       using gim by blast
  2676     show "continuous_on (rel_interior T) g"
  2677       using contg continuous_on_subset rel_interior_subset by blast
  2678   qed
  2679 qed
  2680 
  2681 lemma homeomorphic_rel_interiors:
  2682   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  2683   assumes "S homeomorphic T" "rel_interior S = {} \<longleftrightarrow> rel_interior T = {}"
  2684     shows "(rel_interior S) homeomorphic (rel_interior T)"
  2685 proof (cases "rel_interior T = {}")
  2686   case True
  2687   with assms show ?thesis by auto
  2688 next
  2689   case False
  2690   obtain f g
  2691     where S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
  2692       and contf: "continuous_on S f" and contg: "continuous_on T g"
  2693     using  assms [unfolded homeomorphic_minimal] by auto
  2694   have "aff_dim (affine hull S) \<le> aff_dim (affine hull T)"
  2695     apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior S" _ f])
  2696           apply (simp_all add: openin_rel_interior False assms)
  2697     using contf continuous_on_subset rel_interior_subset apply blast
  2698       apply (meson S hull_subset image_subsetI rel_interior_subset rev_subsetD)
  2699     apply (metis S inj_on_inverseI inj_on_subset rel_interior_subset)
  2700     done
  2701   moreover have "aff_dim (affine hull T) \<le> aff_dim (affine hull S)"
  2702     apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior T" _ g])
  2703           apply (simp_all add: openin_rel_interior False assms)
  2704     using contg continuous_on_subset rel_interior_subset apply blast
  2705       apply (meson T hull_subset image_subsetI rel_interior_subset rev_subsetD)
  2706     apply (metis T inj_on_inverseI inj_on_subset rel_interior_subset)
  2707     done
  2708   ultimately have "aff_dim S = aff_dim T" by force
  2709   then show ?thesis
  2710     by (rule homeomorphic_rel_interiors_same_dimension [OF \<open>S homeomorphic T\<close>])
  2711 qed
  2712 
  2713 
  2714 lemma homeomorphic_rel_boundaries_same_dimension:
  2715   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  2716   assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T"
  2717   shows "(S - rel_interior S) homeomorphic (T - rel_interior T)"
  2718   using assms [unfolded homeomorphic_minimal]
  2719   unfolding homeomorphic_def
  2720 proof (clarify elim!: ex_forward)
  2721   fix f g
  2722   assume S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
  2723      and contf: "continuous_on S f" and contg: "continuous_on T g"
  2724   then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
  2725     by (auto simp: inj_on_def intro: rev_image_eqI) metis+
  2726   have fim: "f ` rel_interior S \<subseteq> rel_interior T"
  2727     by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl)
  2728   have gim: "g ` rel_interior T \<subseteq> rel_interior S"
  2729     by (metis \<open>inj_on g T\<close> aff contg continuous_image_subset_rel_interior gTS order_refl)
  2730   show "homeomorphism (S - rel_interior S) (T - rel_interior T) f g"
  2731     unfolding homeomorphism_def
  2732   proof (intro conjI ballI)
  2733     show gf: "\<And>x. x \<in> S - rel_interior S \<Longrightarrow> g (f x) = x"
  2734       using S rel_interior_subset by blast
  2735     show fg: "\<And>y. y \<in> T - rel_interior T \<Longrightarrow> f (g y) = y"
  2736       using T mem_rel_interior_ball by blast
  2737     show "f ` (S - rel_interior S) = T - rel_interior T"
  2738       using S fST fim gim by auto
  2739     show "continuous_on (S - rel_interior S) f"
  2740       using contf continuous_on_subset rel_interior_subset by blast
  2741     show "g ` (T - rel_interior T) = S - rel_interior S"
  2742       using T gTS gim fim by auto
  2743     show "continuous_on (T - rel_interior T) g"
  2744       using contg continuous_on_subset rel_interior_subset by blast
  2745   qed
  2746 qed
  2747 
  2748 lemma homeomorphic_rel_boundaries:
  2749   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  2750   assumes "S homeomorphic T" "rel_interior S = {} \<longleftrightarrow> rel_interior T = {}"
  2751     shows "(S - rel_interior S) homeomorphic (T - rel_interior T)"
  2752 proof (cases "rel_interior T = {}")
  2753   case True
  2754   with assms show ?thesis by auto
  2755 next
  2756   case False
  2757   obtain f g
  2758     where S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
  2759       and contf: "continuous_on S f" and contg: "continuous_on T g"
  2760     using  assms [unfolded homeomorphic_minimal] by auto
  2761   have "aff_dim (affine hull S) \<le> aff_dim (affine hull T)"
  2762     apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior S" _ f])
  2763           apply (simp_all add: openin_rel_interior False assms)
  2764     using contf continuous_on_subset rel_interior_subset apply blast
  2765       apply (meson S hull_subset image_subsetI rel_interior_subset rev_subsetD)
  2766     apply (metis S inj_on_inverseI inj_on_subset rel_interior_subset)
  2767     done
  2768   moreover have "aff_dim (affine hull T) \<le> aff_dim (affine hull S)"
  2769     apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior T" _ g])
  2770           apply (simp_all add: openin_rel_interior False assms)
  2771     using contg continuous_on_subset rel_interior_subset apply blast
  2772       apply (meson T hull_subset image_subsetI rel_interior_subset rev_subsetD)
  2773     apply (metis T inj_on_inverseI inj_on_subset rel_interior_subset)
  2774     done
  2775   ultimately have "aff_dim S = aff_dim T" by force
  2776   then show ?thesis
  2777     by (rule homeomorphic_rel_boundaries_same_dimension [OF \<open>S homeomorphic T\<close>])
  2778 qed
  2779 
  2780 proposition uniformly_continuous_homeomorphism_UNIV_trivial:
  2781   fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
  2782   assumes contf: "uniformly_continuous_on S f" and hom: "homeomorphism S UNIV f g"
  2783   shows "S = UNIV"
  2784 proof (cases "S = {}")
  2785   case True
  2786   then show ?thesis
  2787     by (metis UNIV_I hom empty_iff homeomorphism_def image_eqI)
  2788 next
  2789   case False
  2790   have "inj g"
  2791     by (metis UNIV_I hom homeomorphism_apply2 injI)
  2792   then have "open (g ` UNIV)"
  2793     by (blast intro: invariance_of_domain hom homeomorphism_cont2)
  2794   then have "open S"
  2795     using hom homeomorphism_image2 by blast
  2796   moreover have "complete S"
  2797     unfolding complete_def
  2798   proof clarify
  2799     fix \<sigma>
  2800     assume \<sigma>: "\<forall>n. \<sigma> n \<in> S" and "Cauchy \<sigma>"
  2801     have "Cauchy (f o \<sigma>)"
  2802       using uniformly_continuous_imp_Cauchy_continuous \<open>Cauchy \<sigma>\<close> \<sigma> contf by blast
  2803     then obtain l where "(f \<circ> \<sigma>) \<longlonglongrightarrow> l"
  2804       by (auto simp: convergent_eq_Cauchy [symmetric])
  2805     show "\<exists>l\<in>S. \<sigma> \<longlonglongrightarrow> l"
  2806     proof
  2807       show "g l \<in> S"
  2808         using hom homeomorphism_image2 by blast
  2809       have "(g \<circ> (f \<circ> \<sigma>)) \<longlonglongrightarrow> g l"
  2810         by (meson UNIV_I \<open>(f \<circ> \<sigma>) \<longlonglongrightarrow> l\<close> continuous_on_sequentially hom homeomorphism_cont2)
  2811       then show "\<sigma> \<longlonglongrightarrow> g l"
  2812       proof -
  2813         have "\<forall>n. \<sigma> n = (g \<circ> (f \<circ> \<sigma>)) n"
  2814           by (metis (no_types) \<sigma> comp_eq_dest_lhs hom homeomorphism_apply1)
  2815         then show ?thesis
  2816           by (metis (no_types) LIMSEQ_iff \<open>(g \<circ> (f \<circ> \<sigma>)) \<longlonglongrightarrow> g l\<close>)
  2817       qed
  2818     qed
  2819   qed
  2820   then have "closed S"
  2821     by (simp add: complete_eq_closed)
  2822   ultimately show ?thesis
  2823     using clopen [of S] False  by simp
  2824 qed
  2825 
  2826 proposition invariance_of_domain_sphere_affine_set_gen:
  2827   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  2828   assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
  2829       and U: "bounded U" "convex U"
  2830       and "affine T" and affTU: "aff_dim T < aff_dim U"
  2831       and ope: "openin (top_of_set (rel_frontier U)) S"
  2832    shows "openin (top_of_set T) (f ` S)"
  2833 proof (cases "rel_frontier U = {}")
  2834   case True
  2835   then show ?thesis
  2836     using ope openin_subset by force
  2837 next
  2838   case False
  2839   obtain b c where b: "b \<in> rel_frontier U" and c: "c \<in> rel_frontier U" and "b \<noteq> c"
  2840     using \<open>bounded U\<close> rel_frontier_not_sing [of U] subset_singletonD False  by fastforce
  2841   obtain V :: "'a set" where "affine V" and affV: "aff_dim V = aff_dim U - 1"
  2842   proof (rule choose_affine_subset [OF affine_UNIV])
  2843     show "- 1 \<le> aff_dim U - 1"
  2844       by (metis aff_dim_empty aff_dim_geq aff_dim_negative_iff affTU diff_0 diff_right_mono not_le)
  2845     show "aff_dim U - 1 \<le> aff_dim (UNIV::'a set)"
  2846       by (metis aff_dim_UNIV aff_dim_le_DIM le_cases not_le zle_diff1_eq)
  2847   qed auto
  2848   have SU: "S \<subseteq> rel_frontier U"
  2849     using ope openin_imp_subset by auto
  2850   have homb: "rel_frontier U - {b} homeomorphic V"
  2851    and homc: "rel_frontier U - {c} homeomorphic V"
  2852     using homeomorphic_punctured_sphere_affine_gen [of U _ V]
  2853     by (simp_all add: \<open>affine V\<close> affV U b c)
  2854   then obtain g h j k
  2855            where gh: "homeomorphism (rel_frontier U - {b}) V g h"
  2856              and jk: "homeomorphism (rel_frontier U - {c}) V j k"
  2857     by (auto simp: homeomorphic_def)
  2858   with SU have hgsub: "(h ` g ` (S - {b})) \<subseteq> S" and kjsub: "(k ` j ` (S - {c})) \<subseteq> S"
  2859     by (simp_all add: homeomorphism_def subset_eq)
  2860   have [simp]: "aff_dim T \<le> aff_dim V"
  2861     by (simp add: affTU affV)
  2862   have "openin (top_of_set T) ((f \<circ> h) ` g ` (S - {b}))"
  2863   proof (rule invariance_of_domain_affine_sets [OF _ \<open>affine V\<close>])
  2864     show "openin (top_of_set V) (g ` (S - {b}))"
  2865       apply (rule homeomorphism_imp_open_map [OF gh])
  2866       by (meson Diff_mono Diff_subset SU ope openin_delete openin_subset_trans order_refl)
  2867     show "continuous_on (g ` (S - {b})) (f \<circ> h)"
  2868        apply (rule continuous_on_compose)
  2869         apply (meson Diff_mono SU homeomorphism_def homeomorphism_of_subsets gh set_eq_subset)
  2870       using contf continuous_on_subset hgsub by blast
  2871     show "inj_on (f \<circ> h) (g ` (S - {b}))"
  2872       using kjsub
  2873       apply (clarsimp simp add: inj_on_def)
  2874       by (metis SU b homeomorphism_def inj_onD injf insert_Diff insert_iff gh rev_subsetD)
  2875     show "(f \<circ> h) ` g ` (S - {b}) \<subseteq> T"
  2876       by (metis fim image_comp image_mono hgsub subset_trans)
  2877   qed (auto simp: assms)
  2878   moreover
  2879   have "openin (top_of_set T) ((f \<circ> k) ` j ` (S - {c}))"
  2880   proof (rule invariance_of_domain_affine_sets [OF _ \<open>affine V\<close>])
  2881     show "openin (top_of_set V) (j ` (S - {c}))"
  2882       apply (rule homeomorphism_imp_open_map [OF jk])
  2883       by (meson Diff_mono Diff_subset SU ope openin_delete openin_subset_trans order_refl)
  2884     show "continuous_on (j ` (S - {c})) (f \<circ> k)"
  2885        apply (rule continuous_on_compose)
  2886         apply (meson Diff_mono SU homeomorphism_def homeomorphism_of_subsets jk set_eq_subset)
  2887       using contf continuous_on_subset kjsub by blast
  2888     show "inj_on (f \<circ> k) (j ` (S - {c}))"
  2889       using kjsub
  2890       apply (clarsimp simp add: inj_on_def)
  2891       by (metis SU c homeomorphism_def inj_onD injf insert_Diff insert_iff jk rev_subsetD)
  2892     show "(f \<circ> k) ` j ` (S - {c}) \<subseteq> T"
  2893       by (metis fim image_comp image_mono kjsub subset_trans)
  2894   qed (auto simp: assms)
  2895   ultimately have "openin (top_of_set T) ((f \<circ> h) ` g ` (S - {b}) \<union> ((f \<circ> k) ` j ` (S - {c})))"
  2896     by (rule openin_Un)
  2897   moreover have "(f \<circ> h) ` g ` (S - {b}) = f ` (S - {b})"
  2898   proof -
  2899     have "h ` g ` (S - {b}) = (S - {b})"
  2900     proof
  2901       show "h ` g ` (S - {b}) \<subseteq> S - {b}"
  2902         using homeomorphism_apply1 [OF gh] SU
  2903         by (fastforce simp add: image_iff image_subset_iff)
  2904       show "S - {b} \<subseteq> h ` g ` (S - {b})"
  2905         apply clarify
  2906         by  (metis SU subsetD homeomorphism_apply1 [OF gh] image_iff member_remove remove_def)
  2907     qed
  2908     then show ?thesis
  2909       by (metis image_comp)
  2910   qed
  2911   moreover have "(f \<circ> k) ` j ` (S - {c}) = f ` (S - {c})"
  2912   proof -
  2913     have "k ` j ` (S - {c}) = (S - {c})"
  2914     proof
  2915       show "k ` j ` (S - {c}) \<subseteq> S - {c}"
  2916         using homeomorphism_apply1 [OF jk] SU
  2917         by (fastforce simp add: image_iff image_subset_iff)
  2918       show "S - {c} \<subseteq> k ` j ` (S - {c})"
  2919         apply clarify
  2920         by  (metis SU subsetD homeomorphism_apply1 [OF jk] image_iff member_remove remove_def)
  2921     qed
  2922     then show ?thesis
  2923       by (metis image_comp)
  2924   qed
  2925   moreover have "f ` (S - {b}) \<union> f ` (S - {c}) = f ` (S)"
  2926     using \<open>b \<noteq> c\<close> by blast
  2927   ultimately show ?thesis
  2928     by simp
  2929 qed
  2930 
  2931 lemma invariance_of_domain_sphere_affine_set:
  2932   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  2933   assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
  2934       and "r \<noteq> 0" "affine T" and affTU: "aff_dim T < DIM('a)"
  2935       and ope: "openin (top_of_set (sphere a r)) S"
  2936    shows "openin (top_of_set T) (f ` S)"
  2937 proof (cases "sphere a r = {}")
  2938   case True
  2939   then show ?thesis
  2940     using ope openin_subset by force
  2941 next
  2942   case False
  2943   show ?thesis
  2944   proof (rule invariance_of_domain_sphere_affine_set_gen [OF contf injf fim bounded_cball convex_cball \<open>affine T\<close>])
  2945     show "aff_dim T < aff_dim (cball a r)"
  2946       by (metis False affTU aff_dim_cball assms(4) linorder_cases sphere_empty)
  2947     show "openin (top_of_set (rel_frontier (cball a r))) S"
  2948       by (simp add: \<open>r \<noteq> 0\<close> ope)
  2949   qed
  2950 qed
  2951 
  2952 lemma no_embedding_sphere_lowdim:
  2953   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  2954   assumes contf: "continuous_on (sphere a r) f" and injf: "inj_on f (sphere a r)" and "r > 0"
  2955    shows "DIM('a) \<le> DIM('b)"
  2956 proof -
  2957   have "False" if "DIM('a) > DIM('b)"
  2958   proof -
  2959     have "compact (f ` sphere a r)"
  2960       using compact_continuous_image
  2961       by (simp add: compact_continuous_image contf)
  2962     then have "\<not> open (f ` sphere a r)"
  2963       using compact_open
  2964       by (metis assms(3) image_is_empty not_less_iff_gr_or_eq sphere_eq_empty)
  2965     then show False
  2966       using invariance_of_domain_sphere_affine_set [OF contf injf subset_UNIV] \<open>r > 0\<close>
  2967       by (metis aff_dim_UNIV affine_UNIV less_irrefl of_nat_less_iff open_openin openin_subtopology_self subtopology_UNIV that)
  2968   qed
  2969   then show ?thesis
  2970     using not_less by blast
  2971 qed
  2972 
  2973 lemma empty_interior_lowdim_gen:
  2974   fixes S :: "'N::euclidean_space set" and T :: "'M::euclidean_space set"
  2975   assumes dim: "DIM('M) < DIM('N)" and ST: "S homeomorphic T" 
  2976   shows "interior S = {}"
  2977 proof -
  2978   obtain h :: "'M \<Rightarrow> 'N" where "linear h" "\<And>x. norm(h x) = norm x"
  2979     by (rule isometry_subset_subspace [OF subspace_UNIV subspace_UNIV, where ?'a = 'M and ?'b = 'N])
  2980        (use dim in auto)
  2981   then have "inj h"
  2982     by (metis linear_inj_iff_eq_0 norm_eq_zero)
  2983   then have "h ` T homeomorphic T"
  2984     using \<open>linear h\<close> homeomorphic_sym linear_homeomorphic_image by blast
  2985   then have "interior (h ` T) homeomorphic interior S"
  2986     using homeomorphic_interiors_same_dimension
  2987     by (metis ST homeomorphic_sym homeomorphic_trans)
  2988   moreover   
  2989   have "interior (range h) = {}"
  2990     by (simp add: \<open>inj h\<close> \<open>linear h\<close> dim dim_image_eq empty_interior_lowdim)
  2991   then have "interior (h ` T) = {}"
  2992     by (metis image_mono interior_mono subset_empty top_greatest)
  2993   ultimately show ?thesis
  2994     by simp
  2995 qed
  2996 
  2997 lemma empty_interior_lowdim_gen_le:
  2998   fixes S :: "'N::euclidean_space set" and T :: "'M::euclidean_space set"
  2999   assumes "DIM('M) \<le> DIM('N)"  "interior T = {}" "S homeomorphic T" 
  3000   shows "interior S = {}"
  3001   by (metis assms empty_interior_lowdim_gen homeomorphic_empty(1) homeomorphic_interiors_same_dimension less_le)
  3002 
  3003 lemma homeomorphic_affine_sets_eq:
  3004   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  3005   assumes "affine S" "affine T"
  3006   shows "S homeomorphic T \<longleftrightarrow> aff_dim S = aff_dim T"
  3007 proof (cases "S = {} \<or> T = {}")
  3008   case True
  3009   then show ?thesis
  3010     using assms homeomorphic_affine_sets by force
  3011 next
  3012   case False
  3013   then obtain a b where "a \<in> S" "b \<in> T"
  3014     by blast
  3015   then have "subspace ((+) (- a) ` S)" "subspace ((+) (- b) ` T)"
  3016     using affine_diffs_subspace assms by blast+
  3017   then show ?thesis
  3018     by (metis affine_imp_convex assms homeomorphic_affine_sets homeomorphic_convex_sets)
  3019 qed
  3020 
  3021 lemma homeomorphic_hyperplanes_eq:
  3022   fixes a :: "'M::euclidean_space" and c :: "'N::euclidean_space"
  3023   assumes "a \<noteq> 0" "c \<noteq> 0" 
  3024   shows "({x. a \<bullet> x = b} homeomorphic {x. c \<bullet> x = d} \<longleftrightarrow> DIM('M) = DIM('N))" (is "?lhs = ?rhs")
  3025 proof -
  3026   have "(DIM('M) - Suc 0 = DIM('N) - Suc 0) \<longleftrightarrow> (DIM('M) = DIM('N))"
  3027     by auto (metis DIM_positive Suc_pred)
  3028   then show ?thesis
  3029     using assms by (simp add: homeomorphic_affine_sets_eq affine_hyperplane)
  3030 qed
  3031 
  3032 end