src/HOL/Homology/Invariance_of_Domain.thy
 author paulson 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
```