src/HOL/Homology/Invariance_of_Domain.thy
author paulson <lp15@cam.ac.uk>
Thu Apr 11 15:26:04 2019 +0100 (6 months ago)
changeset 70125 b601c2c87076
parent 70114 089c17514794
child 70136 f03a01a18c6e
permissions -rw-r--r--
type instantiations for poly_mapping as a real_normed_vector
lp15@70097
     1
section\<open>Invariance of Domain\<close>
lp15@70097
     2
lp15@70097
     3
theory Invariance_of_Domain
lp15@70114
     4
  imports Brouwer_Degree "HOL-Analysis.Continuous_Extension" "HOL-Analysis.Homeomorphism"
lp15@70097
     5
lp15@70097
     6
begin
lp15@70097
     7
lp15@70097
     8
subsection\<open>Degree invariance mod 2 for map between pairs\<close>
lp15@70097
     9
lp15@70097
    10
theorem Borsuk_odd_mapping_degree_step:
lp15@70097
    11
  assumes cmf: "continuous_map (nsphere n) (nsphere n) f"
lp15@70097
    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"
lp15@70097
    13
    and fim: "f ` (topspace(nsphere(n - Suc 0))) \<subseteq> topspace(nsphere(n - Suc 0))"
lp15@70097
    14
  shows "even (Brouwer_degree2 n f - Brouwer_degree2 (n - Suc 0) f)"
lp15@70097
    15
proof (cases "n = 0")
lp15@70097
    16
  case False
lp15@70097
    17
  define neg where "neg \<equiv> \<lambda>x::nat\<Rightarrow>real. \<lambda>i. -x i"
lp15@70097
    18
  define upper where "upper \<equiv> \<lambda>n. {x::nat\<Rightarrow>real. x n \<ge> 0}"
lp15@70097
    19
  define lower where "lower \<equiv> \<lambda>n. {x::nat\<Rightarrow>real. x n \<le> 0}"
lp15@70097
    20
  define equator where "equator \<equiv> \<lambda>n. {x::nat\<Rightarrow>real. x n = 0}"
lp15@70097
    21
  define usphere where "usphere \<equiv> \<lambda>n. subtopology (nsphere n) (upper n)"
lp15@70097
    22
  define lsphere where "lsphere \<equiv> \<lambda>n. subtopology (nsphere n) (lower n)"
lp15@70097
    23
  have [simp]: "neg x i = -x i" for x i
lp15@70097
    24
    by (force simp: neg_def)
lp15@70097
    25
  have equator_upper: "equator n \<subseteq> upper n"
lp15@70097
    26
    by (force simp: equator_def upper_def)
lp15@70097
    27
  have upper_usphere: "subtopology (nsphere n) (upper n) = usphere n"
lp15@70097
    28
    by (simp add: usphere_def)
lp15@70097
    29
  let ?rhgn = "relative_homology_group n (nsphere n)"
lp15@70097
    30
  let ?hi_ee = "hom_induced n (nsphere n) (equator n) (nsphere n) (equator n)"
lp15@70097
    31
  interpret GE: comm_group "?rhgn (equator n)"
lp15@70097
    32
    by simp
lp15@70097
    33
  interpret HB: group_hom "?rhgn (equator n)"
lp15@70097
    34
                          "homology_group (int n - 1) (subtopology (nsphere n) (equator n))"
lp15@70097
    35
                          "hom_boundary n (nsphere n) (equator n)"
lp15@70097
    36
    by (simp add: group_hom_axioms_def group_hom_def hom_boundary_hom)
lp15@70097
    37
  interpret HIU: group_hom "?rhgn (equator n)"
lp15@70097
    38
                           "?rhgn (upper n)"
lp15@70097
    39
                           "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id"
lp15@70097
    40
    by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom)
lp15@70097
    41
  have subt_eq: "subtopology (nsphere n) {x. x n = 0} = nsphere (n - Suc 0)"
lp15@70097
    42
    by (metis False Suc_pred le_zero_eq not_le subtopology_nsphere_equator)
lp15@70097
    43
  then have equ: "subtopology (nsphere n) (equator n) = nsphere(n - Suc 0)"
lp15@70097
    44
    "subtopology (lsphere n) (equator n) = nsphere(n - Suc 0)"
lp15@70097
    45
    "subtopology (usphere n) (equator n) = nsphere(n - Suc 0)"
lp15@70097
    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)
lp15@70097
    47
  have cmr: "continuous_map (nsphere(n - Suc 0)) (nsphere(n - Suc 0)) f"
lp15@70097
    48
    by (metis (no_types, lifting) IntE cmf fim continuous_map_from_subtopology continuous_map_in_subtopology equ(1) image_subset_iff topspace_subtopology)
lp15@70097
    49
lp15@70097
    50
  have "f x n = 0" if "x \<in> topspace (nsphere n)" "x n = 0" for x
lp15@70097
    51
  proof -
lp15@70097
    52
    have "x \<in> topspace (nsphere (n - Suc 0))"
lp15@70097
    53
      by (simp add: that topspace_nsphere_minus1)
lp15@70097
    54
    moreover have "topspace (nsphere n) \<inter> {f. f n = 0} = topspace (nsphere (n - Suc 0))"
lp15@70097
    55
      by (metis subt_eq topspace_subtopology)
lp15@70097
    56
    ultimately show ?thesis
lp15@70097
    57
      using cmr continuous_map_def by fastforce
lp15@70097
    58
  qed
lp15@70097
    59
  then have fimeq: "f ` (topspace (nsphere n) \<inter> equator n) \<subseteq> topspace (nsphere n) \<inter> equator n"
lp15@70097
    60
    using fim cmf by (auto simp: equator_def continuous_map_def image_subset_iff)
lp15@70097
    61
  have "\<And>k. continuous_map (powertop_real UNIV) euclideanreal (\<lambda>x. - x k)"
lp15@70097
    62
    by (metis UNIV_I continuous_map_product_projection continuous_map_minus)
lp15@70097
    63
  then have cm_neg: "continuous_map (nsphere m) (nsphere m) neg" for m
lp15@70097
    64
    by (force simp: nsphere continuous_map_in_subtopology neg_def continuous_map_componentwise_UNIV intro: continuous_map_from_subtopology)
lp15@70097
    65
  then have cm_neg_lu: "continuous_map (lsphere n) (usphere n) neg"
lp15@70097
    66
      by (auto simp: lsphere_def usphere_def lower_def upper_def continuous_map_from_subtopology continuous_map_in_subtopology)
lp15@70097
    67
  have neg_in_top_iff: "neg x \<in> topspace(nsphere m) \<longleftrightarrow> x \<in> topspace(nsphere m)" for m x
lp15@70097
    68
    by (simp add: nsphere_def neg_def topspace_Euclidean_space)
lp15@70097
    69
  obtain z where zcarr: "z \<in> carrier (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))"
lp15@70097
    70
    and zeq: "subgroup_generated (reduced_homology_group (int n - 1) (nsphere (n - Suc 0))) {z}
lp15@70097
    71
              = reduced_homology_group (int n - 1) (nsphere (n - Suc 0))"
lp15@70097
    72
    using cyclic_reduced_homology_group_nsphere [of "int n - 1" "n - Suc 0"] by (auto simp: cyclic_group_def)
lp15@70097
    73
  have "hom_boundary n (subtopology (nsphere n) {x. x n \<le> 0}) {x. x n = 0}
lp15@70097
    74
      \<in> Group.iso (relative_homology_group n
lp15@70097
    75
                     (subtopology (nsphere n) {x. x n \<le> 0}) {x. x n = 0})
lp15@70097
    76
                  (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))"
lp15@70097
    77
    using iso_lower_hemisphere_reduced_homology_group [of "int n - 1" "n - Suc 0"] False by simp
lp15@70097
    78
  then obtain gp where g: "group_isomorphisms
lp15@70097
    79
                          (relative_homology_group n (subtopology (nsphere n) {x. x n \<le> 0}) {x. x n = 0})
lp15@70097
    80
                          (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))
lp15@70097
    81
                          (hom_boundary n (subtopology (nsphere n) {x. x n \<le> 0}) {x. x n = 0})
lp15@70097
    82
                          gp"
lp15@70097
    83
    by (auto simp: group.iso_iff_group_isomorphisms)
lp15@70097
    84
  then interpret gp: group_hom "reduced_homology_group (int n - 1) (nsphere (n - Suc 0))"
lp15@70097
    85
    "relative_homology_group n (subtopology (nsphere n) {x. x n \<le> 0}) {x. x n = 0}" gp
lp15@70097
    86
    by (simp add: group_hom_axioms_def group_hom_def group_isomorphisms_def)
lp15@70097
    87
  obtain zp where zpcarr: "zp \<in> carrier(relative_homology_group n (lsphere n) (equator n))"
lp15@70097
    88
    and zp_z: "hom_boundary n (lsphere n) (equator n) zp = z"
lp15@70097
    89
    and zp_sg: "subgroup_generated (relative_homology_group n (lsphere n) (equator n)) {zp}
lp15@70097
    90
                = relative_homology_group n (lsphere n) (equator n)"
lp15@70097
    91
  proof
lp15@70097
    92
    show "gp z \<in> carrier (relative_homology_group n (lsphere n) (equator n))"
lp15@70097
    93
      "hom_boundary n (lsphere n) (equator n) (gp z) = z"
lp15@70097
    94
      using g zcarr by (auto simp: lsphere_def equator_def lower_def group_isomorphisms_def)
lp15@70097
    95
    have giso: "gp \<in> Group.iso (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))
lp15@70097
    96
                     (relative_homology_group n (subtopology (nsphere n) {x. x n \<le> 0}) {x. x n = 0})"
lp15@70097
    97
      by (metis (mono_tags, lifting) g group_isomorphisms_imp_iso group_isomorphisms_sym)
lp15@70097
    98
    show "subgroup_generated (relative_homology_group n (lsphere n) (equator n)) {gp z} =
lp15@70097
    99
        relative_homology_group n (lsphere n) (equator n)"
lp15@70097
   100
      apply (rule monoid.equality)
lp15@70097
   101
      using giso gp.subgroup_generated_by_image [of "{z}"] zcarr
lp15@70097
   102
      by (auto simp: lsphere_def equator_def lower_def zeq gp.iso_iff)
lp15@70097
   103
  qed
lp15@70097
   104
  have hb_iso: "hom_boundary n (subtopology (nsphere n) {x. x n \<ge> 0}) {x. x n = 0}
lp15@70097
   105
            \<in> iso (relative_homology_group n (subtopology (nsphere n) {x. x n \<ge> 0}) {x. x n = 0})
lp15@70097
   106
                  (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))"
lp15@70097
   107
    using iso_upper_hemisphere_reduced_homology_group [of "int n - 1" "n - Suc 0"] False by simp
lp15@70097
   108
  then obtain gn where g: "group_isomorphisms
lp15@70097
   109
                          (relative_homology_group n (subtopology (nsphere n) {x. x n \<ge> 0}) {x. x n = 0})
lp15@70097
   110
                          (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))
lp15@70097
   111
                          (hom_boundary n (subtopology (nsphere n) {x. x n \<ge> 0}) {x. x n = 0})
lp15@70097
   112
                          gn"
lp15@70097
   113
    by (auto simp: group.iso_iff_group_isomorphisms)
lp15@70097
   114
  then interpret gn: group_hom "reduced_homology_group (int n - 1) (nsphere (n - Suc 0))"
lp15@70097
   115
    "relative_homology_group n (subtopology (nsphere n) {x. x n \<ge> 0}) {x. x n = 0}" gn
lp15@70097
   116
    by (simp add: group_hom_axioms_def group_hom_def group_isomorphisms_def)
lp15@70097
   117
  obtain zn where zncarr: "zn \<in> carrier(relative_homology_group n (usphere n) (equator n))"
lp15@70097
   118
    and zn_z: "hom_boundary n (usphere n) (equator n) zn = z"
lp15@70097
   119
    and zn_sg: "subgroup_generated (relative_homology_group n (usphere n) (equator n)) {zn}
lp15@70097
   120
                 = relative_homology_group n (usphere n) (equator n)"
lp15@70097
   121
  proof
lp15@70097
   122
    show "gn z \<in> carrier (relative_homology_group n (usphere n) (equator n))"
lp15@70097
   123
      "hom_boundary n (usphere n) (equator n) (gn z) = z"
lp15@70097
   124
      using g zcarr by (auto simp: usphere_def equator_def upper_def group_isomorphisms_def)
lp15@70097
   125
    have giso: "gn \<in> Group.iso (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))
lp15@70097
   126
                     (relative_homology_group n (subtopology (nsphere n) {x. x n \<ge> 0}) {x. x n = 0})"
lp15@70097
   127
      by (metis (mono_tags, lifting) g group_isomorphisms_imp_iso group_isomorphisms_sym)
lp15@70097
   128
    show "subgroup_generated (relative_homology_group n (usphere n) (equator n)) {gn z} =
lp15@70097
   129
        relative_homology_group n (usphere n) (equator n)"
lp15@70097
   130
      apply (rule monoid.equality)
lp15@70097
   131
      using giso gn.subgroup_generated_by_image [of "{z}"] zcarr
lp15@70097
   132
      by (auto simp: usphere_def equator_def upper_def zeq gn.iso_iff)
lp15@70097
   133
  qed
lp15@70097
   134
  let ?hi_lu = "hom_induced n (lsphere n) (equator n) (nsphere n) (upper n) id"
lp15@70097
   135
  interpret gh_lu: group_hom "relative_homology_group n (lsphere n) (equator n)" "?rhgn (upper n)" ?hi_lu
lp15@70097
   136
    by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom)
lp15@70097
   137
  interpret gh_eef: group_hom "?rhgn (equator n)" "?rhgn (equator n)" "?hi_ee f"
lp15@70097
   138
    by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom)
lp15@70097
   139
  define wp where "wp \<equiv> ?hi_lu zp"
lp15@70097
   140
  then have wpcarr: "wp \<in> carrier(?rhgn (upper n))"
lp15@70097
   141
    by (simp add: hom_induced_carrier)
lp15@70097
   142
  have "hom_induced n (nsphere n) {} (nsphere n) {x. x n \<ge> 0} id
lp15@70097
   143
      \<in> iso (reduced_homology_group n (nsphere n))
lp15@70097
   144
            (?rhgn {x. x n \<ge> 0})"
lp15@70097
   145
    using iso_reduced_homology_group_upper_hemisphere [of n n n] by auto
lp15@70097
   146
  then have "carrier(?rhgn {x. x n \<ge> 0})
lp15@70097
   147
          \<subseteq> (hom_induced n (nsphere n) {} (nsphere n) {x. x n \<ge> 0} id)
lp15@70097
   148
                         ` carrier(reduced_homology_group n (nsphere n))"
lp15@70097
   149
    by (simp add: iso_iff)
lp15@70097
   150
  then obtain vp where vpcarr: "vp \<in> carrier(reduced_homology_group n (nsphere n))"
lp15@70097
   151
    and eqwp: "hom_induced n (nsphere n) {} (nsphere n) (upper n) id vp = wp"
lp15@70097
   152
    using wpcarr by (auto simp: upper_def)
lp15@70097
   153
  define wn where "wn \<equiv> hom_induced n (usphere n) (equator n) (nsphere n) (lower n) id zn"
lp15@70097
   154
  then have wncarr: "wn \<in> carrier(?rhgn (lower n))"
lp15@70097
   155
    by (simp add: hom_induced_carrier)
lp15@70097
   156
  have "hom_induced n (nsphere n) {} (nsphere n) {x. x n \<le> 0} id
lp15@70097
   157
      \<in> iso (reduced_homology_group n (nsphere n))
lp15@70097
   158
            (?rhgn {x. x n \<le> 0})"
lp15@70097
   159
    using iso_reduced_homology_group_lower_hemisphere [of n n n] by auto
lp15@70097
   160
  then have "carrier(?rhgn {x. x n \<le> 0})
lp15@70097
   161
          \<subseteq> (hom_induced n (nsphere n) {} (nsphere n) {x. x n \<le> 0} id)
lp15@70097
   162
                         ` carrier(reduced_homology_group n (nsphere n))"
lp15@70097
   163
    by (simp add: iso_iff)
lp15@70097
   164
  then obtain vn where vpcarr: "vn \<in> carrier(reduced_homology_group n (nsphere n))"
lp15@70097
   165
    and eqwp: "hom_induced n (nsphere n) {} (nsphere n) (lower n) id vn = wn"
lp15@70097
   166
    using wncarr by (auto simp: lower_def)
lp15@70097
   167
  define up where "up \<equiv> hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id zp"
lp15@70097
   168
  then have upcarr: "up \<in> carrier(?rhgn (equator n))"
lp15@70097
   169
    by (simp add: hom_induced_carrier)
lp15@70097
   170
  define un where "un \<equiv> hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id zn"
lp15@70097
   171
  then have uncarr: "un \<in> carrier(?rhgn (equator n))"
lp15@70097
   172
    by (simp add: hom_induced_carrier)
lp15@70097
   173
  have *: "(\<lambda>(x, y).
lp15@70097
   174
            hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id x
lp15@70097
   175
          \<otimes>\<^bsub>?rhgn (equator n)\<^esub>
lp15@70097
   176
            hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id y)
lp15@70097
   177
        \<in> Group.iso
lp15@70097
   178
            (relative_homology_group n (lsphere n) (equator n) \<times>\<times>
lp15@70097
   179
             relative_homology_group n (usphere n) (equator n))
lp15@70097
   180
            (?rhgn (equator n))"
lp15@70097
   181
  proof (rule conjunct1 [OF exact_sequence_sum_lemma [OF abelian_relative_homology_group]])
lp15@70097
   182
    show "hom_induced n (lsphere n) (equator n) (nsphere n) (upper n) id
lp15@70097
   183
        \<in> Group.iso (relative_homology_group n (lsphere n) (equator n))
lp15@70097
   184
            (?rhgn (upper n))"
lp15@70097
   185
      apply (simp add: lsphere_def usphere_def equator_def lower_def upper_def)
lp15@70097
   186
      using iso_relative_homology_group_lower_hemisphere by blast
lp15@70097
   187
    show "hom_induced n (usphere n) (equator n) (nsphere n) (lower n) id
lp15@70097
   188
        \<in> Group.iso (relative_homology_group n (usphere n) (equator n))
lp15@70097
   189
            (?rhgn (lower n))"
lp15@70097
   190
      apply (simp_all add: lsphere_def usphere_def equator_def lower_def upper_def)
lp15@70097
   191
      using iso_relative_homology_group_upper_hemisphere by blast+
lp15@70097
   192
    show "exact_seq
lp15@70097
   193
         ([?rhgn (lower n),
lp15@70097
   194
           ?rhgn (equator n),
lp15@70097
   195
           relative_homology_group n (lsphere n) (equator n)],
lp15@70097
   196
          [hom_induced n (nsphere n) (equator n) (nsphere n) (lower n) id,
lp15@70097
   197
           hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id])"
lp15@70097
   198
      unfolding lsphere_def usphere_def equator_def lower_def upper_def
lp15@70097
   199
      by (rule homology_exactness_triple_3) force
lp15@70097
   200
    show "exact_seq
lp15@70097
   201
         ([?rhgn (upper n),
lp15@70097
   202
           ?rhgn (equator n),
lp15@70097
   203
           relative_homology_group n (usphere n) (equator n)],
lp15@70097
   204
          [hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id,
lp15@70097
   205
           hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id])"
lp15@70097
   206
      unfolding lsphere_def usphere_def equator_def lower_def upper_def
lp15@70097
   207
      by (rule homology_exactness_triple_3) force
lp15@70097
   208
  next
lp15@70097
   209
    fix x
lp15@70097
   210
    assume "x \<in> carrier (relative_homology_group n (lsphere n) (equator n))"
lp15@70097
   211
    show "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id
lp15@70097
   212
         (hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id x) =
lp15@70097
   213
        hom_induced n (lsphere n) (equator n) (nsphere n) (upper n) id x"
lp15@70097
   214
      by (simp add: hom_induced_compose' subset_iff lsphere_def usphere_def equator_def lower_def upper_def)
lp15@70097
   215
  next
lp15@70097
   216
    fix x
lp15@70097
   217
    assume "x \<in> carrier (relative_homology_group n (usphere n) (equator n))"
lp15@70097
   218
    show "hom_induced n (nsphere n) (equator n) (nsphere n) (lower n) id
lp15@70097
   219
         (hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id x) =
lp15@70097
   220
        hom_induced n (usphere n) (equator n) (nsphere n) (lower n) id x"
lp15@70097
   221
      by (simp add: hom_induced_compose' subset_iff lsphere_def usphere_def equator_def lower_def upper_def)
lp15@70097
   222
  qed
lp15@70097
   223
  then have sb: "carrier (?rhgn (equator n))
lp15@70097
   224
             \<subseteq> (\<lambda>(x, y).
lp15@70097
   225
            hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id x
lp15@70097
   226
          \<otimes>\<^bsub>?rhgn (equator n)\<^esub>
lp15@70097
   227
            hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id y)
lp15@70097
   228
               ` carrier (relative_homology_group n (lsphere n) (equator n) \<times>\<times>
lp15@70097
   229
             relative_homology_group n (usphere n) (equator n))"
lp15@70097
   230
    by (simp add: iso_iff)
lp15@70097
   231
  obtain a b::int
lp15@70097
   232
    where up_ab: "?hi_ee f up
lp15@70097
   233
             = up [^]\<^bsub>?rhgn (equator n)\<^esub> a\<otimes>\<^bsub>?rhgn (equator n)\<^esub> un [^]\<^bsub>?rhgn (equator n)\<^esub> b"
lp15@70097
   234
  proof -
lp15@70097
   235
    have hiupcarr: "?hi_ee f up \<in> carrier(?rhgn (equator n))"
lp15@70097
   236
      by (simp add: hom_induced_carrier)
lp15@70097
   237
    obtain u v where u: "u \<in> carrier (relative_homology_group n (lsphere n) (equator n))"
lp15@70097
   238
      and v: "v \<in> carrier (relative_homology_group n (usphere n) (equator n))"
lp15@70097
   239
      and eq: "?hi_ee f up =
lp15@70097
   240
                hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id u
lp15@70097
   241
                \<otimes>\<^bsub>?rhgn (equator n)\<^esub>
lp15@70097
   242
                hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id v"
lp15@70097
   243
      using subsetD [OF sb hiupcarr] by auto
lp15@70097
   244
    have "u \<in> carrier (subgroup_generated (relative_homology_group n (lsphere n) (equator n)) {zp})"
lp15@70097
   245
      by (simp_all add: u zp_sg)
lp15@70097
   246
    then obtain a::int where a: "u = zp [^]\<^bsub>relative_homology_group n (lsphere n) (equator n)\<^esub> a"
lp15@70097
   247
      by (metis group.carrier_subgroup_generated_by_singleton group_relative_homology_group rangeE zpcarr)
lp15@70097
   248
    have ae: "hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id
lp15@70097
   249
            (pow (relative_homology_group n (lsphere n) (equator n)) zp a)
lp15@70097
   250
          = pow (?rhgn (equator n)) (hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id zp) a"
lp15@70097
   251
      by (meson group_hom.hom_int_pow group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced zpcarr)
lp15@70097
   252
    have "v \<in> carrier (subgroup_generated (relative_homology_group n (usphere n) (equator n)) {zn})"
lp15@70097
   253
      by (simp_all add: v zn_sg)
lp15@70097
   254
    then obtain b::int where b: "v = zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> b"
lp15@70097
   255
      by (metis group.carrier_subgroup_generated_by_singleton group_relative_homology_group rangeE zncarr)
lp15@70097
   256
    have be: "hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id
lp15@70097
   257
           (zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> b)
lp15@70097
   258
        = hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id
lp15@70097
   259
           zn [^]\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub> b"
lp15@70097
   260
      by (meson group_hom.hom_int_pow group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced zncarr)
lp15@70097
   261
    show thesis
lp15@70097
   262
    proof
lp15@70097
   263
      show "?hi_ee f up
lp15@70097
   264
         = up [^]\<^bsub>?rhgn (equator n)\<^esub> a \<otimes>\<^bsub>?rhgn (equator n)\<^esub> un [^]\<^bsub>?rhgn (equator n)\<^esub> b"
lp15@70097
   265
        using a ae b be eq local.up_def un_def by auto
lp15@70097
   266
    qed
lp15@70097
   267
  qed
lp15@70097
   268
  have "(hom_boundary n (nsphere n) (equator n)
lp15@70097
   269
       \<circ> hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id) zp = z"
lp15@70097
   270
    using zp_z equ apply (simp add: lsphere_def naturality_hom_induced)
lp15@70097
   271
    by (metis hom_boundary_carrier hom_induced_id)
lp15@70097
   272
  then have up_z: "hom_boundary n (nsphere n) (equator n) up = z"
lp15@70097
   273
    by (simp add: up_def)
lp15@70097
   274
  have "(hom_boundary n (nsphere n) (equator n)
lp15@70097
   275
       \<circ> hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id) zn = z"
lp15@70097
   276
    using zn_z equ apply (simp add: usphere_def naturality_hom_induced)
lp15@70097
   277
    by (metis hom_boundary_carrier hom_induced_id)
lp15@70097
   278
  then have un_z: "hom_boundary n (nsphere n) (equator n) un = z"
lp15@70097
   279
    by (simp add: un_def)
lp15@70097
   280
  have Bd_ab: "Brouwer_degree2 (n - Suc 0) f = a + b"
lp15@70097
   281
  proof (rule Brouwer_degree2_unique_generator; use False int_ops in simp_all)
lp15@70097
   282
    show "continuous_map (nsphere (n - Suc 0)) (nsphere (n - Suc 0)) f"
lp15@70097
   283
      using cmr by auto
lp15@70097
   284
    show "subgroup_generated (reduced_homology_group (int n - 1) (nsphere (n - Suc 0))) {z} =
lp15@70097
   285
        reduced_homology_group (int n - 1) (nsphere (n - Suc 0))"
lp15@70097
   286
      using zeq by blast
lp15@70097
   287
    have "(hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} f
lp15@70097
   288
           \<circ> hom_boundary n (nsphere n) (equator n)) up
lp15@70097
   289
        = (hom_boundary n (nsphere n) (equator n) \<circ>
lp15@70097
   290
           ?hi_ee f) up"
lp15@70097
   291
      using naturality_hom_induced [OF cmf fimeq, of n, symmetric]
lp15@70097
   292
      by (simp add: subtopology_restrict equ fun_eq_iff)
lp15@70097
   293
    also have "\<dots> = hom_boundary n (nsphere n) (equator n)
lp15@70097
   294
                       (up [^]\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub>
lp15@70097
   295
                        a \<otimes>\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub>
lp15@70097
   296
                        un [^]\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub> b)"
lp15@70097
   297
      by (simp add: o_def up_ab)
lp15@70097
   298
    also have "\<dots> = z [^]\<^bsub>reduced_homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> (a + b)"
lp15@70097
   299
      using zcarr
lp15@70097
   300
      apply (simp add: HB.hom_int_pow reduced_homology_group_def group.int_pow_subgroup_generated upcarr uncarr)
lp15@70097
   301
      by (metis equ(1) group.int_pow_mult group_relative_homology_group hom_boundary_carrier un_z up_z)
lp15@70097
   302
  finally show "hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} f z =
lp15@70097
   303
        z [^]\<^bsub>reduced_homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> (a + b)"
lp15@70097
   304
      by (simp add: up_z)
lp15@70097
   305
  qed
lp15@70097
   306
  define u where "u \<equiv> up \<otimes>\<^bsub>?rhgn (equator n)\<^esub> inv\<^bsub>?rhgn (equator n)\<^esub> un"
lp15@70097
   307
  have ucarr: "u \<in> carrier (?rhgn (equator n))"
lp15@70097
   308
    by (simp add: u_def uncarr upcarr)
lp15@70097
   309
  then have "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f = u [^]\<^bsub>?rhgn (equator n)\<^esub> (a - b)
lp15@70097
   310
             \<longleftrightarrow> (GE.ord u) dvd a - b - Brouwer_degree2 n f"
lp15@70097
   311
    by (simp add: GE.int_pow_eq)
lp15@70097
   312
  moreover
lp15@70097
   313
  have "GE.ord u = 0"
lp15@70097
   314
  proof (clarsimp simp add: GE.ord_eq_0 ucarr)
lp15@70097
   315
    fix d :: nat
lp15@70097
   316
    assume "0 < d"
lp15@70097
   317
      and "u [^]\<^bsub>?rhgn (equator n)\<^esub> d = singular_relboundary_set n (nsphere n) (equator n)"
lp15@70097
   318
    then have "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id u [^]\<^bsub>?rhgn (upper n)\<^esub> d
lp15@70097
   319
               = \<one>\<^bsub>?rhgn (upper n)\<^esub>"
lp15@70097
   320
      by (metis HIU.hom_one HIU.hom_nat_pow one_relative_homology_group ucarr)
lp15@70097
   321
    moreover
lp15@70097
   322
    have "?hi_lu
lp15@70097
   323
        = hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id \<circ>
lp15@70097
   324
          hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id"
lp15@70097
   325
      by (simp add: lsphere_def image_subset_iff equator_upper flip: hom_induced_compose)
lp15@70097
   326
    then have p: "wp = hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id up"
lp15@70097
   327
      by (simp add: local.up_def wp_def)
lp15@70097
   328
    have n: "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id un = \<one>\<^bsub>?rhgn (upper n)\<^esub>"
lp15@70097
   329
      using homology_exactness_triple_3 [OF equator_upper, of n "nsphere n"]
lp15@70097
   330
      using un_def zncarr by (auto simp: upper_usphere kernel_def)
lp15@70097
   331
    have "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id u = wp"
lp15@70097
   332
      unfolding u_def
lp15@70097
   333
      using p n HIU.inv_one HIU.r_one uncarr upcarr by auto
lp15@70097
   334
    ultimately have "(wp [^]\<^bsub>?rhgn (upper n)\<^esub> d) = \<one>\<^bsub>?rhgn (upper n)\<^esub>"
lp15@70097
   335
      by simp
lp15@70097
   336
    moreover have "infinite (carrier (subgroup_generated (?rhgn (upper n)) {wp}))"
lp15@70097
   337
    proof -
lp15@70097
   338
      have "?rhgn (upper n) \<cong> reduced_homology_group n (nsphere n)"
lp15@70097
   339
        unfolding upper_def
lp15@70097
   340
        using iso_reduced_homology_group_upper_hemisphere [of n n n]
lp15@70097
   341
        by (blast intro: group.iso_sym group_reduced_homology_group is_isoI)
lp15@70097
   342
      also have "\<dots> \<cong> integer_group"
lp15@70097
   343
        by (simp add: reduced_homology_group_nsphere)
lp15@70097
   344
      finally have iso: "?rhgn (upper n) \<cong> integer_group" .
lp15@70097
   345
      have "carrier (subgroup_generated (?rhgn (upper n)) {wp}) = carrier (?rhgn (upper n))"
lp15@70097
   346
        using gh_lu.subgroup_generated_by_image [of "{zp}"] zpcarr HIU.carrier_subgroup_generated_subset
lp15@70097
   347
          gh_lu.iso_iff iso_relative_homology_group_lower_hemisphere zp_sg
lp15@70097
   348
        by (auto simp: lower_def lsphere_def upper_def equator_def wp_def)
lp15@70097
   349
      then show ?thesis
lp15@70097
   350
        using infinite_UNIV_int iso_finite [OF iso] by simp
lp15@70097
   351
    qed
lp15@70097
   352
    ultimately show False
lp15@70097
   353
      using HIU.finite_cyclic_subgroup \<open>0 < d\<close> wpcarr by blast
lp15@70097
   354
  qed
lp15@70097
   355
  ultimately have iff: "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f = u [^]\<^bsub>?rhgn (equator n)\<^esub> (a - b)
lp15@70097
   356
                   \<longleftrightarrow> Brouwer_degree2 n f = a - b"
lp15@70097
   357
    by auto
lp15@70097
   358
  have "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f = ?hi_ee f u"
lp15@70097
   359
  proof -
lp15@70097
   360
    have ne: "topspace (nsphere n) \<inter> equator n \<noteq> {}"
lp15@70097
   361
      by (metis equ(1) nonempty_nsphere topspace_subtopology)
lp15@70097
   362
    have eq1: "hom_boundary n (nsphere n) (equator n) u
lp15@70097
   363
               = \<one>\<^bsub>reduced_homology_group (int n - 1) (subtopology (nsphere n) (equator n))\<^esub>"
lp15@70097
   364
      using one_reduced_homology_group u_def un_z uncarr up_z upcarr by force
lp15@70097
   365
    then have uhom: "u \<in> hom_induced n (nsphere n) {} (nsphere n) (equator n) id `
lp15@70097
   366
                         carrier (reduced_homology_group (int n) (nsphere n))"
lp15@70097
   367
      using homology_exactness_reduced_1 [OF ne, of n] eq1 ucarr by (auto simp: kernel_def)
lp15@70097
   368
    then obtain v where vcarr: "v \<in> carrier (reduced_homology_group (int n) (nsphere n))"
lp15@70097
   369
                  and ueq: "u = hom_induced n (nsphere n) {} (nsphere n) (equator n) id v"
lp15@70097
   370
      by blast
lp15@70097
   371
    interpret GH_hi: group_hom "homology_group n (nsphere n)"
lp15@70097
   372
                        "?rhgn (equator n)"
lp15@70097
   373
                        "hom_induced n (nsphere n) {} (nsphere n) (equator n) id"
lp15@70097
   374
      by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom)
lp15@70097
   375
    have poweq: "pow (homology_group n (nsphere n)) x i = pow (reduced_homology_group n (nsphere n)) x i"
lp15@70097
   376
      for x and i::int
lp15@70097
   377
      by (simp add: False un_reduced_homology_group)
lp15@70097
   378
    have vcarr': "v \<in> carrier (homology_group n (nsphere n))"
lp15@70097
   379
      using carrier_reduced_homology_group_subset vcarr by blast
lp15@70097
   380
    have "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f
lp15@70097
   381
          = hom_induced n (nsphere n) {} (nsphere n) (equator n) f v"
lp15@70097
   382
      using vcarr vcarr'
lp15@70097
   383
      by (simp add: ueq poweq hom_induced_compose' cmf flip: GH_hi.hom_int_pow Brouwer_degree2)
lp15@70097
   384
    also have "\<dots> = hom_induced n (nsphere n) (topspace(nsphere n) \<inter> equator n) (nsphere n) (equator n) f
lp15@70097
   385
                     (hom_induced n (nsphere n) {} (nsphere n) (topspace(nsphere n) \<inter> equator n) id v)"
lp15@70097
   386
      using fimeq by (simp add: hom_induced_compose' cmf)
lp15@70097
   387
    also have "\<dots> = ?hi_ee f u"
lp15@70097
   388
      by (metis hom_induced inf.left_idem ueq)
lp15@70097
   389
    finally show ?thesis .
lp15@70097
   390
  qed
lp15@70097
   391
  moreover
lp15@70097
   392
  interpret gh_een: group_hom "?rhgn (equator n)" "?rhgn (equator n)" "?hi_ee neg"
lp15@70097
   393
    by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom)
lp15@70097
   394
  have hi_up_eq_un: "?hi_ee neg up = un [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg"
lp15@70097
   395
  proof -
lp15@70097
   396
    have "?hi_ee neg (hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id zp)
lp15@70097
   397
         = hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) (neg \<circ> id) zp"
lp15@70097
   398
      by (intro hom_induced_compose') (auto simp: lsphere_def equator_def cm_neg)
lp15@70097
   399
    also have "\<dots> = hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id
lp15@70097
   400
            (hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp)"
lp15@70097
   401
      by (subst hom_induced_compose' [OF cm_neg_lu]) (auto simp: usphere_def equator_def)
lp15@70097
   402
    also have "hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp
lp15@70097
   403
             = zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg"
lp15@70097
   404
    proof -
lp15@70097
   405
      let ?hb = "hom_boundary n (usphere n) (equator n)"
lp15@70097
   406
      have eq: "subtopology (nsphere n) {x. x n \<ge> 0} = usphere n \<and> {x. x n = 0} = equator n"
lp15@70097
   407
        by (auto simp: usphere_def upper_def equator_def)
lp15@70097
   408
      with hb_iso have inj: "inj_on (?hb) (carrier (relative_homology_group n (usphere n) (equator n)))"
lp15@70097
   409
        by (simp add: iso_iff)
lp15@70097
   410
      interpret hb_hom: group_hom "relative_homology_group n (usphere n) (equator n)"
lp15@70097
   411
                                  "reduced_homology_group (int n - 1) (nsphere (n - Suc 0))"
lp15@70097
   412
                                  "?hb"
lp15@70097
   413
        using hb_iso iso_iff eq group_hom_axioms_def group_hom_def by fastforce
lp15@70097
   414
      show ?thesis
lp15@70097
   415
      proof (rule inj_onD [OF inj])
lp15@70097
   416
        have *: "hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} neg z
lp15@70097
   417
                 = z [^]\<^bsub>homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> Brouwer_degree2 (n - Suc 0) neg"
lp15@70097
   418
          using Brouwer_degree2 [of z "n - Suc 0" neg] False zcarr
lp15@70097
   419
          by (simp add: int_ops group.int_pow_subgroup_generated reduced_homology_group_def)
lp15@70097
   420
        have "?hb \<circ>
lp15@70097
   421
              hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg
lp15@70097
   422
            = hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} neg \<circ>
lp15@70097
   423
              hom_boundary n (lsphere n) (equator n)"
lp15@70097
   424
          apply (subst naturality_hom_induced [OF cm_neg_lu])
lp15@70097
   425
           apply (force simp: equator_def neg_def)
lp15@70097
   426
          by (simp add: equ)
lp15@70097
   427
        then have "?hb
lp15@70097
   428
                    (hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp)
lp15@70097
   429
            = (z [^]\<^bsub>homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> Brouwer_degree2 (n - Suc 0) neg)"
lp15@70097
   430
          by (metis "*" comp_apply zp_z)
lp15@70097
   431
        also have "\<dots> = ?hb (zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub>
lp15@70097
   432
          Brouwer_degree2 (n - Suc 0) neg)"
lp15@70097
   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)
lp15@70097
   434
        finally show "?hb (hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp) =
lp15@70097
   435
        ?hb (zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub>
lp15@70097
   436
          Brouwer_degree2 (n - Suc 0) neg)" by simp
lp15@70097
   437
      qed (auto simp: hom_induced_carrier group.int_pow_closed zncarr)
lp15@70097
   438
    qed
lp15@70097
   439
    finally show ?thesis
lp15@70097
   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)
lp15@70097
   441
  qed
lp15@70097
   442
  have "continuous_map (nsphere (n - Suc 0)) (nsphere (n - Suc 0)) neg"
lp15@70097
   443
    using cm_neg by blast
lp15@70097
   444
  then have "homeomorphic_map (nsphere (n - Suc 0)) (nsphere (n - Suc 0)) neg"
lp15@70097
   445
    apply (auto simp: homeomorphic_map_maps homeomorphic_maps_def)
lp15@70097
   446
    apply (rule_tac x=neg in exI, auto)
lp15@70097
   447
    done
lp15@70097
   448
  then have Brouwer_degree2_21: "Brouwer_degree2 (n - Suc 0) neg ^ 2 = 1"
lp15@70097
   449
    using Brouwer_degree2_homeomorphic_map power2_eq_1_iff by force
lp15@70097
   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")
lp15@70097
   451
  proof -
lp15@70097
   452
    have [simp]: "neg \<circ> neg = id"
lp15@70097
   453
      by force
lp15@70097
   454
    have "?f (?f ?y) = ?y"
lp15@70097
   455
      apply (subst hom_induced_compose' [OF cm_neg _ cm_neg])
lp15@70097
   456
       apply(force simp: equator_def)
lp15@70097
   457
      apply (simp add: upcarr hom_induced_id_gen)
lp15@70097
   458
      done
lp15@70097
   459
    moreover have "?f ?y = un"
lp15@70097
   460
      using upcarr apply (simp only: gh_een.hom_int_pow hi_up_eq_un)
lp15@70097
   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)
lp15@70097
   462
    ultimately show "?f un = ?y"
lp15@70097
   463
      by simp
lp15@70097
   464
  qed
lp15@70097
   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"
lp15@70097
   466
  proof -
lp15@70097
   467
    let ?TE = "topspace (nsphere n) \<inter> equator n"
lp15@70097
   468
    have fneg: "(f \<circ> neg) x = (neg \<circ> f) x" if "x \<in> topspace (nsphere n)" for x
lp15@70097
   469
      using f [OF that] by (force simp: neg_def)
lp15@70097
   470
    have neg_im: "neg ` (topspace (nsphere n) \<inter> equator n) \<subseteq> topspace (nsphere n) \<inter> equator n"
lp15@70097
   471
      by (metis cm_neg continuous_map_image_subset_topspace equ(1) topspace_subtopology)
lp15@70097
   472
    have 1: "hom_induced n (nsphere n) ?TE (nsphere n) ?TE f \<circ> hom_induced n (nsphere n) ?TE (nsphere n) ?TE neg
lp15@70097
   473
           = hom_induced n (nsphere n) ?TE (nsphere n) ?TE neg \<circ> hom_induced n (nsphere n) ?TE (nsphere n) ?TE f"
lp15@70097
   474
      using neg_im fimeq cm_neg cmf
lp15@70097
   475
      apply (simp add: flip: hom_induced_compose del: hom_induced_restrict)
lp15@70097
   476
      using fneg by (auto intro: hom_induced_eq)
lp15@70097
   477
    have "(un [^]\<^bsub>?rhgn (equator n)\<^esub> a) \<otimes>\<^bsub>?rhgn (equator n)\<^esub> (up [^]\<^bsub>?rhgn (equator n)\<^esub> b)
lp15@70097
   478
        = un [^]\<^bsub>?rhgn (equator n)\<^esub> (Brouwer_degree2 (n - 1) neg * a * Brouwer_degree2 (n - 1) neg)
lp15@70097
   479
          \<otimes>\<^bsub>?rhgn (equator n)\<^esub>
lp15@70097
   480
          up [^]\<^bsub>?rhgn (equator n)\<^esub> (Brouwer_degree2 (n - 1) neg * b * Brouwer_degree2 (n - 1) neg)"
lp15@70097
   481
    proof -
lp15@70097
   482
      have "Brouwer_degree2 (n - Suc 0) neg = 1 \<or> Brouwer_degree2 (n - Suc 0) neg = - 1"
lp15@70097
   483
        using Brouwer_degree2_21 power2_eq_1_iff by blast
lp15@70097
   484
      then show ?thesis
lp15@70097
   485
        by fastforce
lp15@70097
   486
    qed
lp15@70097
   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>
lp15@70097
   488
           (up [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - 1) neg) [^]\<^bsub>?rhgn (equator n)\<^esub> b) [^]\<^bsub>?rhgn (equator n)\<^esub>
lp15@70097
   489
          Brouwer_degree2 (n - 1) neg"
lp15@70097
   490
      by (simp add: GE.int_pow_distrib GE.int_pow_pow uncarr upcarr)
lp15@70097
   491
    also have "\<dots> = ?hi_ee neg (?hi_ee f up) [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg"
lp15@70097
   492
      by (simp add: gh_een.hom_int_pow hi_un_eq_up hi_up_eq_un uncarr up_ab upcarr)
lp15@70097
   493
    finally have 2: "(un [^]\<^bsub>?rhgn (equator n)\<^esub> a) \<otimes>\<^bsub>?rhgn (equator n)\<^esub> (up [^]\<^bsub>?rhgn (equator n)\<^esub> b)
lp15@70097
   494
             = ?hi_ee neg (?hi_ee f up) [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg" .
lp15@70097
   495
    have "un = ?hi_ee neg up [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg"
lp15@70097
   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)
lp15@70097
   497
    moreover have "?hi_ee f ((?hi_ee neg up) [^]\<^bsub>?rhgn (equator n)\<^esub> (Brouwer_degree2 (n - Suc 0) neg))
lp15@70097
   498
                 = un [^]\<^bsub>?rhgn (equator n)\<^esub> a \<otimes>\<^bsub>?rhgn (equator n)\<^esub> up [^]\<^bsub>?rhgn (equator n)\<^esub> b"
lp15@70097
   499
      using 1 2 by (simp add: hom_induced_carrier gh_eef.hom_int_pow fun_eq_iff)
lp15@70097
   500
    ultimately show ?thesis
lp15@70097
   501
      by blast
lp15@70097
   502
  qed
lp15@70097
   503
  then have "?hi_ee f u = u [^]\<^bsub>?rhgn (equator n)\<^esub> (a - b)"
lp15@70097
   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)
lp15@70097
   505
  ultimately
lp15@70097
   506
  have "Brouwer_degree2 n f = a - b"
lp15@70097
   507
    using iff by blast
lp15@70097
   508
  with Bd_ab show ?thesis
lp15@70097
   509
    by simp
lp15@70097
   510
qed simp
lp15@70097
   511
lp15@70097
   512
lp15@70097
   513
subsection \<open>General Jordan-Brouwer separation theorem and invariance of dimension\<close>
lp15@70097
   514
lp15@70097
   515
proposition relative_homology_group_Euclidean_complement_step:
lp15@70097
   516
  assumes "closedin (Euclidean_space n) S"
lp15@70097
   517
  shows "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S)
lp15@70097
   518
      \<cong> relative_homology_group (p + k) (Euclidean_space (n+k)) (topspace(Euclidean_space (n+k)) - S)"
lp15@70097
   519
proof -
lp15@70097
   520
  have *: "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S)
lp15@70097
   521
           \<cong> relative_homology_group (p + 1) (Euclidean_space (Suc n)) (topspace(Euclidean_space (Suc n)) - {x \<in> S. x n = 0})"
lp15@70097
   522
    (is "?lhs \<cong> ?rhs")
lp15@70097
   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"
lp15@70097
   524
      for p n S
lp15@70097
   525
  proof -
lp15@70097
   526
    have Ssub: "S \<subseteq> topspace (Euclidean_space (Suc n))"
lp15@70097
   527
      by (meson clo closedin_def)
lp15@70097
   528
    define lo where "lo \<equiv> {x \<in> topspace(Euclidean_space (Suc n)). x n < (if x \<in> S then 0 else 1)}"
lp15@70097
   529
    define hi where "hi = {x \<in> topspace(Euclidean_space (Suc n)). x n > (if x \<in> S then 0 else -1)}"
lp15@70097
   530
    have lo_hi_Int: "lo \<inter> hi = {x \<in> topspace(Euclidean_space (Suc n)) - S. x n \<in> {-1<..<1}}"
lp15@70097
   531
      by (auto simp: hi_def lo_def)
lp15@70097
   532
    have lo_hi_Un: "lo \<union> hi = topspace(Euclidean_space (Suc n)) - {x \<in> S. x n = 0}"
lp15@70097
   533
      by (auto simp: hi_def lo_def)
lp15@70097
   534
    define ret where "ret \<equiv> \<lambda>c::real. \<lambda>x i. if i = n then c else x i"
lp15@70097
   535
    have cm_ret: "continuous_map (powertop_real UNIV) (powertop_real UNIV) (ret t)" for t
lp15@70097
   536
      by (auto simp: ret_def continuous_map_componentwise_UNIV intro: continuous_map_product_projection)
lp15@70097
   537
    let ?ST = "\<lambda>t. subtopology (Euclidean_space (Suc n)) {x. x n = t}"
lp15@70097
   538
    define squashable where
lp15@70097
   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"
lp15@70097
   540
    have squashable: "squashable t (topspace(Euclidean_space(Suc n)))" for t
lp15@70097
   541
      by (simp add: squashable_def topspace_Euclidean_space ret_def)
lp15@70097
   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
lp15@70097
   543
      by (auto simp: squashable_def)
lp15@70097
   544
    have "squashable 1 hi"
lp15@70097
   545
      by (force simp: squashable_def hi_def ret_def topspace_Euclidean_space intro: cong)
lp15@70097
   546
    have "squashable t UNIV" for t
lp15@70097
   547
      by (force simp: squashable_def hi_def ret_def topspace_Euclidean_space intro: cong)
lp15@70097
   548
    have squashable_0_lohi: "squashable 0 (lo \<inter> hi)"
lp15@70097
   549
      using Ssub
lp15@70097
   550
      by (auto simp: squashable_def hi_def lo_def ret_def topspace_Euclidean_space intro: cong)
lp15@70097
   551
    have rm_ret: "retraction_maps (subtopology (Euclidean_space (Suc n)) U)
lp15@70097
   552
                                  (subtopology (Euclidean_space (Suc n)) {x. x \<in> U \<and> x n = t})
lp15@70097
   553
                                  (ret t) id"
lp15@70097
   554
      if "squashable t U" for t U
lp15@70097
   555
      unfolding retraction_maps_def
lp15@70097
   556
    proof (intro conjI ballI)
lp15@70097
   557
      show "continuous_map (subtopology (Euclidean_space (Suc n)) U)
lp15@70097
   558
             (subtopology (Euclidean_space (Suc n)) {x \<in> U. x n = t}) (ret t)"
lp15@70097
   559
        apply (simp add: cm_ret continuous_map_in_subtopology continuous_map_from_subtopology Euclidean_space_def)
lp15@70097
   560
        using that by (fastforce simp: squashable_def ret_def)
lp15@70097
   561
    next
lp15@70097
   562
      show "continuous_map (subtopology (Euclidean_space (Suc n)) {x \<in> U. x n = t})
lp15@70097
   563
                           (subtopology (Euclidean_space (Suc n)) U) id"
lp15@70097
   564
        using continuous_map_in_subtopology by fastforce
lp15@70097
   565
      show "ret t (id x) = x"
lp15@70097
   566
        if "x \<in> topspace (subtopology (Euclidean_space (Suc n)) {x \<in> U. x n = t})" for x
lp15@70097
   567
        using that by (simp add: topspace_Euclidean_space ret_def fun_eq_iff)
lp15@70097
   568
    qed
lp15@70097
   569
    have cm_snd: "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (powertop_real UNIV) S))
lp15@70097
   570
                              euclideanreal (\<lambda>x. snd x k)" for k::nat and S
lp15@70097
   571
      using continuous_map_componentwise_UNIV continuous_map_into_fulltopology continuous_map_snd by fastforce
lp15@70097
   572
    have cm_fstsnd: "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (powertop_real UNIV) S))
lp15@70097
   573
                              euclideanreal (\<lambda>x. fst x * snd x k)" for k::nat and S
lp15@70097
   574
      by (intro continuous_intros continuous_map_into_fulltopology [OF continuous_map_fst] cm_snd)
lp15@70097
   575
    have hw_sub: "homotopic_with (\<lambda>k. k ` V \<subseteq> V) (subtopology (Euclidean_space (Suc n)) U)
lp15@70097
   576
                                 (subtopology (Euclidean_space (Suc n)) U) (ret t) id"
lp15@70097
   577
      if "squashable t U" "squashable t V" for U V t
lp15@70097
   578
      unfolding homotopic_with_def
lp15@70097
   579
    proof (intro exI conjI allI ballI)
lp15@70097
   580
      let ?h = "\<lambda>(z,x). ret ((1 - z) * t + z * x n) x"
lp15@70097
   581
      show "(\<lambda>x. ?h (u, x)) ` V \<subseteq> V" if "u \<in> {0..1}" for u
lp15@70097
   582
        using that
lp15@70097
   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)
lp15@70097
   584
      have 1: "?h ` ({0..1} \<times> ({x. \<forall>i\<ge>Suc n. x i = 0} \<inter> U)) \<subseteq> U"
lp15@70097
   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)
lp15@70097
   586
      show "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (Euclidean_space (Suc n)) U))
lp15@70097
   587
                           (subtopology (Euclidean_space (Suc n)) U) ?h"
lp15@70097
   588
        apply (simp add: continuous_map_in_subtopology Euclidean_space_def subtopology_subtopology 1)
lp15@70097
   589
        apply (auto simp: case_prod_unfold ret_def continuous_map_componentwise_UNIV)
lp15@70097
   590
         apply (intro continuous_map_into_fulltopology [OF continuous_map_fst] cm_snd continuous_intros)
lp15@70097
   591
        by (auto simp: cm_snd)
lp15@70097
   592
    qed (auto simp: ret_def)
lp15@70097
   593
    have cs_hi: "contractible_space(subtopology (Euclidean_space(Suc n)) hi)"
lp15@70097
   594
    proof -
lp15@70097
   595
      have "homotopic_with (\<lambda>x. True) (?ST 1) (?ST 1) id (\<lambda>x. (\<lambda>i. if i = n then 1 else 0))"
lp15@70097
   596
        apply (subst homotopic_with_sym)
lp15@70097
   597
        apply (simp add: homotopic_with)
lp15@70097
   598
        apply (rule_tac x="(\<lambda>(z,x) i. if i=n then 1 else z * x i)" in exI)
lp15@70097
   599
        apply (auto simp: Euclidean_space_def subtopology_subtopology continuous_map_in_subtopology case_prod_unfold continuous_map_componentwise_UNIV cm_fstsnd)
lp15@70097
   600
        done
lp15@70097
   601
      then have "contractible_space (?ST 1)"
lp15@70097
   602
        unfolding contractible_space_def by metis
lp15@70097
   603
      moreover have "?thesis = contractible_space (?ST 1)"
lp15@70097
   604
      proof (intro deformation_retract_imp_homotopy_equivalent_space homotopy_equivalent_space_contractibility)
lp15@70097
   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}"
lp15@70097
   606
          by (auto simp: hi_def topspace_Euclidean_space)
lp15@70097
   607
        then have eq: "subtopology (Euclidean_space (Suc n)) {x. x \<in> hi \<and> x n = 1} = ?ST 1"
lp15@70097
   608
          by (simp add: Euclidean_space_def subtopology_subtopology)
lp15@70097
   609
        show "homotopic_with (\<lambda>x. True) (subtopology (Euclidean_space (Suc n)) hi) (subtopology (Euclidean_space (Suc n)) hi) (ret 1) id"
lp15@70097
   610
          using hw_sub [OF \<open>squashable 1 hi\<close> \<open>squashable 1 UNIV\<close>] eq by simp
lp15@70097
   611
        show "retraction_maps (subtopology (Euclidean_space (Suc n)) hi) (?ST 1) (ret 1) id"
lp15@70097
   612
          using rm_ret [OF \<open>squashable 1 hi\<close>] eq by simp
lp15@70097
   613
      qed
lp15@70097
   614
      ultimately show ?thesis by metis
lp15@70097
   615
    qed
lp15@70097
   616
    have "?lhs \<cong> relative_homology_group p (Euclidean_space (Suc n)) (lo \<inter> hi)"
lp15@70097
   617
    proof (rule group.iso_sym [OF _ deformation_retract_imp_isomorphic_relative_homology_groups])
lp15@70097
   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)}"
lp15@70097
   619
        by auto (metis le_less_Suc_eq not_le)
lp15@70097
   620
      then have "?ST 0 = Euclidean_space n"
lp15@70097
   621
        by (simp add: Euclidean_space_def subtopology_subtopology)
lp15@70097
   622
      then show "retraction_maps (Euclidean_space (Suc n)) (Euclidean_space n) (ret 0) id"
lp15@70097
   623
        using rm_ret [OF \<open>squashable 0 UNIV\<close>] by auto
lp15@70097
   624
      then have "ret 0 x \<in> topspace (Euclidean_space n)"
lp15@70097
   625
        if "x \<in> topspace (Euclidean_space (Suc n))" "-1 < x n" "x n < 1" for x
lp15@70097
   626
        using that by (simp add: continuous_map_def retraction_maps_def)
lp15@70097
   627
      then show "(ret 0) ` (lo \<inter> hi) \<subseteq> topspace (Euclidean_space n) - S"
lp15@70097
   628
        by (auto simp: local.cong ret_def hi_def lo_def)
lp15@70097
   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"
lp15@70097
   630
        using hw_sub [OF squashable squashable_0_lohi] by simp
lp15@70097
   631
    qed (auto simp: lo_def hi_def Euclidean_space_def)
lp15@70097
   632
    also have "\<dots> \<cong> relative_homology_group p (subtopology (Euclidean_space (Suc n)) hi) (lo \<inter> hi)"
lp15@70097
   633
    proof (rule group.iso_sym [OF _ isomorphic_relative_homology_groups_inclusion_contractible])
lp15@70097
   634
      show "contractible_space (subtopology (Euclidean_space (Suc n)) hi)"
lp15@70097
   635
        by (simp add: cs_hi)
lp15@70097
   636
      show "topspace (Euclidean_space (Suc n)) \<inter> hi \<noteq> {}"
lp15@70097
   637
        apply (simp add: hi_def topspace_Euclidean_space set_eq_iff)
lp15@70097
   638
        apply (rule_tac x="\<lambda>i. if i = n then 1 else 0" in exI, auto)
lp15@70097
   639
        done
lp15@70097
   640
    qed auto
lp15@70097
   641
    also have "\<dots> \<cong> relative_homology_group p (subtopology (Euclidean_space (Suc n)) (lo \<union> hi)) lo"
lp15@70097
   642
    proof -
lp15@70097
   643
      have oo: "openin (Euclidean_space (Suc n)) {x \<in> topspace (Euclidean_space (Suc n)). x n \<in> A}"
lp15@70097
   644
        if "open A" for A
lp15@70097
   645
      proof (rule openin_continuous_map_preimage)
lp15@70097
   646
        show "continuous_map (Euclidean_space (Suc n)) euclideanreal (\<lambda>x. x n)"
lp15@70097
   647
        proof -
lp15@70097
   648
          have "\<forall>n f. continuous_map (product_topology f UNIV) (f (n::nat)) (\<lambda>f. f n::real)"
lp15@70097
   649
            by (simp add: continuous_map_product_projection)
lp15@70097
   650
          then show ?thesis
lp15@70097
   651
            using Euclidean_space_def continuous_map_from_subtopology
lp15@70097
   652
            by (metis (mono_tags))
lp15@70097
   653
        qed
lp15@70097
   654
      qed (auto intro: that)
lp15@70097
   655
      have "openin (Euclidean_space(Suc n)) lo"
lp15@70097
   656
        apply (simp add: openin_subopen [of _ lo])
lp15@70097
   657
        apply (simp add: lo_def, safe)
lp15@70097
   658
         apply (force intro: oo [of "lessThan 0", simplified] open_Collect_less)
lp15@70097
   659
        apply (rule_tac x="{x \<in> topspace(Euclidean_space(Suc n)). x n < 1}
lp15@70097
   660
                            \<inter> (topspace(Euclidean_space(Suc n)) - S)" in exI)
lp15@70097
   661
        using clo apply (force intro: oo [of "lessThan 1", simplified] open_Collect_less)
lp15@70097
   662
        done
lp15@70097
   663
      moreover have "openin (Euclidean_space(Suc n)) hi"
lp15@70097
   664
        apply (simp add: openin_subopen [of _ hi])
lp15@70097
   665
        apply (simp add: hi_def, safe)
lp15@70097
   666
         apply (force intro: oo [of "greaterThan 0", simplified] open_Collect_less)
lp15@70097
   667
        apply (rule_tac x="{x \<in> topspace(Euclidean_space(Suc n)). x n > -1}
lp15@70097
   668
                                \<inter> (topspace(Euclidean_space(Suc n)) - S)" in exI)
lp15@70097
   669
        using clo apply (force intro: oo [of "greaterThan (-1)", simplified] open_Collect_less)
lp15@70097
   670
        done
lp15@70097
   671
      ultimately
lp15@70097
   672
      have *: "subtopology (Euclidean_space (Suc n)) (lo \<union> hi) closure_of
lp15@70097
   673
                   (topspace (subtopology (Euclidean_space (Suc n)) (lo \<union> hi)) - hi)
lp15@70097
   674
                   \<subseteq> subtopology (Euclidean_space (Suc n)) (lo \<union> hi) interior_of lo"
lp15@70097
   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)
lp15@70097
   676
      have eq: "((lo \<union> hi) \<inter> (lo \<union> hi - (topspace (Euclidean_space (Suc n)) \<inter> (lo \<union> hi) - hi))) = hi"
lp15@70097
   677
        "(lo - (topspace (Euclidean_space (Suc n)) \<inter> (lo \<union> hi) - hi)) = lo \<inter> hi"
lp15@70097
   678
        by (auto simp: lo_def hi_def Euclidean_space_def)
lp15@70097
   679
      show ?thesis
lp15@70097
   680
        using homology_excision_axiom [OF *, of "lo \<union> hi" p]
lp15@70097
   681
        by (force simp: subtopology_subtopology eq is_iso_def)
lp15@70097
   682
    qed
lp15@70097
   683
    also have "\<dots> \<cong> relative_homology_group (p + 1 - 1) (subtopology (Euclidean_space (Suc n)) (lo \<union> hi)) lo"
lp15@70097
   684
      by simp
lp15@70097
   685
    also have "\<dots> \<cong> relative_homology_group (p + 1) (Euclidean_space (Suc n)) (lo \<union> hi)"
lp15@70097
   686
    proof (rule group.iso_sym [OF _ isomorphic_relative_homology_groups_relboundary_contractible])
lp15@70097
   687
      have proj: "continuous_map (powertop_real UNIV) euclideanreal (\<lambda>f. f n)"
lp15@70097
   688
        by (metis UNIV_I continuous_map_product_projection)
lp15@70097
   689
      have hilo: "\<And>x. x \<in> hi \<Longrightarrow> (\<lambda>i. if i = n then - x i else x i) \<in> lo"
lp15@70097
   690
                 "\<And>x. x \<in> lo \<Longrightarrow> (\<lambda>i. if i = n then - x i else x i) \<in> hi"
lp15@70097
   691
        using local.cong
lp15@70097
   692
        by (auto simp: hi_def lo_def topspace_Euclidean_space split: if_split_asm)
lp15@70097
   693
      have "subtopology (Euclidean_space (Suc n)) hi homeomorphic_space subtopology (Euclidean_space (Suc n)) lo"
lp15@70097
   694
        unfolding homeomorphic_space_def
lp15@70097
   695
        apply (rule_tac x="\<lambda>x i. if i = n then -(x i) else x i" in exI)+
lp15@70097
   696
        using proj
lp15@70097
   697
        apply (auto simp: homeomorphic_maps_def Euclidean_space_def continuous_map_in_subtopology
lp15@70097
   698
                          hilo continuous_map_componentwise_UNIV continuous_map_from_subtopology continuous_map_minus
lp15@70097
   699
                    intro: continuous_map_from_subtopology continuous_map_product_projection)
lp15@70097
   700
        done
lp15@70097
   701
      then have "contractible_space(subtopology (Euclidean_space(Suc n)) hi)
lp15@70097
   702
             \<longleftrightarrow> contractible_space (subtopology (Euclidean_space (Suc n)) lo)"
lp15@70097
   703
        by (rule homeomorphic_space_contractibility)
lp15@70097
   704
      then show "contractible_space (subtopology (Euclidean_space (Suc n)) lo)"
lp15@70097
   705
        using cs_hi by auto
lp15@70097
   706
      show "topspace (Euclidean_space (Suc n)) \<inter> lo \<noteq> {}"
lp15@70097
   707
        apply (simp add: lo_def Euclidean_space_def set_eq_iff)
lp15@70097
   708
        apply (rule_tac x="\<lambda>i. if i = n then -1 else 0" in exI, auto)
lp15@70097
   709
        done
lp15@70097
   710
    qed auto
lp15@70097
   711
    also have "\<dots> \<cong> ?rhs"
lp15@70097
   712
      by (simp flip: lo_hi_Un)
lp15@70097
   713
    finally show ?thesis .
lp15@70097
   714
  qed
lp15@70097
   715
  show ?thesis
lp15@70097
   716
  proof (induction k)
lp15@70097
   717
    case (Suc m)
lp15@70097
   718
    with assms obtain T where cloT: "closedin (powertop_real UNIV) T"
lp15@70097
   719
                         and SeqT: "S = T \<inter> {x. \<forall>i\<ge>n. x i = 0}"
lp15@70097
   720
      by (auto simp: Euclidean_space_def closedin_subtopology)
lp15@70097
   721
    then have "closedin (Euclidean_space (m + n)) S"
lp15@70097
   722
      apply (simp add: Euclidean_space_def closedin_subtopology)
lp15@70097
   723
      apply (rule_tac x="T \<inter> topspace(Euclidean_space n)" in exI)
lp15@70097
   724
      using closedin_Euclidean_space topspace_Euclidean_space by force
lp15@70097
   725
    moreover have "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - S)
lp15@70097
   726
                \<cong> relative_homology_group (p + 1) (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - S)"
lp15@70097
   727
      if "closedin (Euclidean_space n) S" for p n
lp15@70097
   728
    proof -
lp15@70097
   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}"
lp15@70097
   730
      have Ssub_n: "S \<subseteq> topspace (Euclidean_space n)"
lp15@70097
   731
        by (meson that closedin_def)
lp15@70097
   732
      have "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S')
lp15@70097
   733
           \<cong> relative_homology_group (p + 1) (Euclidean_space (Suc n)) (topspace(Euclidean_space (Suc n)) - {x \<in> S'. x n = 0})"
lp15@70097
   734
      proof (rule *)
lp15@70097
   735
        have cm: "continuous_map (powertop_real UNIV) euclideanreal (\<lambda>f. f u)" for u
lp15@70097
   736
          by (metis UNIV_I continuous_map_product_projection)
lp15@70097
   737
        have "continuous_map (subtopology (powertop_real UNIV) {x. \<forall>i>n. x i = 0}) euclideanreal
lp15@70097
   738
                (\<lambda>x. if k \<le> n then x k else 0)" for k
lp15@70097
   739
          by (simp add: continuous_map_from_subtopology [OF cm])
lp15@70097
   740
        moreover have "\<forall>i\<ge>n. (if i < n then x i else 0) = 0"
lp15@70097
   741
          if "x \<in> topspace (subtopology (powertop_real UNIV) {x. \<forall>i>n. x i = 0})" for x
lp15@70097
   742
          using that by simp
lp15@70097
   743
        ultimately have "continuous_map (Euclidean_space (Suc n)) (Euclidean_space n) (\<lambda>x i. if i < n then x i else 0)"
lp15@70097
   744
          by (simp add: Euclidean_space_def continuous_map_in_subtopology continuous_map_componentwise_UNIV
lp15@70097
   745
                        continuous_map_from_subtopology [OF cm] image_subset_iff)
lp15@70097
   746
        then show "closedin (Euclidean_space (Suc n)) S'"
lp15@70097
   747
          unfolding S'_def using that by (rule closedin_continuous_map_preimage)
lp15@70097
   748
      next
lp15@70097
   749
        fix x y
lp15@70097
   750
        assume xy: "\<And>i. i \<noteq> n \<Longrightarrow> x i = y i" "x \<in> S'"
lp15@70097
   751
        then have "(\<lambda>i. if i < n then x i else 0) = (\<lambda>i. if i < n then y i else 0)"
lp15@70097
   752
          by (simp add: S'_def Euclidean_space_def fun_eq_iff)
lp15@70097
   753
        with xy show "y \<in> S'"
lp15@70097
   754
          by (simp add: S'_def Euclidean_space_def)
lp15@70097
   755
      qed
lp15@70097
   756
      moreover
lp15@70097
   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
lp15@70097
   758
        using that by auto
lp15@70097
   759
      then have "topspace (Euclidean_space n) - S' = topspace (Euclidean_space n) - S"
lp15@70097
   760
        by (simp add: S'_def Euclidean_space_def set_eq_iff cong: conj_cong)
lp15@70097
   761
      moreover
lp15@70097
   762
      have "topspace (Euclidean_space (Suc n)) - {x \<in> S'. x n = 0} = topspace (Euclidean_space (Suc n)) - S"
lp15@70097
   763
        using Ssub_n
lp15@70097
   764
        apply (auto simp: S'_def subset_iff Euclidean_space_def set_eq_iff abs_eq  cong: conj_cong)
lp15@70097
   765
        by (metis abs_eq le_antisym not_less_eq_eq)
lp15@70097
   766
      ultimately show ?thesis
lp15@70097
   767
        by simp
lp15@70097
   768
    qed
lp15@70097
   769
    ultimately have "relative_homology_group (p + m)(Euclidean_space (m + n))(topspace (Euclidean_space (m + n)) - S)
lp15@70097
   770
            \<cong> relative_homology_group (p + m + 1) (Euclidean_space (Suc (m + n))) (topspace (Euclidean_space (Suc (m + n))) - S)"
lp15@70097
   771
      by (metis \<open>closedin (Euclidean_space (m + n)) S\<close>)
lp15@70097
   772
    then show ?case
lp15@70097
   773
      using Suc.IH iso_trans by (force simp: algebra_simps)
lp15@70097
   774
  qed (simp add: iso_refl)
lp15@70097
   775
qed
lp15@70097
   776
lp15@70097
   777
lemma iso_Euclidean_complements_lemma1:
lp15@70097
   778
  assumes S: "closedin (Euclidean_space m) S" and cmf: "continuous_map(subtopology (Euclidean_space m) S) (Euclidean_space n) f"
lp15@70097
   779
  obtains g where "continuous_map (Euclidean_space m) (Euclidean_space n) g"
lp15@70097
   780
                  "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
lp15@70097
   781
proof -
lp15@70097
   782
  have cont: "continuous_on (topspace (Euclidean_space m) \<inter> S) (\<lambda>x. f x i)" for i
lp15@70097
   783
    by (metis (no_types) continuous_on_product_then_coordinatewise
lp15@70097
   784
            cm_Euclidean_space_iff_continuous_on cmf topspace_subtopology)
lp15@70097
   785
  have "f ` (topspace (Euclidean_space m) \<inter> S) \<subseteq> topspace (Euclidean_space n)"
lp15@70097
   786
    using cmf continuous_map_image_subset_topspace by fastforce
lp15@70097
   787
  then
lp15@70097
   788
  have "\<exists>g. continuous_on (topspace (Euclidean_space m)) g \<and> (\<forall>x \<in> S. g x = f x i)" for i
lp15@70097
   789
    using S Tietze_unbounded [OF cont [of i]]
lp15@70097
   790
    by (metis closedin_Euclidean_space_iff closedin_closed_Int topspace_subtopology topspace_subtopology_subset)
lp15@70097
   791
  then obtain g where cmg: "\<And>i. continuous_map (Euclidean_space m) euclideanreal (g i)"
lp15@70097
   792
    and gf: "\<And>i x. x \<in> S \<Longrightarrow> g i x = f x i"
lp15@70097
   793
    unfolding continuous_map_Euclidean_space_iff by metis
lp15@70097
   794
  let ?GG = "\<lambda>x i. if i < n then g i x else 0"
lp15@70097
   795
  show thesis
lp15@70097
   796
  proof
lp15@70097
   797
    show "continuous_map (Euclidean_space m) (Euclidean_space n) ?GG"
lp15@70097
   798
      unfolding Euclidean_space_def [of n]
lp15@70097
   799
      by (auto simp: continuous_map_in_subtopology continuous_map_componentwise cmg)
lp15@70097
   800
    show "?GG x = f x" if "x \<in> S" for x
lp15@70097
   801
    proof -
lp15@70097
   802
      have "S \<subseteq> topspace (Euclidean_space m)"
lp15@70097
   803
        by (meson S closedin_def)
lp15@70097
   804
      then have "f x \<in> topspace (Euclidean_space n)"
lp15@70097
   805
        using cmf that unfolding continuous_map_def topspace_subtopology by blast
lp15@70097
   806
      then show ?thesis
lp15@70097
   807
        by (force simp: topspace_Euclidean_space gf that)
lp15@70097
   808
    qed
lp15@70097
   809
  qed
lp15@70097
   810
qed
lp15@70097
   811
lp15@70097
   812
lp15@70097
   813
lemma iso_Euclidean_complements_lemma2:
lp15@70097
   814
  assumes S: "closedin (Euclidean_space m) S"
lp15@70097
   815
      and T: "closedin (Euclidean_space n) T"
lp15@70097
   816
      and hom: "homeomorphic_map (subtopology (Euclidean_space m) S) (subtopology (Euclidean_space n) T) f"
lp15@70097
   817
  obtains g where "homeomorphic_map (prod_topology (Euclidean_space m) (Euclidean_space n))
lp15@70097
   818
                                    (prod_topology (Euclidean_space n) (Euclidean_space m)) g"
lp15@70097
   819
                  "\<And>x. x \<in> S \<Longrightarrow> g(x,(\<lambda>i. 0)) = (f x,(\<lambda>i. 0))"
lp15@70097
   820
proof -
lp15@70097
   821
  obtain g where cmf: "continuous_map (subtopology (Euclidean_space m) S) (subtopology (Euclidean_space n) T) f"
lp15@70097
   822
           and cmg: "continuous_map (subtopology (Euclidean_space n) T) (subtopology (Euclidean_space m) S) g"
lp15@70097
   823
           and gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
lp15@70097
   824
           and fg: "\<And>y. y \<in> T \<Longrightarrow> f (g y) = y"
lp15@70097
   825
    using hom S T closedin_subset unfolding homeomorphic_map_maps homeomorphic_maps_def
lp15@70097
   826
    by fastforce
lp15@70097
   827
  obtain f' where cmf': "continuous_map (Euclidean_space m) (Euclidean_space n) f'"
lp15@70097
   828
             and f'f: "\<And>x. x \<in> S \<Longrightarrow> f' x = f x"
lp15@70097
   829
    using iso_Euclidean_complements_lemma1 S cmf continuous_map_into_fulltopology by metis
lp15@70097
   830
  obtain g' where cmg': "continuous_map (Euclidean_space n) (Euclidean_space m) g'"
lp15@70097
   831
             and g'g: "\<And>x. x \<in> T \<Longrightarrow> g' x = g x"
lp15@70097
   832
    using iso_Euclidean_complements_lemma1 T cmg continuous_map_into_fulltopology by metis
lp15@70097
   833
  define p  where "p \<equiv> \<lambda>(x,y). (x,(\<lambda>i. y i + f' x i))"
lp15@70097
   834
  define p' where "p' \<equiv> \<lambda>(x,y). (x,(\<lambda>i. y i - f' x i))"
lp15@70097
   835
  define q  where "q \<equiv> \<lambda>(x,y). (x,(\<lambda>i. y i + g' x i))"
lp15@70097
   836
  define q' where "q' \<equiv> \<lambda>(x,y). (x,(\<lambda>i. y i - g' x i))"
lp15@70097
   837
  have "homeomorphic_maps (prod_topology (Euclidean_space m) (Euclidean_space n))
lp15@70097
   838
                          (prod_topology (Euclidean_space m) (Euclidean_space n))
lp15@70097
   839
                          p p'"
lp15@70097
   840
       "homeomorphic_maps (prod_topology (Euclidean_space n) (Euclidean_space m))
lp15@70097
   841
                          (prod_topology (Euclidean_space n) (Euclidean_space m))
lp15@70097
   842
                          q q'"
lp15@70097
   843
       "homeomorphic_maps (prod_topology (Euclidean_space m) (Euclidean_space n))
lp15@70097
   844
                          (prod_topology (Euclidean_space n) (Euclidean_space m)) (\<lambda>(x,y). (y,x)) (\<lambda>(x,y). (y,x))"
lp15@70097
   845
    apply (simp_all add: p_def p'_def q_def q'_def homeomorphic_maps_def continuous_map_pairwise)
lp15@70097
   846
    apply (force simp: case_prod_unfold continuous_map_of_fst [unfolded o_def] cmf' cmg' intro: continuous_intros)+
lp15@70097
   847
    done
lp15@70097
   848
  then have "homeomorphic_maps (prod_topology (Euclidean_space m) (Euclidean_space n))
lp15@70097
   849
                          (prod_topology (Euclidean_space n) (Euclidean_space m))
lp15@70097
   850
                          (q' \<circ> (\<lambda>(x,y). (y,x)) \<circ> p) (p' \<circ> ((\<lambda>(x,y). (y,x)) \<circ> q))"
lp15@70097
   851
    using homeomorphic_maps_compose homeomorphic_maps_sym by (metis (no_types, lifting))
lp15@70097
   852
  moreover
lp15@70097
   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)"
lp15@70097
   854
    apply (simp add: q'_def p_def f'f)
lp15@70097
   855
    apply (simp add: fun_eq_iff)
lp15@70097
   856
    by (metis S T closedin_subset g'g gf hom homeomorphic_imp_surjective_map image_eqI topspace_subtopology_subset)
lp15@70097
   857
  ultimately
lp15@70097
   858
  show thesis
lp15@70097
   859
    using homeomorphic_map_maps that by blast
lp15@70097
   860
qed
lp15@70097
   861
lp15@70097
   862
lp15@70097
   863
proposition isomorphic_relative_homology_groups_Euclidean_complements:
lp15@70097
   864
  assumes S: "closedin (Euclidean_space n) S" and T: "closedin (Euclidean_space n) T"
lp15@70097
   865
   and hom: "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)"
lp15@70097
   866
   shows "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S)
lp15@70097
   867
          \<cong> relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - T)"
lp15@70097
   868
proof -
lp15@70097
   869
  have subST: "S \<subseteq> topspace(Euclidean_space n)" "T \<subseteq> topspace(Euclidean_space n)"
lp15@70097
   870
    by (meson S T closedin_def)+
lp15@70097
   871
  have "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - S)
lp15@70097
   872
        \<cong> relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - S)"
lp15@70097
   873
    using relative_homology_group_Euclidean_complement_step [OF S] by blast
lp15@70097
   874
  moreover have "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - T)
lp15@70097
   875
        \<cong> relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - T)"
lp15@70097
   876
    using relative_homology_group_Euclidean_complement_step [OF T] by blast
lp15@70097
   877
  moreover have "relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - S)
lp15@70097
   878
               \<cong> relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - T)"
lp15@70097
   879
  proof -
lp15@70097
   880
    obtain f where f: "homeomorphic_map (subtopology (Euclidean_space n) S)
lp15@70097
   881
                                        (subtopology (Euclidean_space n) T) f"
lp15@70097
   882
      using hom unfolding homeomorphic_space by blast
lp15@70097
   883
    obtain g where g: "homeomorphic_map (prod_topology (Euclidean_space n) (Euclidean_space n))
lp15@70097
   884
                                        (prod_topology (Euclidean_space n) (Euclidean_space n)) g"
lp15@70097
   885
              and gf: "\<And>x. x \<in> S \<Longrightarrow> g(x,(\<lambda>i. 0)) = (f x,(\<lambda>i. 0))"
lp15@70097
   886
      using S T f iso_Euclidean_complements_lemma2 by blast
lp15@70097
   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))"
lp15@70097
   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)"
lp15@70097
   889
    have hk: "homeomorphic_maps (Euclidean_space(2 * n)) (prod_topology (Euclidean_space n) (Euclidean_space n)) h k"
lp15@70097
   890
      unfolding homeomorphic_maps_def
lp15@70097
   891
    proof safe
lp15@70097
   892
      show "continuous_map (Euclidean_space (2 * n))
lp15@70097
   893
                           (prod_topology (Euclidean_space n) (Euclidean_space n)) h"
lp15@70097
   894
        apply (simp add: h_def continuous_map_pairwise o_def continuous_map_componentwise_Euclidean_space)
lp15@70097
   895
        unfolding Euclidean_space_def
lp15@70097
   896
        by (metis (mono_tags) UNIV_I continuous_map_from_subtopology continuous_map_product_projection)
lp15@70097
   897
      have "continuous_map (prod_topology (Euclidean_space n) (Euclidean_space n)) euclideanreal (\<lambda>p. fst p i)" for i
lp15@70097
   898
        using Euclidean_space_def continuous_map_into_fulltopology continuous_map_fst by fastforce
lp15@70097
   899
      moreover
lp15@70097
   900
      have "continuous_map (prod_topology (Euclidean_space n) (Euclidean_space n)) euclideanreal (\<lambda>p. snd p (i - n))" for i
lp15@70097
   901
        using Euclidean_space_def continuous_map_into_fulltopology continuous_map_snd by fastforce
lp15@70097
   902
      ultimately
lp15@70097
   903
      show "continuous_map (prod_topology (Euclidean_space n) (Euclidean_space n))
lp15@70097
   904
                           (Euclidean_space (2 * n)) k"
lp15@70097
   905
        by (simp add: k_def continuous_map_pairwise o_def continuous_map_componentwise_Euclidean_space case_prod_unfold)
lp15@70097
   906
    qed (auto simp: k_def h_def fun_eq_iff topspace_Euclidean_space)
lp15@70097
   907
    define kgh where "kgh \<equiv> k \<circ> g \<circ> h"
lp15@70097
   908
    let ?i = "hom_induced (p + n) (Euclidean_space(2 * n)) (topspace(Euclidean_space(2 * n)) - S)
lp15@70097
   909
                                 (Euclidean_space(2 * n)) (topspace(Euclidean_space(2 * n)) - T) kgh"
lp15@70097
   910
    have "?i \<in> iso (relative_homology_group (p + int n) (Euclidean_space (2 * n))
lp15@70097
   911
                    (topspace (Euclidean_space (2 * n)) - S))
lp15@70097
   912
                   (relative_homology_group (p + int n) (Euclidean_space (2 * n))
lp15@70097
   913
                    (topspace (Euclidean_space (2 * n)) - T))"
lp15@70097
   914
    proof (rule homeomorphic_map_relative_homology_iso)
lp15@70097
   915
      show hm: "homeomorphic_map (Euclidean_space (2 * n)) (Euclidean_space (2 * n)) kgh"
lp15@70097
   916
        unfolding kgh_def by (meson hk g homeomorphic_map_maps homeomorphic_maps_compose homeomorphic_maps_sym)
lp15@70097
   917
      have Teq: "T = f ` S"
lp15@70097
   918
        using f homeomorphic_imp_surjective_map subST(1) subST(2) topspace_subtopology_subset by blast
lp15@70097
   919
      have khf: "\<And>x. x \<in> S \<Longrightarrow> k(h(f x)) = f x"
lp15@70097
   920
        by (metis (no_types, lifting) Teq hk homeomorphic_maps_def image_subset_iff le_add1 mult_2 subST(2) subsetD subset_Euclidean_space)
lp15@70097
   921
      have gh: "g(h x) = h(f x)" if "x \<in> S" for x
lp15@70097
   922
      proof -
lp15@70097
   923
        have [simp]: "(\<lambda>i. if i < n then x i else 0) = x"
lp15@70097
   924
          using subST(1) that topspace_Euclidean_space by (auto simp: fun_eq_iff)
lp15@70097
   925
        have "f x \<in> topspace(Euclidean_space n)"
lp15@70097
   926
          using Teq subST(2) that by blast
lp15@70097
   927
        moreover have "(\<lambda>j. if j < n then x (n + j) else 0) = (\<lambda>j. 0::real)"
lp15@70097
   928
          using Euclidean_space_def subST(1) that by force
lp15@70097
   929
        ultimately show ?thesis
lp15@70097
   930
          by (simp add: topspace_Euclidean_space h_def gf \<open>x \<in> S\<close> fun_eq_iff)
lp15@70097
   931
      qed
lp15@70097
   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
lp15@70097
   933
        unfolding inj_on_def set_eq_iff by blast
lp15@70097
   934
      show "kgh ` (topspace (Euclidean_space (2 * n)) - S) = topspace (Euclidean_space (2 * n)) - T"
lp15@70097
   935
      proof (rule *)
lp15@70097
   936
        show "kgh ` topspace (Euclidean_space (2 * n)) = topspace (Euclidean_space (2 * n))"
lp15@70097
   937
          by (simp add: hm homeomorphic_imp_surjective_map)
lp15@70097
   938
        show "inj_on kgh (topspace (Euclidean_space (2 * n)))"
lp15@70097
   939
          using hm homeomorphic_map_def by auto
lp15@70097
   940
        show "kgh ` S = T"
lp15@70097
   941
          by (simp add: Teq kgh_def gh khf)
lp15@70097
   942
      qed (use subST topspace_Euclidean_space in \<open>fastforce+\<close>)
lp15@70097
   943
    qed auto
lp15@70097
   944
    then show ?thesis
lp15@70097
   945
      by (simp add: is_isoI mult_2)
lp15@70097
   946
  qed
lp15@70097
   947
  ultimately show ?thesis
lp15@70097
   948
    by (meson group.iso_sym iso_trans group_relative_homology_group)
lp15@70097
   949
qed
lp15@70097
   950
lp15@70097
   951
lemma lemma_iod:
lp15@70097
   952
  assumes "S \<subseteq> T" "S \<noteq> {}" and Tsub: "T \<subseteq> topspace(Euclidean_space n)"
lp15@70097
   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"
lp15@70097
   954
    shows "path_connectedin (Euclidean_space n) T"
lp15@70097
   955
proof -
lp15@70097
   956
  obtain a where "a \<in> S"
lp15@70097
   957
    using assms by blast
lp15@70097
   958
  have "path_component_of (subtopology (Euclidean_space n) T) a b" if "b \<in> T" for b
lp15@70097
   959
    unfolding path_component_of_def
lp15@70097
   960
  proof (intro exI conjI)
lp15@70097
   961
    have [simp]: "\<forall>i\<ge>n. a i = 0"
lp15@70097
   962
      using Tsub \<open>a \<in> S\<close> assms(1) topspace_Euclidean_space by auto
lp15@70097
   963
    have [simp]: "\<forall>i\<ge>n. b i = 0"
lp15@70097
   964
      using Tsub that topspace_Euclidean_space by auto
lp15@70097
   965
    have inT: "(\<lambda>i. (1 - x) * a i + x * b i) \<in> T" if "0 \<le> x" "x \<le> 1" for x
lp15@70097
   966
    proof (cases "x = 0 \<or> x = 1")
lp15@70097
   967
      case True
lp15@70097
   968
      with \<open>a \<in> S\<close> \<open>b \<in> T\<close> \<open>S \<subseteq> T\<close> show ?thesis
lp15@70097
   969
        by force
lp15@70097
   970
    next
lp15@70097
   971
      case False
lp15@70097
   972
      then show ?thesis
lp15@70097
   973
        using subsetD [OF \<open>S \<subseteq> T\<close> S] \<open>a \<in> S\<close> \<open>b \<in> T\<close> that by auto
lp15@70097
   974
    qed
lp15@70097
   975
    have "continuous_on {0..1} (\<lambda>x. (1 - x) * a k + x * b k)" for k
lp15@70097
   976
      by (intro continuous_intros)
lp15@70097
   977
    then show "pathin (subtopology (Euclidean_space n) T) (\<lambda>t i. (1 - t) * a i + t * b i)"
lp15@70097
   978
      apply (simp add: Euclidean_space_def subtopology_subtopology pathin_subtopology)
lp15@70097
   979
      apply (simp add: pathin_def continuous_map_componentwise_UNIV inT)
lp15@70097
   980
      done
lp15@70097
   981
  qed auto
lp15@70097
   982
  then have "path_connected_space (subtopology (Euclidean_space n) T)"
lp15@70097
   983
    by (metis Tsub path_component_of_equiv path_connected_space_iff_path_component topspace_subtopology_subset)
lp15@70097
   984
  then show ?thesis
lp15@70097
   985
    by (simp add: Tsub path_connectedin_def)
lp15@70097
   986
qed
lp15@70097
   987
lp15@70097
   988
lp15@70097
   989
lemma invariance_of_dimension_closedin_Euclidean_space:
lp15@70097
   990
  assumes "closedin (Euclidean_space n) S"
lp15@70097
   991
  shows "subtopology (Euclidean_space n) S homeomorphic_space Euclidean_space n
lp15@70097
   992
         \<longleftrightarrow> S = topspace(Euclidean_space n)"
lp15@70097
   993
         (is "?lhs = ?rhs")
lp15@70097
   994
proof
lp15@70097
   995
  assume L: ?lhs
lp15@70097
   996
  have Ssub: "S \<subseteq> topspace (Euclidean_space n)"
lp15@70097
   997
    by (meson assms closedin_def)
lp15@70097
   998
  moreover have False if "a \<notin> S" and "a \<in> topspace (Euclidean_space n)" for a
lp15@70097
   999
  proof -
lp15@70097
  1000
    have cl_n: "closedin (Euclidean_space (Suc n)) (topspace(Euclidean_space n))"
lp15@70097
  1001
      using Euclidean_space_def closedin_Euclidean_space closedin_subtopology by fastforce
lp15@70097
  1002
    then have sub: "subtopology (Euclidean_space(Suc n)) (topspace(Euclidean_space n)) = Euclidean_space n"
lp15@70097
  1003
      by (metis (no_types, lifting) Euclidean_space_def closedin_subset subtopology_subtopology topspace_Euclidean_space topspace_subtopology topspace_subtopology_subset)
lp15@70097
  1004
    then have cl_S: "closedin (Euclidean_space(Suc n)) S"
lp15@70097
  1005
      using cl_n assms closedin_closed_subtopology by fastforce
lp15@70097
  1006
    have sub_SucS: "subtopology (Euclidean_space (Suc n)) S = subtopology (Euclidean_space n) S"
lp15@70097
  1007
      by (metis Ssub sub subtopology_subtopology topspace_subtopology topspace_subtopology_subset)
lp15@70097
  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}"
lp15@70097
  1009
    proof safe
lp15@70097
  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
lp15@70097
  1011
        by (metis that le_antisym not_less_eq_eq)
lp15@70097
  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
lp15@70097
  1013
        by (rule_tac x="(\<lambda>i. 0)(n:= a)" in exI) (force simp: that)
lp15@70097
  1014
    qed
lp15@70097
  1015
    have "homology_group 0 (subtopology (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - S))
lp15@70097
  1016
          \<cong> homology_group 0 (subtopology (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n)))"
lp15@70097
  1017
    proof (rule isomorphic_relative_contractible_space_imp_homology_groups)
lp15@70097
  1018
      show "(topspace (Euclidean_space (Suc n)) - S = {}) =
lp15@70097
  1019
            (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n) = {})"
lp15@70097
  1020
        using cl_n closedin_subset that by auto
lp15@70097
  1021
    next
lp15@70097
  1022
      fix p
lp15@70097
  1023
      show "relative_homology_group p (Euclidean_space (Suc n))
lp15@70097
  1024
         (topspace (Euclidean_space (Suc n)) - S) \<cong>
lp15@70097
  1025
        relative_homology_group p (Euclidean_space (Suc n))
lp15@70097
  1026
         (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n))"
lp15@70097
  1027
        by (simp add: L sub_SucS cl_S cl_n isomorphic_relative_homology_groups_Euclidean_complements sub)
lp15@70097
  1028
    qed (auto simp: L)
lp15@70097
  1029
    moreover
lp15@70097
  1030
    have "continuous_map (powertop_real UNIV) euclideanreal (\<lambda>x. x n)"
lp15@70097
  1031
      by (metis (no_types) UNIV_I continuous_map_product_projection)
lp15@70097
  1032
    then have cm: "continuous_map (subtopology (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n)))
lp15@70097
  1033
                                  euclideanreal (\<lambda>x. x n)"
lp15@70097
  1034
      by (simp add: Euclidean_space_def continuous_map_from_subtopology)
lp15@70097
  1035
    have False if "path_connected_space
lp15@70097
  1036
                      (subtopology (Euclidean_space (Suc n))
lp15@70097
  1037
                       (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n)))"
lp15@70097
  1038
      using path_connectedin_continuous_map_image [OF cm that [unfolded path_connectedin_topspace [symmetric]]]
lp15@70097
  1039
            bounded_path_connected_Compl_real [of "{0}"]
lp15@70097
  1040
      by (simp add: topspace_Euclidean_space image_def Bex_def non0 flip: path_connectedin_topspace)
lp15@70097
  1041
    moreover
lp15@70097
  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"
lp15@70097
  1043
      by auto
lp15@70097
  1044
    have "path_connectedin (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - S)"
lp15@70097
  1045
    proof (subst eq, rule path_connectedin_Un)
lp15@70097
  1046
      have "topspace(Euclidean_space(Suc n)) \<inter> {x. x n = 0} = topspace(Euclidean_space n)"
lp15@70097
  1047
        apply (auto simp: topspace_Euclidean_space)
lp15@70097
  1048
        by (metis Suc_leI inf.absorb_iff2 inf.orderE leI)
lp15@70097
  1049
      let ?S = "topspace(Euclidean_space(Suc n)) \<inter> {x. x n < 0}"
lp15@70097
  1050
      show "path_connectedin (Euclidean_space (Suc n))
lp15@70097
  1051
              ((topspace (Euclidean_space (Suc n)) - S) \<inter> {x. x n \<le> 0})"
lp15@70097
  1052
      proof (rule lemma_iod)
lp15@70097
  1053
        show "?S \<subseteq> (topspace (Euclidean_space (Suc n)) - S) \<inter> {x. x n \<le> 0}"
lp15@70097
  1054
          using Ssub topspace_Euclidean_space by auto
lp15@70097
  1055
        show "?S \<noteq> {}"
lp15@70097
  1056
          apply (simp add: topspace_Euclidean_space set_eq_iff)
lp15@70097
  1057
          apply (rule_tac x="(\<lambda>i. 0)(n:= -1)" in exI)
lp15@70097
  1058
          apply auto
lp15@70097
  1059
          done
lp15@70097
  1060
        fix a b and u::real
lp15@70097
  1061
        assume
lp15@70097
  1062
          "a \<in> ?S" "0 < u" "u < 1"
lp15@70097
  1063
          "b \<in> (topspace (Euclidean_space (Suc n)) - S) \<inter> {x. x n \<le> 0}"
lp15@70097
  1064
        then show "(\<lambda>i. (1 - u) * a i + u * b i) \<in> ?S"
lp15@70097
  1065
          by (simp add: topspace_Euclidean_space add_neg_nonpos less_eq_real_def mult_less_0_iff)
lp15@70097
  1066
      qed (simp add: topspace_Euclidean_space subset_iff)
lp15@70097
  1067
      let ?T = "topspace(Euclidean_space(Suc n)) \<inter> {x. x n > 0}"
lp15@70097
  1068
      show "path_connectedin (Euclidean_space (Suc n))
lp15@70097
  1069
              ((topspace (Euclidean_space (Suc n)) - S) \<inter> {x. 0 \<le> x n})"
lp15@70097
  1070
      proof (rule lemma_iod)
lp15@70097
  1071
        show "?T \<subseteq> (topspace (Euclidean_space (Suc n)) - S) \<inter> {x. 0 \<le> x n}"
lp15@70097
  1072
          using Ssub topspace_Euclidean_space by auto
lp15@70097
  1073
        show "?T \<noteq> {}"
lp15@70097
  1074
          apply (simp add: topspace_Euclidean_space set_eq_iff)
lp15@70097
  1075
          apply (rule_tac x="(\<lambda>i. 0)(n:= 1)" in exI)
lp15@70097
  1076
          apply auto
lp15@70097
  1077
          done
lp15@70097
  1078
        fix a b and u::real
lp15@70097
  1079
        assume  "a \<in> ?T" "0 < u" "u < 1" "b \<in> (topspace (Euclidean_space (Suc n)) - S) \<inter> {x. 0 \<le> x n}"
lp15@70097
  1080
        then show "(\<lambda>i. (1 - u) * a i + u * b i) \<in> ?T"
lp15@70097
  1081
          by (simp add: topspace_Euclidean_space add_pos_nonneg)
lp15@70097
  1082
      qed (simp add: topspace_Euclidean_space subset_iff)
lp15@70097
  1083
      show "(topspace (Euclidean_space (Suc n)) - S) \<inter> {x. x n \<le> 0} \<inter>
lp15@70097
  1084
            ((topspace (Euclidean_space (Suc n)) - S) \<inter> {x. 0 \<le> x n}) \<noteq> {}"
lp15@70097
  1085
        using that
lp15@70097
  1086
        apply (auto simp: Set.set_eq_iff topspace_Euclidean_space)
lp15@70097
  1087
        by (metis Suc_leD order_refl)
lp15@70097
  1088
    qed
lp15@70097
  1089
    then have "path_connected_space (subtopology (Euclidean_space (Suc n))
lp15@70097
  1090
                                         (topspace (Euclidean_space (Suc n)) - S))"
lp15@70097
  1091
      apply (simp add: path_connectedin_subtopology flip: path_connectedin_topspace)
lp15@70097
  1092
      by (metis Int_Diff inf_idem)
lp15@70097
  1093
    ultimately
lp15@70097
  1094
    show ?thesis
lp15@70097
  1095
      using isomorphic_homology_imp_path_connectedness by blast
lp15@70097
  1096
  qed
lp15@70097
  1097
  ultimately show ?rhs
lp15@70097
  1098
    by blast
lp15@70097
  1099
qed (simp add: homeomorphic_space_refl)
lp15@70097
  1100
lp15@70097
  1101
lp15@70097
  1102
lp15@70097
  1103
lemma isomorphic_homology_groups_Euclidean_complements:
lp15@70097
  1104
  assumes "closedin (Euclidean_space n) S" "closedin (Euclidean_space n) T"
lp15@70097
  1105
           "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)"
lp15@70097
  1106
  shows "homology_group p (subtopology (Euclidean_space n) (topspace(Euclidean_space n) - S))
lp15@70097
  1107
         \<cong> homology_group p (subtopology (Euclidean_space n) (topspace(Euclidean_space n) - T))"
lp15@70097
  1108
proof (rule isomorphic_relative_contractible_space_imp_homology_groups)
lp15@70097
  1109
  show "topspace (Euclidean_space n) - S \<subseteq> topspace (Euclidean_space n)"
lp15@70097
  1110
    using assms homeomorphic_space_sym invariance_of_dimension_closedin_Euclidean_space subtopology_superset by fastforce
lp15@70097
  1111
  show "topspace (Euclidean_space n) - T \<subseteq> topspace (Euclidean_space n)"
lp15@70097
  1112
    using assms invariance_of_dimension_closedin_Euclidean_space subtopology_superset by force
lp15@70097
  1113
  show "(topspace (Euclidean_space n) - S = {}) = (topspace (Euclidean_space n) - T = {})"
lp15@70097
  1114
    by (metis Diff_eq_empty_iff assms closedin_subset homeomorphic_space_sym invariance_of_dimension_closedin_Euclidean_space subset_antisym subtopology_topspace)
lp15@70097
  1115
  show "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - S) \<cong>
lp15@70097
  1116
        relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - T)" for p
lp15@70097
  1117
    using assms isomorphic_relative_homology_groups_Euclidean_complements by blast
lp15@70097
  1118
qed auto
lp15@70097
  1119
lp15@70097
  1120
lemma eqpoll_path_components_Euclidean_complements:
lp15@70097
  1121
  assumes "closedin (Euclidean_space n) S" "closedin (Euclidean_space n) T"
lp15@70097
  1122
          "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)"
lp15@70097
  1123
 shows "path_components_of
lp15@70097
  1124
             (subtopology (Euclidean_space n)
lp15@70097
  1125
                          (topspace(Euclidean_space n) - S))
lp15@70097
  1126
      \<approx> path_components_of
lp15@70097
  1127
             (subtopology (Euclidean_space n)
lp15@70097
  1128
                          (topspace(Euclidean_space n) - T))"
lp15@70097
  1129
  by (simp add: assms isomorphic_homology_groups_Euclidean_complements isomorphic_homology_imp_path_components)
lp15@70097
  1130
lp15@70097
  1131
lemma path_connectedin_Euclidean_complements:
lp15@70097
  1132
  assumes "closedin (Euclidean_space n) S" "closedin (Euclidean_space n) T"
lp15@70097
  1133
          "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)"
lp15@70097
  1134
  shows "path_connectedin (Euclidean_space n) (topspace(Euclidean_space n) - S)
lp15@70097
  1135
         \<longleftrightarrow> path_connectedin (Euclidean_space n) (topspace(Euclidean_space n) - T)"
lp15@70097
  1136
  by (meson Diff_subset assms isomorphic_homology_groups_Euclidean_complements isomorphic_homology_imp_path_connectedness path_connectedin_def)
lp15@70097
  1137
lp15@70097
  1138
lemma eqpoll_connected_components_Euclidean_complements:
lp15@70097
  1139
  assumes S: "closedin (Euclidean_space n) S" and T: "closedin (Euclidean_space n) T"
lp15@70097
  1140
     and ST: "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)"
lp15@70097
  1141
  shows "connected_components_of
lp15@70097
  1142
             (subtopology (Euclidean_space n)
lp15@70097
  1143
                          (topspace(Euclidean_space n) - S))
lp15@70097
  1144
        \<approx> connected_components_of
lp15@70097
  1145
             (subtopology (Euclidean_space n)
lp15@70097
  1146
                          (topspace(Euclidean_space n) - T))"
lp15@70097
  1147
  using eqpoll_path_components_Euclidean_complements [OF assms]
lp15@70097
  1148
  by (metis S T closedin_def locally_path_connected_Euclidean_space locally_path_connected_space_open_subset path_components_eq_connected_components_of)
lp15@70097
  1149
lp15@70097
  1150
lemma connected_in_Euclidean_complements:
lp15@70097
  1151
  assumes "closedin (Euclidean_space n) S" "closedin (Euclidean_space n) T"
lp15@70097
  1152
          "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)"
lp15@70097
  1153
  shows "connectedin (Euclidean_space n) (topspace(Euclidean_space n) - S)
lp15@70097
  1154
     \<longleftrightarrow> connectedin (Euclidean_space n) (topspace(Euclidean_space n) - T)"
lp15@70097
  1155
  apply (simp add: connectedin_def connected_space_iff_components_subset_singleton subset_singleton_iff_lepoll)
lp15@70097
  1156
  using eqpoll_connected_components_Euclidean_complements [OF assms]
lp15@70097
  1157
  by (meson eqpoll_sym lepoll_trans1)
lp15@70097
  1158
lp15@70097
  1159
lp15@70097
  1160
theorem invariance_of_dimension_Euclidean_space:
lp15@70097
  1161
   "Euclidean_space m homeomorphic_space Euclidean_space n \<longleftrightarrow> m = n"
lp15@70097
  1162
proof (cases m n rule: linorder_cases)
lp15@70097
  1163
  case less
lp15@70097
  1164
  then have *: "topspace (Euclidean_space m) \<subseteq> topspace (Euclidean_space n)"
lp15@70097
  1165
    by (meson le_cases not_le subset_Euclidean_space)
lp15@70097
  1166
  then have "Euclidean_space m = subtopology (Euclidean_space n) (topspace(Euclidean_space m))"
lp15@70097
  1167
    by (simp add: Euclidean_space_def inf.absorb_iff2 subtopology_subtopology)
lp15@70097
  1168
  then show ?thesis
lp15@70097
  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)
lp15@70097
  1170
next
lp15@70097
  1171
  case equal
lp15@70097
  1172
  then show ?thesis
lp15@70097
  1173
    by (simp add: homeomorphic_space_refl)
lp15@70097
  1174
next
lp15@70097
  1175
  case greater
lp15@70097
  1176
  then have *: "topspace (Euclidean_space n) \<subseteq> topspace (Euclidean_space m)"
lp15@70097
  1177
    by (meson le_cases not_le subset_Euclidean_space)
lp15@70097
  1178
  then have "Euclidean_space n = subtopology (Euclidean_space m) (topspace(Euclidean_space n))"
lp15@70097
  1179
    by (simp add: Euclidean_space_def inf.absorb_iff2 subtopology_subtopology)
lp15@70097
  1180
  then show ?thesis
lp15@70097
  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)
lp15@70097
  1182
qed
lp15@70097
  1183
lp15@70097
  1184
lp15@70097
  1185
lp15@70097
  1186
lemma biglemma:
lp15@70097
  1187
  assumes "n \<noteq> 0" and S: "compactin (Euclidean_space n) S"
lp15@70097
  1188
      and cmh: "continuous_map (subtopology (Euclidean_space n) S) (Euclidean_space n) h"
lp15@70097
  1189
      and "inj_on h S"
lp15@70097
  1190
    shows "path_connectedin (Euclidean_space n) (topspace(Euclidean_space n) - h ` S)
lp15@70097
  1191
       \<longleftrightarrow> path_connectedin (Euclidean_space n) (topspace(Euclidean_space n) - S)"
lp15@70097
  1192
proof (rule path_connectedin_Euclidean_complements)
lp15@70097
  1193
  have hS_sub: "h ` S \<subseteq> topspace(Euclidean_space n)"
lp15@70097
  1194
    by (metis (no_types) S cmh compactin_subspace continuous_map_image_subset_topspace topspace_subtopology_subset)
lp15@70097
  1195
  show clo_S: "closedin (Euclidean_space n) S"
lp15@70097
  1196
    using assms by (simp add: continuous_map_in_subtopology Hausdorff_Euclidean_space compactin_imp_closedin)
lp15@70097
  1197
  show clo_hS: "closedin (Euclidean_space n) (h ` S)"
lp15@70097
  1198
    using Hausdorff_Euclidean_space S cmh compactin_absolute compactin_imp_closedin image_compactin by blast
lp15@70097
  1199
  have "homeomorphic_map (subtopology (Euclidean_space n) S) (subtopology (Euclidean_space n) (h ` S)) h"
lp15@70097
  1200
  proof (rule continuous_imp_homeomorphic_map)
lp15@70097
  1201
    show "compact_space (subtopology (Euclidean_space n) S)"
lp15@70097
  1202
      by (simp add: S compact_space_subtopology)
lp15@70097
  1203
    show "Hausdorff_space (subtopology (Euclidean_space n) (h ` S))"
lp15@70097
  1204
      using hS_sub
lp15@70097
  1205
      by (simp add: Hausdorff_Euclidean_space Hausdorff_space_subtopology)
lp15@70097
  1206
    show "continuous_map (subtopology (Euclidean_space n) S) (subtopology (Euclidean_space n) (h ` S)) h"
lp15@70097
  1207
      using cmh continuous_map_in_subtopology by fastforce
lp15@70097
  1208
    show "h ` topspace (subtopology (Euclidean_space n) S) = topspace (subtopology (Euclidean_space n) (h ` S))"
lp15@70097
  1209
      using clo_hS clo_S closedin_subset by auto
lp15@70097
  1210
    show "inj_on h (topspace (subtopology (Euclidean_space n) S))"
lp15@70097
  1211
      by (metis \<open>inj_on h S\<close> clo_S closedin_def topspace_subtopology_subset)
lp15@70097
  1212
  qed
lp15@70097
  1213
  then show "subtopology (Euclidean_space n) (h ` S) homeomorphic_space subtopology (Euclidean_space n) S"
lp15@70097
  1214
    using homeomorphic_space homeomorphic_space_sym by blast
lp15@70097
  1215
qed
lp15@70097
  1216
lp15@70097
  1217
lp15@70097
  1218
lemma lemmaIOD:
lp15@70097
  1219
  assumes
lp15@70097
  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> {}"
lp15@70097
  1221
    "pairwise disjnt U" "~(\<exists>T. U \<subseteq> {T})"
lp15@70097
  1222
  shows "c \<in> U"
lp15@70097
  1223
  using assms
lp15@70097
  1224
  apply safe
lp15@70097
  1225
  subgoal for C' D'
lp15@70097
  1226
  proof (cases "C'=D'")
lp15@70097
  1227
    show "c \<in> U"
lp15@70097
  1228
      if UU: "\<Union> U = c \<union> d"
lp15@70097
  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'"
lp15@70097
  1230
    proof -
lp15@70097
  1231
      have "c \<union> d = D'"
lp15@70097
  1232
        using Union_upper sup_mono UU that(5) that(6) that(7) that(8) by auto
lp15@70097
  1233
      then have "\<Union>U = D'"
lp15@70097
  1234
        by (simp add: UU)
lp15@70097
  1235
      with U have "U = {D'}"
lp15@70097
  1236
        by (metis (no_types, lifting) disjnt_Union1 disjnt_self_iff_empty insertCI pairwiseD subset_iff that(4) that(6))
lp15@70097
  1237
      then show ?thesis
lp15@70097
  1238
        using that(4) by auto
lp15@70097
  1239
    qed
lp15@70097
  1240
    show "c \<in> U"
lp15@70097
  1241
      if "\<Union> U = c \<union> d""disjoint U" "C' \<in> U" "c \<subseteq> C'""D' \<in> U" "d \<subseteq> D'" "C' \<noteq> D'"
lp15@70097
  1242
    proof -
lp15@70097
  1243
      have "C' \<inter> D' = {}"
lp15@70097
  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
lp15@70097
  1245
        by blast
lp15@70097
  1246
      then show ?thesis
lp15@70097
  1247
        using subset_antisym that(1) \<open>C' \<in> U\<close> \<open>c \<subseteq> C'\<close> \<open>d \<subseteq> D'\<close> by fastforce
lp15@70097
  1248
    qed
lp15@70097
  1249
  qed
lp15@70097
  1250
  done
lp15@70097
  1251
lp15@70097
  1252
lp15@70097
  1253
lp15@70097
  1254
lp15@70097
  1255
theorem invariance_of_domain_Euclidean_space:
lp15@70097
  1256
  assumes U: "openin (Euclidean_space n) U"
lp15@70097
  1257
    and cmf: "continuous_map (subtopology (Euclidean_space n) U) (Euclidean_space n) f"
lp15@70097
  1258
    and "inj_on f U"
lp15@70097
  1259
  shows "openin (Euclidean_space n) (f ` U)"   (is "openin ?E (f ` U)")
lp15@70097
  1260
proof (cases "n = 0")
lp15@70097
  1261
  case True
lp15@70097
  1262
  have [simp]: "Euclidean_space 0 = discrete_topology {\<lambda>i. 0}"
lp15@70097
  1263
    by (auto simp: subtopology_eq_discrete_topology_sing topspace_Euclidean_space)
lp15@70097
  1264
  show ?thesis
lp15@70097
  1265
    using cmf True U by auto
lp15@70097
  1266
next
lp15@70097
  1267
  case False
lp15@70097
  1268
  define enorm where "enorm \<equiv> \<lambda>x. sqrt(\<Sum>i<n. x i ^ 2)"
lp15@70097
  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
lp15@70097
  1270
    using \<open>n \<noteq> 0\<close> by (auto simp:  enorm_def power2_eq_square if_distrib [of "\<lambda>x. x * _"] cong: if_cong)
lp15@70097
  1271
  define zero::"nat\<Rightarrow>real" where "zero \<equiv> \<lambda>i. 0"
lp15@70097
  1272
  have zero_in [simp]: "zero \<in> topspace ?E"
lp15@70097
  1273
    using False by (simp add: zero_def topspace_Euclidean_space)
lp15@70097
  1274
  have enorm_eq_0 [simp]: "enorm x = 0 \<longleftrightarrow> x = zero"
lp15@70097
  1275
    if "x \<in> topspace(Euclidean_space n)" for x
lp15@70097
  1276
    using that unfolding zero_def enorm_def
lp15@70097
  1277
    apply (simp add: sum_nonneg_eq_0_iff fun_eq_iff topspace_Euclidean_space)
lp15@70097
  1278
    using le_less_linear by blast
lp15@70097
  1279
  have [simp]: "enorm zero = 0"
lp15@70097
  1280
    by (simp add: zero_def enorm_def)
lp15@70097
  1281
  have cm_enorm: "continuous_map ?E euclideanreal enorm"
lp15@70097
  1282
    unfolding enorm_def
lp15@70097
  1283
  proof (intro continuous_intros)
lp15@70097
  1284
    show "continuous_map ?E euclideanreal (\<lambda>x. x i)"
lp15@70097
  1285
      if "i \<in> {..<n}" for i
lp15@70097
  1286
      using that by (auto simp: Euclidean_space_def intro: continuous_map_product_projection continuous_map_from_subtopology)
lp15@70097
  1287
  qed auto
lp15@70097
  1288
  have enorm_ge0: "0 \<le> enorm x" for x
lp15@70097
  1289
    by (auto simp: enorm_def sum_nonneg)
lp15@70097
  1290
  have le_enorm: "\<bar>x i\<bar> \<le> enorm x" if "i < n" for i x
lp15@70097
  1291
  proof -
lp15@70097
  1292
    have "\<bar>x i\<bar> \<le> sqrt (\<Sum>k\<in>{i}. (x k)\<^sup>2)"
lp15@70097
  1293
      by auto
lp15@70097
  1294
    also have "\<dots> \<le> sqrt (\<Sum>k<n. (x k)\<^sup>2)"
lp15@70097
  1295
      by (rule real_sqrt_le_mono [OF sum_mono2]) (use that in auto)
lp15@70097
  1296
    finally show ?thesis
lp15@70097
  1297
      by (simp add: enorm_def)
lp15@70097
  1298
  qed
lp15@70097
  1299
  define B where "B \<equiv> \<lambda>r. {x \<in> topspace ?E. enorm x < r}"
lp15@70097
  1300
  define C where "C \<equiv> \<lambda>r. {x \<in> topspace ?E. enorm x \<le> r}"
lp15@70097
  1301
  define S where "S \<equiv> \<lambda>r. {x \<in> topspace ?E. enorm x = r}"
lp15@70097
  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
lp15@70097
  1303
    by (auto simp: B_def C_def S_def disjnt_def)
lp15@70097
  1304
  consider "n = 1" | "n \<ge> 2"
lp15@70097
  1305
    using False by linarith
lp15@70097
  1306
  then have **: "openin ?E (h ` (B r))"
lp15@70097
  1307
    if "r > 0" and cmh: "continuous_map(subtopology ?E (C r)) ?E h" and injh: "inj_on h (C r)" for r h
lp15@70097
  1308
  proof cases
lp15@70097
  1309
    case 1
lp15@70097
  1310
    define e :: "[real,nat]\<Rightarrow>real" where "e \<equiv> \<lambda>x i. if i = 0 then x else 0"
lp15@70097
  1311
    define e' :: "(nat\<Rightarrow>real)\<Rightarrow>real" where "e' \<equiv> \<lambda>x. x 0"
lp15@70097
  1312
    have "continuous_map euclidean euclideanreal (\<lambda>f. f (0::nat))"
lp15@70097
  1313
      by auto
lp15@70097
  1314
    then have "continuous_map (subtopology (powertop_real UNIV) {f. \<forall>n\<ge>Suc 0. f n = 0}) euclideanreal (\<lambda>f. f 0)"
lp15@70097
  1315
      by (metis (mono_tags) continuous_map_from_subtopology euclidean_product_topology)
lp15@70097
  1316
    then have hom_ee': "homeomorphic_maps euclideanreal (Euclidean_space 1) e e'"
lp15@70097
  1317
      by (auto simp: homeomorphic_maps_def e_def e'_def continuous_map_in_subtopology Euclidean_space_def)
lp15@70097
  1318
    have eBr: "e ` {-r<..<r} = B r"
lp15@70097
  1319
      unfolding B_def e_def C_def
lp15@70097
  1320
      by(force simp: "1" topspace_Euclidean_space enorm_def power2_eq_square if_distrib [of "\<lambda>x. x * _"] cong: if_cong)
lp15@70097
  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"
lp15@70097
  1322
      using \<open>n \<noteq> 0\<close> by (auto simp: C_def topspace_Euclidean_space)
lp15@70097
  1323
    have inj: "inj_on (e' \<circ> h \<circ> e) {- r<..<r}"
lp15@70097
  1324
    proof (clarsimp simp: inj_on_def e_def e'_def)
lp15@70097
  1325
      show "(x::real) = y"
lp15@70097
  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"
lp15@70097
  1327
          and "-r < x" "x < r" "-r < y" "y < r"
lp15@70097
  1328
        for x y :: real
lp15@70097
  1329
      proof -
lp15@70097
  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"
lp15@70097
  1331
          by (blast intro: inj_onD [OF \<open>inj_on h (C r)\<close>] that in_Cr)+
lp15@70097
  1332
        have "continuous_map (subtopology (Euclidean_space (Suc 0)) (C r)) (Euclidean_space (Suc 0)) h"
lp15@70097
  1333
          using cmh by (simp add: 1)
lp15@70097
  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}"
lp15@70097
  1335
          by (force simp: Euclidean_space_def subtopology_subtopology continuous_map_def)
lp15@70097
  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
lp15@70097
  1337
        proof (cases j)
lp15@70097
  1338
          case (Suc j')
lp15@70097
  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}"
lp15@70097
  1340
            using continuous_map_image_subset_topspace [OF cmh]
lp15@70097
  1341
            by (simp add: 1 Euclidean_space_def subtopology_subtopology)
lp15@70097
  1342
          with Suc f x y show ?thesis
lp15@70097
  1343
            by (simp add: "1" image_subset_iff)
lp15@70097
  1344
        qed (use f in blast)
lp15@70097
  1345
        then have "(\<lambda>i. if i = 0 then x else 0) = (\<lambda>i::nat. if i = 0 then y else 0)"
lp15@70097
  1346
          by (blast intro: inj_onD [OF \<open>inj_on h (C r)\<close>] that in_Cr)
lp15@70097
  1347
        then show ?thesis
lp15@70097
  1348
          by (simp add: fun_eq_iff) presburger
lp15@70097
  1349
      qed
lp15@70097
  1350
    qed
lp15@70097
  1351
    have hom_e': "homeomorphic_map (Euclidean_space 1) euclideanreal e'"
lp15@70097
  1352
      using hom_ee' homeomorphic_maps_map by blast
lp15@70097
  1353
    have "openin (Euclidean_space n) (h ` e ` {- r<..<r})"
lp15@70097
  1354
      unfolding 1
lp15@70097
  1355
    proof (subst homeomorphic_map_openness [OF hom_e', symmetric])
lp15@70097
  1356
      show "h ` e ` {- r<..<r} \<subseteq> topspace (Euclidean_space 1)"
lp15@70097
  1357
        using "1" C_def \<open>\<And>r. B r \<subseteq> C r\<close> cmh continuous_map_image_subset_topspace eBr by fastforce
lp15@70097
  1358
      have cont: "continuous_on {- r<..<r} (e' \<circ> h \<circ> e)"
lp15@70097
  1359
      proof (intro continuous_on_compose)
lp15@70097
  1360
        have "\<And>i. continuous_on {- r<..<r} (\<lambda>x. if i = 0 then x else 0)"
lp15@70097
  1361
          by (auto simp: continuous_on_topological)
lp15@70097
  1362
        then show "continuous_on {- r<..<r} e"
lp15@70097
  1363
          by (force simp: e_def intro: continuous_on_coordinatewise_then_product)
lp15@70097
  1364
        have subCr: "e ` {- r<..<r} \<subseteq> topspace (subtopology ?E (C r))"
lp15@70097
  1365
          by (auto simp: eBr \<open>\<And>r. B r \<subseteq> C r\<close>) (auto simp: B_def)
lp15@70097
  1366
        with cmh show "continuous_on (e ` {- r<..<r}) h"
lp15@70097
  1367
          by (meson cm_Euclidean_space_iff_continuous_on continuous_on_subset)
lp15@70097
  1368
        have "h ` (e ` {- r<..<r}) \<subseteq> topspace ?E"
lp15@70097
  1369
          using subCr cmh by (simp add: continuous_map_def image_subset_iff)
lp15@70097
  1370
        moreover have "continuous_on (topspace ?E) e'"
lp15@70097
  1371
          by (metis "1" continuous_map_Euclidean_space_iff hom_ee' homeomorphic_maps_def)
lp15@70097
  1372
        ultimately show "continuous_on (h ` e ` {- r<..<r}) e'"
lp15@70097
  1373
          by (simp add: e'_def continuous_on_subset)
lp15@70097
  1374
      qed
lp15@70097
  1375
      show "openin euclideanreal (e' ` h ` e ` {- r<..<r})"
lp15@70097
  1376
        using injective_eq_1d_open_map_UNIV [OF cont] inj by (simp add: image_image is_interval_1)
lp15@70097
  1377
    qed
lp15@70097
  1378
    then show ?thesis
lp15@70097
  1379
      by (simp flip: eBr)
lp15@70097
  1380
  next
lp15@70097
  1381
    case 2
lp15@70097
  1382
    have cloC: "\<And>r. closedin (Euclidean_space n) (C r)"
lp15@70097
  1383
      unfolding C_def
lp15@70097
  1384
      by (rule closedin_continuous_map_preimage [OF cm_enorm, of concl:  "{.._}", simplified])
lp15@70097
  1385
    have cloS: "\<And>r. closedin (Euclidean_space n) (S r)"
lp15@70097
  1386
      unfolding S_def
lp15@70097
  1387
      by (rule closedin_continuous_map_preimage [OF cm_enorm, of concl:  "{_}", simplified])
lp15@70097
  1388
    have C_subset: "C r \<subseteq> UNIV \<rightarrow>\<^sub>E {- \<bar>r\<bar>..\<bar>r\<bar>}"
lp15@70097
  1389
      using le_enorm \<open>r > 0\<close>
lp15@70097
  1390
      apply (auto simp: C_def topspace_Euclidean_space abs_le_iff)
lp15@70097
  1391
       apply (metis add.inverse_neutral le_cases less_minus_iff not_le order_trans)
lp15@70097
  1392
      by (metis enorm_ge0 not_le order.trans)
lp15@70097
  1393
    have compactinC: "compactin (Euclidean_space n) (C r)"
lp15@70097
  1394
      unfolding Euclidean_space_def compactin_subtopology
lp15@70097
  1395
    proof
lp15@70097
  1396
      show "compactin (powertop_real UNIV) (C r)"
lp15@70097
  1397
      proof (rule closed_compactin [OF _ C_subset])
lp15@70097
  1398
        show "closedin (powertop_real UNIV) (C r)"
lp15@70097
  1399
          by (metis Euclidean_space_def cloC closedin_Euclidean_space closedin_closed_subtopology topspace_Euclidean_space)
lp15@70097
  1400
      qed (simp add: compactin_PiE)
lp15@70097
  1401
    qed (auto simp: C_def topspace_Euclidean_space)
lp15@70097
  1402
    have compactinS: "compactin (Euclidean_space n) (S r)"
lp15@70097
  1403
      unfolding Euclidean_space_def compactin_subtopology
lp15@70097
  1404
    proof
lp15@70097
  1405
      show "compactin (powertop_real UNIV) (S r)"
lp15@70097
  1406
      proof (rule closed_compactin)
lp15@70097
  1407
        show "S r \<subseteq> UNIV \<rightarrow>\<^sub>E {- \<bar>r\<bar>..\<bar>r\<bar>}"
lp15@70097
  1408
          using C_subset \<open>\<And>r. S r \<subseteq> C r\<close> by blast
lp15@70097
  1409
        show "closedin (powertop_real UNIV) (S r)"
lp15@70097
  1410
          by (metis Euclidean_space_def cloS closedin_Euclidean_space closedin_closed_subtopology topspace_Euclidean_space)
lp15@70097
  1411
      qed (simp add: compactin_PiE)
lp15@70097
  1412
    qed (auto simp: S_def topspace_Euclidean_space)
lp15@70097
  1413
    have h_if_B: "\<And>y. y \<in> B r \<Longrightarrow> h y \<in> topspace ?E"
lp15@70097
  1414
      using B_def \<open>\<And>r. B r \<union> S r = C r\<close> cmh continuous_map_image_subset_topspace by fastforce
lp15@70097
  1415
    have com_hSr: "compactin (Euclidean_space n) (h ` S r)"
lp15@70097
  1416
      by (meson \<open>\<And>r. S r \<subseteq> C r\<close> cmh compactinS compactin_subtopology image_compactin)
lp15@70097
  1417
    have ope_comp_hSr: "openin (Euclidean_space n) (topspace (Euclidean_space n) - h ` S r)"
lp15@70097
  1418
    proof (rule openin_diff)
lp15@70097
  1419
      show "closedin (Euclidean_space n) (h ` S r)"
lp15@70097
  1420
        using Hausdorff_Euclidean_space com_hSr compactin_imp_closedin by blast
lp15@70097
  1421
    qed auto
lp15@70097
  1422
    have h_pcs: "h ` (B r) \<in> path_components_of (subtopology ?E (topspace ?E - h ` (S r)))"
lp15@70097
  1423
    proof (rule lemmaIOD)
lp15@70097
  1424
      have pc_interval: "path_connectedin (Euclidean_space n) {x \<in> topspace(Euclidean_space n). enorm x \<in> T}"
lp15@70097
  1425
        if T: "is_interval T" for T
lp15@70097
  1426
      proof -
lp15@70097
  1427
        define mul :: "[real, nat \<Rightarrow> real, nat] \<Rightarrow> real" where "mul \<equiv> \<lambda>a x i. a * x i"
lp15@70097
  1428
        let ?neg = "mul (-1)"
lp15@70097
  1429
        have neg_neg [simp]: "?neg (?neg x) = x" for x
lp15@70097
  1430
          by (simp add: mul_def)
lp15@70097
  1431
        have enorm_mul [simp]: "enorm(mul a x) = abs a * enorm x" for a x
lp15@70097
  1432
          by (simp add: enorm_def mul_def power_mult_distrib) (metis real_sqrt_abs real_sqrt_mult sum_distrib_left)
lp15@70097
  1433
        have mul_in_top: "mul a x \<in> topspace ?E"
lp15@70097
  1434
            if "x \<in> topspace ?E" for a x
lp15@70097
  1435
          using mul_def that topspace_Euclidean_space by auto
lp15@70097
  1436
        have neg_in_S: "?neg x \<in> S r"
lp15@70097
  1437
            if "x \<in> S r" for x r
lp15@70097
  1438
          using that topspace_Euclidean_space S_def by simp (simp add: mul_def)
lp15@70097
  1439
        have *: "path_connectedin ?E (S d)"
lp15@70097
  1440
          if "d \<ge> 0" for d
lp15@70097
  1441
        proof (cases "d = 0")
lp15@70097
  1442
          let ?ES = "subtopology ?E (S d)"
lp15@70097
  1443
          case False
lp15@70097
  1444
          then have "d > 0"
lp15@70097
  1445
            using that by linarith
lp15@70097
  1446
          moreover have "path_connected_space ?ES"
lp15@70097
  1447
            unfolding path_connected_space_iff_path_component
lp15@70097
  1448
          proof clarify
lp15@70097
  1449
            have **: "path_component_of ?ES x y"
lp15@70097
  1450
              if x: "x \<in> topspace ?ES" and y: "y \<in> topspace ?ES" "x \<noteq> ?neg y" for x y
lp15@70097
  1451
            proof -
lp15@70097
  1452
              show ?thesis
lp15@70097
  1453
                unfolding path_component_of_def pathin_def S_def
lp15@70097
  1454
              proof (intro exI conjI)
lp15@70097
  1455
                let ?g = "(\<lambda>x. mul (d / enorm x) x) \<circ> (\<lambda>t i. (1 - t) * x i + t * y i)"
lp15@70097
  1456
                show "continuous_map (top_of_set {0::real..1}) (subtopology ?E {x \<in> topspace ?E. enorm x = d}) ?g"
lp15@70097
  1457
                proof (rule continuous_map_compose)
lp15@70097
  1458
                  let ?Y = "subtopology ?E (- {zero})"
lp15@70097
  1459
                  have **: False
lp15@70097
  1460
                    if eq0: "\<And>j. (1 - r) * x j + r * y j = 0"
lp15@70097
  1461
                      and ne: "x i \<noteq> - y i"
lp15@70097
  1462
                      and d: "enorm x = d" "enorm y = d"
lp15@70097
  1463
                      and r: "0 \<le> r" "r \<le> 1"
lp15@70097
  1464
                    for i r
lp15@70097
  1465
                  proof -
lp15@70097
  1466
                    have "mul (1-r) x = ?neg (mul r y)"
lp15@70097
  1467
                      using eq0 by (simp add: mul_def fun_eq_iff algebra_simps)
lp15@70097
  1468
                    then have "enorm (mul (1-r) x) = enorm (?neg (mul r y))"
lp15@70097
  1469
                      by metis
lp15@70097
  1470
                    with r have "(1-r) * enorm x = r * enorm y"
lp15@70097
  1471
                      by simp
lp15@70097
  1472
                    then have r12: "r = 1/2"
lp15@70097
  1473
                      using \<open>d \<noteq> 0\<close> d by auto
lp15@70097
  1474
                    show ?thesis
lp15@70097
  1475
                      using ne eq0 [of i] unfolding r12 by (simp add: algebra_simps)
lp15@70097
  1476
                  qed
lp15@70097
  1477
                  show "continuous_map (top_of_set {0..1}) ?Y (\<lambda>t i. (1 - t) * x i + t * y i)"
lp15@70097
  1478
                    using x y
lp15@70097
  1479
                    unfolding continuous_map_componentwise_UNIV Euclidean_space_def continuous_map_in_subtopology
lp15@70097
  1480
                    apply (intro conjI allI continuous_intros)
lp15@70097
  1481
                          apply (auto simp: zero_def mul_def S_def Euclidean_space_def fun_eq_iff)
lp15@70097
  1482
                    using ** by blast
lp15@70097
  1483
                  have cm_enorm': "continuous_map (subtopology (powertop_real UNIV) A) euclideanreal enorm" for A
lp15@70097
  1484
                    unfolding enorm_def by (intro continuous_intros) auto
lp15@70097
  1485
                  have "continuous_map ?Y (subtopology ?E {x. enorm x = d}) (\<lambda>x. mul (d / enorm x) x)"
lp15@70097
  1486
                    unfolding continuous_map_in_subtopology
lp15@70097
  1487
                  proof (intro conjI)
lp15@70097
  1488
                    show "continuous_map ?Y (Euclidean_space n) (\<lambda>x. mul (d / enorm x) x)"
lp15@70097
  1489
                      unfolding continuous_map_in_subtopology Euclidean_space_def mul_def zero_def subtopology_subtopology continuous_map_componentwise_UNIV
lp15@70097
  1490
                    proof (intro conjI allI cm_enorm' continuous_intros)
lp15@70097
  1491
                      show "enorm x \<noteq> 0"
lp15@70097
  1492
                        if "x \<in> topspace (subtopology (powertop_real UNIV) ({x. \<forall>i\<ge>n. x i = 0} \<inter> - {\<lambda>i. 0}))" for x
lp15@70097
  1493
                        using that by simp (metis abs_le_zero_iff le_enorm not_less)
lp15@70097
  1494
                    qed auto
lp15@70097
  1495
                  qed (use \<open>d > 0\<close> enorm_ge0 in auto)
lp15@70097
  1496
                  moreover have "subtopology ?E {x \<in> topspace ?E. enorm x = d} = subtopology ?E {x. enorm x = d}"
lp15@70097
  1497
                    by (simp add: subtopology_restrict Collect_conj_eq)
lp15@70097
  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)"
lp15@70097
  1499
                    by metis
lp15@70097
  1500
                qed
lp15@70097
  1501
                show "?g (0::real) = x" "?g (1::real) = y"
lp15@70097
  1502
                  using that by (auto simp: S_def zero_def mul_def fun_eq_iff)
lp15@70097
  1503
              qed
lp15@70097
  1504
            qed
lp15@70097
  1505
            obtain a b where a: "a \<in> topspace ?ES" and b: "b \<in> topspace ?ES"
lp15@70097
  1506
              and "a \<noteq> b" and negab: "?neg a \<noteq> b"
lp15@70097
  1507
            proof
lp15@70097
  1508
              let ?v = "\<lambda>j i::nat. if i = j then d else 0"
lp15@70097
  1509
              show "?v 0 \<in> topspace (subtopology ?E (S d))" "?v 1 \<in> topspace (subtopology ?E (S d))"
lp15@70097
  1510
                using \<open>n \<ge> 2\<close> \<open>d \<ge> 0\<close> by (auto simp: S_def topspace_Euclidean_space)
lp15@70097
  1511
              show "?v 0 \<noteq> ?v 1" "?neg (?v 0) \<noteq> (?v 1)"
lp15@70097
  1512
                using \<open>d > 0\<close> by (auto simp: mul_def fun_eq_iff)
lp15@70097
  1513
            qed
lp15@70097
  1514
            show "path_component_of ?ES x y"
lp15@70097
  1515
              if x: "x \<in> topspace ?ES" and y: "y \<in> topspace ?ES"
lp15@70097
  1516
              for x y
lp15@70097
  1517
            proof -
lp15@70097
  1518
              have "path_component_of ?ES x (?neg x)"
lp15@70097
  1519
              proof -
lp15@70097
  1520
                have "path_component_of ?ES x a"
lp15@70097
  1521
                  by (metis (no_types, hide_lams) ** a b \<open>a \<noteq> b\<close> negab path_component_of_trans path_component_of_sym x)
lp15@70097
  1522
                moreover
lp15@70097
  1523
                have pa_ab: "path_component_of ?ES a b" using "**" a b negab neg_neg by blast
lp15@70097
  1524
                then have "path_component_of ?ES a (?neg x)"
lp15@70097
  1525
                  by (metis "**" \<open>a \<noteq> b\<close> cloS closedin_def neg_in_S path_component_of_equiv topspace_subtopology_subset x)
lp15@70097
  1526
                ultimately show ?thesis
lp15@70097
  1527
                  by (meson path_component_of_trans)
lp15@70097
  1528
              qed
lp15@70097
  1529
              then show ?thesis
lp15@70097
  1530
                using "**" x y by force
lp15@70097
  1531
            qed
lp15@70097
  1532
          qed
lp15@70097
  1533
          ultimately show ?thesis
lp15@70097
  1534
            by (simp add: cloS closedin_subset path_connectedin_def)
lp15@70097
  1535
        qed (simp add: S_def cong: conj_cong)
lp15@70097
  1536
        have "path_component_of (subtopology ?E {x \<in> topspace ?E. enorm x \<in> T}) x y"
lp15@70097
  1537
          if "enorm x = a" "x \<in> topspace ?E" "enorm x \<in> T" "enorm y = b" "y \<in> topspace ?E" "enorm y \<in> T"
lp15@70097
  1538
          for x y a b
lp15@70097
  1539
          using that
lp15@70097
  1540
          proof (induction a b arbitrary: x y rule: linorder_less_wlog)
lp15@70097
  1541
            case (less a b)
lp15@70097
  1542
            then have "a \<ge> 0"
lp15@70097
  1543
              using enorm_ge0 by blast
lp15@70097
  1544
            with less.hyps have "b > 0"
lp15@70097
  1545
              by linarith
lp15@70097
  1546
            show ?case
lp15@70097
  1547
            proof (rule path_component_of_trans)
lp15@70097
  1548
              have y'_ts: "mul (a / b) y \<in> topspace ?E"
lp15@70097
  1549
                using \<open>y \<in> topspace ?E\<close> mul_in_top by blast
lp15@70097
  1550
              moreover have "enorm (mul (a / b) y) = a"
lp15@70097
  1551
                unfolding enorm_mul using \<open>0 < b\<close> \<open>0 \<le> a\<close> less.prems by simp
lp15@70097
  1552
              ultimately have y'_S: "mul (a / b) y \<in> S a"
lp15@70097
  1553
                using S_def by blast
lp15@70097
  1554
              have "x \<in> S a"
lp15@70097
  1555
                using S_def less.prems by blast
lp15@70097
  1556
              with \<open>x \<in> topspace ?E\<close> y'_ts y'_S
lp15@70097
  1557
              have "path_component_of (subtopology ?E (S a)) x (mul (a / b) y)"
lp15@70097
  1558
                by (metis * [OF \<open>a \<ge> 0\<close>] path_connected_space_iff_path_component path_connectedin_def topspace_subtopology_subset)
lp15@70097
  1559
              moreover
lp15@70097
  1560
              have "{f \<in> topspace ?E. enorm f = a} \<subseteq> {f \<in> topspace ?E. enorm f \<in> T}"
lp15@70097
  1561
                using \<open>enorm x = a\<close> \<open>enorm x \<in> T\<close> by force
lp15@70097
  1562
              ultimately
lp15@70097
  1563
              show "path_component_of (subtopology ?E {x. x \<in> topspace ?E \<and> enorm x \<in> T}) x (mul (a / b) y)"
lp15@70097
  1564
                by (simp add: S_def path_component_of_mono)
lp15@70097
  1565
              have "pathin ?E (\<lambda>t. mul (((1 - t) * b + t * a) / b) y)"
lp15@70097
  1566
                using \<open>b > 0\<close> \<open>y \<in> topspace ?E\<close>
lp15@70097
  1567
                unfolding pathin_def Euclidean_space_def mul_def continuous_map_in_subtopology continuous_map_componentwise_UNIV
lp15@70097
  1568
                by (intro allI conjI continuous_intros) auto
lp15@70097
  1569
              moreover have "mul (((1 - t) * b + t * a) / b) y \<in> topspace ?E"
lp15@70097
  1570
                if "t \<in> {0..1}" for t
lp15@70097
  1571
                using \<open>y \<in> topspace ?E\<close> mul_in_top by blast
lp15@70097
  1572
                moreover have "enorm (mul (((1 - t) * b + t * a) / b) y) \<in> T"
lp15@70097
  1573
                  if "t \<in> {0..1}" for t
lp15@70097
  1574
                proof -
lp15@70097
  1575
                  have "a \<in> T" "b \<in> T"
lp15@70097
  1576
                    using less.prems by auto
lp15@70097
  1577
                  then have "\<bar>(1 - t) * b + t * a\<bar> \<in> T"
lp15@70097
  1578
                  proof (rule mem_is_interval_1_I [OF T])
lp15@70097
  1579
                    show "a \<le> \<bar>(1 - t) * b + t * a\<bar>"
lp15@70097
  1580
                      using that \<open>a \<ge> 0\<close> less.hyps segment_bound_lemma by auto
lp15@70097
  1581
                    show "\<bar>(1 - t) * b + t * a\<bar> \<le> b"
lp15@70097
  1582
                      using that \<open>a \<ge> 0\<close> less.hyps by (auto intro: convex_bound_le)
lp15@70097
  1583
                  qed
lp15@70097
  1584
                then show ?thesis
lp15@70097
  1585
                  unfolding enorm_mul \<open>enorm y = b\<close> using that \<open>b > 0\<close> by simp
lp15@70097
  1586
              qed
lp15@70097
  1587
              ultimately have pa: "pathin (subtopology ?E {x \<in> topspace ?E. enorm x \<in> T})
lp15@70097
  1588
                                          (\<lambda>t. mul (((1 - t) * b + t * a) / b) y)"
lp15@70097
  1589
                by (auto simp: pathin_subtopology)
lp15@70097
  1590
              have ex_pathin: "\<exists>g. pathin (subtopology ?E {x \<in> topspace ?E. enorm x \<in> T}) g \<and>
lp15@70097
  1591
                                   g 0 = y \<and> g 1 = mul (a / b) y"
lp15@70097
  1592
                apply (rule_tac x="\<lambda>t. mul (((1 - t) * b + t * a) / b) y" in exI)
lp15@70097
  1593
                using \<open>b > 0\<close> pa by (auto simp: mul_def)
lp15@70097
  1594
              show "path_component_of (subtopology ?E {x. x \<in> topspace ?E \<and> enorm x \<in> T}) (mul (a / b) y) y"
lp15@70097
  1595
                by (rule path_component_of_sym) (simp add: path_component_of_def ex_pathin)
lp15@70097
  1596
            qed
lp15@70097
  1597
          next
lp15@70097
  1598
            case (refl a)
lp15@70097
  1599
            then have pc: "path_component_of (subtopology ?E (S (enorm u))) u v"
lp15@70097
  1600
              if "u \<in> topspace ?E \<inter> S (enorm x)" "v \<in> topspace ?E \<inter> S (enorm u)" for u v
lp15@70097
  1601
              using * [of a] enorm_ge0 that
lp15@70097
  1602
              by (auto simp: path_connectedin_def path_connected_space_iff_path_component S_def)
lp15@70097
  1603
            have sub: "{u \<in> topspace ?E. enorm u = enorm x} \<subseteq> {u \<in> topspace ?E. enorm u \<in> T}"
lp15@70097
  1604
              using \<open>enorm x \<in> T\<close> by auto
lp15@70097
  1605
            show ?case
lp15@70097
  1606
              using pc [of x y] refl by (auto simp: S_def path_component_of_mono [OF _ sub])
lp15@70097
  1607
          next
lp15@70097
  1608
            case (sym a b)
lp15@70097
  1609
            then show ?case
lp15@70097
  1610
              by (blast intro: path_component_of_sym)
lp15@70097
  1611
          qed
lp15@70097
  1612
        then show ?thesis
lp15@70097
  1613
          by (simp add: path_connectedin_def path_connected_space_iff_path_component)
lp15@70097
  1614
      qed
lp15@70097
  1615
      have "h ` S r \<subseteq> topspace ?E"
lp15@70097
  1616
        by (meson SC cmh compact_imp_compactin_subtopology compactinS compactin_subset_topspace image_compactin)
lp15@70097
  1617
      moreover
lp15@70097
  1618
      have "\<not> compact_space ?E "
lp15@70097
  1619
        by (metis compact_Euclidean_space \<open>n \<noteq> 0\<close>)
lp15@70097
  1620
      then have "\<not> compactin ?E (topspace ?E)"
lp15@70097
  1621
        by (simp add: compact_space_def topspace_Euclidean_space)
lp15@70097
  1622
      then have "h ` S r \<noteq> topspace ?E"
lp15@70097
  1623
        using com_hSr by auto
lp15@70097
  1624
      ultimately have top_hSr_ne: "topspace (subtopology ?E (topspace ?E - h ` S r)) \<noteq> {}"
lp15@70097
  1625
        by auto
lp15@70097
  1626
      show pc1: "\<exists>T. T \<in> path_components_of (subtopology ?E (topspace ?E - h ` S r)) \<and> h ` B r \<subseteq> T"
lp15@70097
  1627
      proof (rule exists_path_component_of_superset [OF _ top_hSr_ne])
lp15@70097
  1628
        have "path_connectedin ?E (h ` B r)"
lp15@70097
  1629
        proof (rule path_connectedin_continuous_map_image)
lp15@70097
  1630
          show "continuous_map (subtopology ?E (C r)) ?E h"
lp15@70097
  1631
            by (simp add: cmh)
lp15@70097
  1632
          have "path_connectedin ?E (B r)"
lp15@70097
  1633
            using pc_interval[of "{..<r}"] is_interval_convex_1 unfolding B_def by auto
lp15@70097
  1634
            then show "path_connectedin (subtopology ?E (C r)) (B r)"
lp15@70097
  1635
              by (simp add: path_connectedin_subtopology BC)
lp15@70097
  1636
          qed
lp15@70097
  1637
          moreover have "h ` B r \<subseteq> topspace ?E - h ` S r"
lp15@70097
  1638
            apply (auto simp: h_if_B)
lp15@70097
  1639
            by (metis BC SC disjSB disjnt_iff inj_onD [OF injh] subsetD)
lp15@70097
  1640
        ultimately show "path_connectedin (subtopology ?E (topspace ?E - h ` S r)) (h ` B r)"
lp15@70097
  1641
          by (simp add: path_connectedin_subtopology)
lp15@70097
  1642
      qed metis
lp15@70097
  1643
      show "\<exists>T. T \<in> path_components_of (subtopology ?E (topspace ?E - h ` S r)) \<and> topspace ?E - h ` (C r) \<subseteq> T"
lp15@70097
  1644
      proof (rule exists_path_component_of_superset [OF _ top_hSr_ne])
lp15@70097
  1645
        have eq: "topspace ?E - {x \<in> topspace ?E. enorm x \<le> r} = {x \<in> topspace ?E. r < enorm x}"
lp15@70097
  1646
          by auto
lp15@70097
  1647
        have "path_connectedin ?E (topspace ?E - C r)"
lp15@70097
  1648
          using pc_interval[of "{r<..}"] is_interval_convex_1 unfolding C_def eq by auto
lp15@70097
  1649
        then have "path_connectedin ?E (topspace ?E - h ` C r)"
lp15@70097
  1650
          by (metis biglemma [OF \<open>n \<noteq> 0\<close> compactinC cmh injh])
lp15@70097
  1651
        then show "path_connectedin (subtopology ?E (topspace ?E - h ` S r)) (topspace ?E - h ` C r)"
lp15@70097
  1652
          by (simp add: Diff_mono SC image_mono path_connectedin_subtopology)
lp15@70097
  1653
      qed metis
lp15@70097
  1654
      have "topspace ?E \<inter> (topspace ?E - h ` S r) = h ` B r \<union> (topspace ?E - h ` C r)"         (is "?lhs = ?rhs")
lp15@70097
  1655
      proof
lp15@70097
  1656
        show "?lhs \<subseteq> ?rhs"
lp15@70097
  1657
          using \<open>\<And>r. B r \<union> S r = C r\<close> by auto
lp15@70097
  1658
        have "h ` B r \<inter> h ` S r = {}"
lp15@70097
  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)
lp15@70097
  1660
        then show "?rhs \<subseteq> ?lhs"
lp15@70097
  1661
          using path_components_of_subset pc1 \<open>\<And>r. B r \<union> S r = C r\<close>
lp15@70097
  1662
          by (fastforce simp add: h_if_B)
lp15@70097
  1663
      qed
lp15@70097
  1664
      then show "\<Union> (path_components_of (subtopology ?E (topspace ?E - h ` S r))) = h ` B r \<union> (topspace ?E - h ` (C r))"
lp15@70097
  1665
        by (simp add: Union_path_components_of)
lp15@70097
  1666
      show "T \<noteq> {}"
lp15@70097
  1667
        if "T \<in> path_components_of (subtopology ?E (topspace ?E - h ` S r))" for T
lp15@70097
  1668
        using that by (simp add: nonempty_path_components_of)
lp15@70097
  1669
      show "disjoint (path_components_of (subtopology ?E (topspace ?E - h ` S r)))"
lp15@70097
  1670
        by (simp add: pairwise_disjoint_path_components_of)
lp15@70097
  1671
      have "\<not> path_connectedin ?E (topspace ?E - h ` S r)"
lp15@70097
  1672
      proof (subst biglemma [OF \<open>n \<noteq> 0\<close> compactinS])
lp15@70097
  1673
        show "continuous_map (subtopology ?E (S r)) ?E h"
lp15@70097
  1674
          by (metis Un_commute Un_upper1 cmh continuous_map_from_subtopology_mono eqC)
lp15@70097
  1675
        show "inj_on h (S r)"
lp15@70097
  1676
          using SC inj_on_subset injh by blast
lp15@70097
  1677
        show "\<not> path_connectedin ?E (topspace ?E - S r)"
lp15@70097
  1678
        proof
lp15@70097
  1679
          have "topspace ?E - S r = {x \<in> topspace ?E. enorm x \<noteq> r}"
lp15@70097
  1680
            by (auto simp: S_def)
lp15@70097
  1681
          moreover have "enorm ` {x \<in> topspace ?E. enorm x \<noteq> r} = {0..} - {r}"
lp15@70097
  1682
          proof
lp15@70097
  1683
            have "\<exists>x. x \<in> topspace ?E \<and> enorm x \<noteq> r \<and> d = enorm x"
lp15@70097
  1684
              if "d \<noteq> r" "d \<ge> 0" for d
lp15@70097
  1685
            proof (intro exI conjI)
lp15@70097
  1686
              show "(\<lambda>i. if i = 0 then d else 0) \<in> topspace ?E"
lp15@70097
  1687
                using \<open>n \<noteq> 0\<close> by (auto simp: Euclidean_space_def)
lp15@70097
  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)"
lp15@70097
  1689
                using \<open>n \<noteq> 0\<close> that by simp_all
lp15@70097
  1690
            qed
lp15@70097
  1691
            then show "{0..} - {r} \<subseteq> enorm ` {x \<in> topspace ?E. enorm x \<noteq> r}"
lp15@70097
  1692
              by (auto simp: image_def)
lp15@70097
  1693
          qed (auto simp: enorm_ge0)
lp15@70097
  1694
          ultimately have non_r: "enorm ` (topspace ?E - S r) = {0..} - {r}"
lp15@70097
  1695
            by simp
lp15@70097
  1696
          have "\<exists>x\<ge>0. x \<noteq> r \<and> r \<le> x"
lp15@70097
  1697
            by (metis gt_ex le_cases not_le order_trans)
lp15@70097
  1698
          then have "\<not> is_interval ({0..} - {r})"
lp15@70097
  1699
            unfolding is_interval_1
lp15@70097
  1700
            using  \<open>r > 0\<close> by (auto simp: Bex_def)
lp15@70097
  1701
          then show False
lp15@70097
  1702
            if "path_connectedin ?E (topspace ?E - S r)"
lp15@70097
  1703
            using path_connectedin_continuous_map_image [OF cm_enorm that] by (simp add: is_interval_path_connected_1 non_r)
lp15@70097
  1704
        qed
lp15@70097
  1705
      qed
lp15@70097
  1706
      then have "\<not> path_connected_space (subtopology ?E (topspace ?E - h ` S r))"
lp15@70097
  1707
        by (simp add: path_connectedin_def)
lp15@70097
  1708
      then show "\<nexists>T. path_components_of (subtopology ?E (topspace ?E - h ` S r)) \<subseteq> {T}"
lp15@70097
  1709
        by (simp add: path_components_of_subset_singleton)
lp15@70097
  1710
    qed
lp15@70097
  1711
    moreover have "openin ?E A"
lp15@70097
  1712
      if "A \<in> path_components_of (subtopology ?E (topspace ?E - h ` (S r)))" for A
lp15@70097
  1713
      using locally_path_connected_Euclidean_space [of n] that ope_comp_hSr
lp15@70097
  1714
      by (simp add: locally_path_connected_space_open_path_components)
lp15@70097
  1715
    ultimately show ?thesis by metis
lp15@70097
  1716
  qed
lp15@70097
  1717
  have "\<exists>T. openin ?E T \<and> f x \<in> T \<and> T \<subseteq> f ` U"
lp15@70097
  1718
    if "x \<in> U" for x
lp15@70097
  1719
  proof -
lp15@70097
  1720
    have x: "x \<in> topspace ?E"
lp15@70097
  1721
      by (meson U in_mono openin_subset that)
lp15@70097
  1722
    obtain V where V: "openin (powertop_real UNIV) V" and Ueq: "U = V \<inter> {x. \<forall>i\<ge>n. x i = 0}"
lp15@70097
  1723
      using U by (auto simp: openin_subtopology Euclidean_space_def)
lp15@70097
  1724
    with \<open>x \<in> U\<close> have "x \<in> V" by blast
lp15@70097
  1725
    then obtain T where Tfin: "finite {i. T i \<noteq> UNIV}" and Topen: "\<And>i. open (T i)"
lp15@70097
  1726
      and Tx: "x \<in> Pi\<^sub>E UNIV T" and TV: "Pi\<^sub>E UNIV T \<subseteq> V"
lp15@70097
  1727
      using V by (force simp: openin_product_topology_alt)
lp15@70097
  1728
    have "\<exists>e>0. \<forall>x'. \<bar>x' - x i\<bar> < e \<longrightarrow> x' \<in> T i" for i
lp15@70097
  1729
      using Topen [of i] Tx by (auto simp: open_real)
lp15@70097
  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"
lp15@70097
  1731
      by metis
lp15@70097
  1732
    define r where "r \<equiv> Min (insert 1 (\<beta> ` {i. T i \<noteq> UNIV}))"
lp15@70097
  1733
    have "r > 0"
lp15@70097
  1734
      by (simp add: B0 Tfin r_def)
lp15@70097
  1735
    have inU: "y \<in> U"
lp15@70097
  1736
      if y: "y \<in> topspace ?E" and yxr: "\<And>i. i<n \<Longrightarrow> \<bar>y i - x i\<bar> < r" for y
lp15@70097
  1737
    proof -
lp15@70097
  1738
      have "y i \<in> T i" for i
lp15@70097
  1739
      proof (cases "T i = UNIV")
lp15@70097
  1740
        show "y i \<in> T i" if "T i \<noteq> UNIV"
lp15@70097
  1741
        proof (cases "i < n")
lp15@70097
  1742
          case True
lp15@70097
  1743
          then show ?thesis
lp15@70097
  1744
            using yxr [OF True] that by (simp add: r_def BT Tfin)
lp15@70097
  1745
        next
lp15@70097
  1746
          case False
lp15@70097
  1747
          then show ?thesis
lp15@70097
  1748
            using B0 Ueq \<open>x \<in> U\<close> topspace_Euclidean_space y by (force intro: BT)
lp15@70097
  1749
        qed
lp15@70097
  1750
      qed auto
lp15@70097
  1751
      with TV have "y \<in> V" by auto
lp15@70097
  1752
      then show ?thesis
lp15@70097
  1753
        using that by (auto simp: Ueq topspace_Euclidean_space)
lp15@70097
  1754
    qed
lp15@70097
  1755
    have xinU: "(\<lambda>i. x i + y i) \<in> U" if "y \<in> C(r/2)" for y
lp15@70097
  1756
    proof (rule inU)
lp15@70097
  1757
      have y: "y \<in> topspace ?E"
lp15@70097
  1758
        using C_def that by blast
lp15@70097
  1759
      show "(\<lambda>i. x i + y i) \<in> topspace ?E"
lp15@70097
  1760
        using x y by (simp add: topspace_Euclidean_space)
lp15@70097
  1761
      have "enorm y \<le> r/2"
lp15@70097
  1762
        using that by (simp add: C_def)
lp15@70097
  1763
      then show "\<bar>x i + y i - x i\<bar> < r" if "i < n" for i
lp15@70097
  1764
        using le_enorm enorm_ge0 that \<open>0 < r\<close> leI order_trans by fastforce
lp15@70097
  1765
    qed
lp15@70097
  1766
    show ?thesis
lp15@70097
  1767
    proof (intro exI conjI)
lp15@70097
  1768
      show "openin ?E ((f \<circ> (\<lambda>y i. x i + y i)) ` B (r/2))"
lp15@70097
  1769
      proof (rule **)
lp15@70097
  1770
        have "continuous_map (subtopology ?E (C(r/2))) (subtopology ?E U) (\<lambda>y i. x i + y i)"
lp15@70097
  1771
          by (auto simp: xinU continuous_map_in_subtopology
lp15@70097
  1772
              intro!: continuous_intros continuous_map_Euclidean_space_add x)
lp15@70097
  1773
        then show "continuous_map (subtopology ?E (C(r/2))) ?E (f \<circ> (\<lambda>y i. x i + y i))"
lp15@70097
  1774
          by (rule continuous_map_compose) (simp add: cmf)
lp15@70097
  1775
        show "inj_on (f \<circ> (\<lambda>y i. x i + y i)) (C(r/2))"
lp15@70097
  1776
        proof (clarsimp simp add: inj_on_def C_def topspace_Euclidean_space simp del: divide_const_simps)
lp15@70097
  1777
          show "y' = y"
lp15@70097
  1778
            if ey: "enorm y \<le> r / 2" and ey': "enorm y' \<le> r / 2"
lp15@70097
  1779
              and y0: "\<forall>i\<ge>n. y i = 0" and y'0: "\<forall>i\<ge>n. y' i = 0"
lp15@70097
  1780
              and feq: "f (\<lambda>i. x i + y' i) = f (\<lambda>i. x i + y i)"
lp15@70097
  1781
            for y' y :: "nat \<Rightarrow> real"
lp15@70097
  1782
          proof -
lp15@70097
  1783
            have "(\<lambda>i. x i + y i) \<in> U"
lp15@70097
  1784
            proof (rule inU)
lp15@70097
  1785
              show "(\<lambda>i. x i + y i) \<in> topspace ?E"
lp15@70097
  1786
                using topspace_Euclidean_space x y0 by auto
lp15@70097
  1787
              show "\<bar>x i + y i - x i\<bar> < r" if "i < n" for i
lp15@70097
  1788
                using ey le_enorm [of _ y] \<open>r > 0\<close> that by fastforce
lp15@70097
  1789
            qed
lp15@70097
  1790
            moreover have "(\<lambda>i. x i + y' i) \<in> U"
lp15@70097
  1791
            proof (rule inU)
lp15@70097
  1792
              show "(\<lambda>i. x i + y' i) \<in> topspace ?E"
lp15@70097
  1793
                using topspace_Euclidean_space x y'0 by auto
lp15@70097
  1794
              show "\<bar>x i + y' i - x i\<bar> < r" if "i < n" for i
lp15@70097
  1795
                using ey' le_enorm [of _ y'] \<open>r > 0\<close> that by fastforce
lp15@70097
  1796
            qed
lp15@70097
  1797
            ultimately have "(\<lambda>i. x i + y' i) = (\<lambda>i. x i + y i)"
lp15@70097
  1798
              using feq by (meson \<open>inj_on f U\<close> inj_on_def)
lp15@70097
  1799
            then show ?thesis
lp15@70097
  1800
              by (auto simp: fun_eq_iff)
lp15@70097
  1801
          qed
lp15@70097
  1802
        qed
lp15@70097
  1803
      qed (simp add: \<open>0 < r\<close>)
lp15@70097
  1804
      have "x \<in> (\<lambda>y i. x i + y i) ` B (r / 2)"
lp15@70097
  1805
      proof
lp15@70097
  1806
        show "x = (\<lambda>i. x i + zero i)"
lp15@70097
  1807
          by (simp add: zero_def)
lp15@70097
  1808
      qed (auto simp: B_def \<open>r > 0\<close>)
lp15@70097
  1809
      then show "f x \<in> (f \<circ> (\<lambda>y i. x i + y i)) ` B (r/2)"
lp15@70097
  1810
        by (metis image_comp image_eqI)
lp15@70097
  1811
      show "(f \<circ> (\<lambda>y i. x i + y i)) ` B (r/2) \<subseteq> f ` U"
lp15@70097
  1812
        using \<open>\<And>r. B r \<subseteq> C r\<close> xinU by fastforce
lp15@70097
  1813
    qed
lp15@70097
  1814
  qed
lp15@70097
  1815
  then show ?thesis
lp15@70097
  1816
    using openin_subopen by force
lp15@70097
  1817
qed
lp15@70097
  1818
lp15@70097
  1819
lp15@70097
  1820
corollary invariance_of_domain_Euclidean_space_embedding_map:
lp15@70097
  1821
  assumes "openin (Euclidean_space n) U"
lp15@70097
  1822
    and cmf: "continuous_map(subtopology (Euclidean_space n) U) (Euclidean_space n) f"
lp15@70097
  1823
    and "inj_on f U"
lp15@70097
  1824
  shows "embedding_map(subtopology (Euclidean_space n) U) (Euclidean_space n) f"
lp15@70097
  1825
proof (rule injective_open_imp_embedding_map [OF cmf])
lp15@70097
  1826
  show "open_map (subtopology (Euclidean_space n) U) (Euclidean_space n) f"
lp15@70097
  1827
    unfolding open_map_def
lp15@70097
  1828
    by (meson assms continuous_map_from_subtopology_mono inj_on_subset invariance_of_domain_Euclidean_space openin_imp_subset openin_trans_full)
lp15@70097
  1829
  show "inj_on f (topspace (subtopology (Euclidean_space n) U))"
lp15@70097
  1830
    using assms openin_subset topspace_subtopology_subset by fastforce
lp15@70097
  1831
qed
lp15@70097
  1832
lp15@70097
  1833
corollary invariance_of_domain_Euclidean_space_gen:
lp15@70097
  1834
  assumes "n \<le> m" and U: "openin (Euclidean_space m) U"
lp15@70097
  1835
    and cmf: "continuous_map(subtopology (Euclidean_space m) U) (Euclidean_space n) f"
lp15@70097
  1836
    and "inj_on f U"
lp15@70097
  1837
  shows "openin (Euclidean_space n) (f ` U)"
lp15@70097
  1838
proof -
lp15@70097
  1839
  have *: "Euclidean_space n = subtopology (Euclidean_space m) (topspace(Euclidean_space n))"
lp15@70097
  1840
    by (metis Euclidean_space_def \<open>n \<le> m\<close> inf.absorb_iff2 subset_Euclidean_space subtopology_subtopology topspace_Euclidean_space)
lp15@70097
  1841
  moreover have "U \<subseteq> topspace (subtopology (Euclidean_space m) U)"
lp15@70097
  1842
    by (metis U inf.absorb_iff2 openin_subset openin_subtopology openin_topspace)
lp15@70097
  1843
  ultimately show ?thesis
lp15@70097
  1844
    by (metis (no_types) U \<open>inj_on f U\<close> cmf continuous_map_in_subtopology inf.absorb_iff2
lp15@70097
  1845
        inf.orderE invariance_of_domain_Euclidean_space openin_imp_subset openin_subtopology openin_topspace)
lp15@70097
  1846
qed
lp15@70097
  1847
lp15@70097
  1848
corollary invariance_of_domain_Euclidean_space_embedding_map_gen:
lp15@70097
  1849
  assumes "n \<le> m" and U: "openin (Euclidean_space m) U"
lp15@70097
  1850
    and cmf: "continuous_map(subtopology (Euclidean_space m) U) (Euclidean_space n) f"
lp15@70097
  1851
    and "inj_on f U"
lp15@70097
  1852
  shows "embedding_map(subtopology (Euclidean_space m) U) (Euclidean_space n) f"
lp15@70097
  1853
  proof (rule injective_open_imp_embedding_map [OF cmf])
lp15@70097
  1854
  show "open_map (subtopology (Euclidean_space m) U) (Euclidean_space n) f"
lp15@70097
  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)
lp15@70097
  1856
  show "inj_on f (topspace (subtopology (Euclidean_space m) U))"
lp15@70097
  1857
    using assms openin_subset topspace_subtopology_subset by fastforce
lp15@70097
  1858
qed
lp15@70097
  1859
lp15@70097
  1860
lp15@70097
  1861
subsection\<open>Relating two variants of Euclidean space, one within product topology.    \<close>
lp15@70097
  1862
lp15@70097
  1863
proposition homeomorphic_maps_Euclidean_space_euclidean_gen_OLD:
lp15@70097
  1864
  fixes B :: "'n::euclidean_space set"
lp15@70097
  1865
  assumes "finite B" "independent B" and orth: "pairwise orthogonal B" and n: "card B = n"
lp15@70097
  1866
  obtains f g where "homeomorphic_maps (Euclidean_space n) (top_of_set (span B)) f g"
lp15@70097
  1867
proof -
lp15@70097
  1868
  note representation_basis [OF \<open>independent B\<close>, simp]
lp15@70097
  1869
  obtain b where injb: "inj_on b {..<n}" and beq: "b ` {..<n} = B"
lp15@70097
  1870
    using finite_imp_nat_seg_image_inj_on [OF \<open>finite B\<close>]
lp15@70097
  1871
    by (metis n card_Collect_less_nat card_image lessThan_def)
lp15@70097
  1872
  then have biB: "\<And>i. i < n \<Longrightarrow> b i \<in> B"
lp15@70097
  1873
    by force
lp15@70097
  1874
  have repr: "\<And>v. v \<in> span B \<Longrightarrow> (\<Sum>i<n. representation B v (b i) *\<^sub>R b i) = v"
lp15@70097
  1875
    using real_vector.sum_representation_eq [OF \<open>independent B\<close> _ \<open>finite B\<close>]
lp15@70097
  1876
    by (metis (no_types, lifting) injb beq order_refl sum.reindex_cong)
lp15@70097
  1877
  let ?f = "\<lambda>x. \<Sum>i<n. x i *\<^sub>R b i"
lp15@70097
  1878
  let ?g = "\<lambda>v i. if i < n then representation B v (b i) else 0"
lp15@70097
  1879
  show thesis
lp15@70097
  1880
  proof
lp15@70097
  1881
    show "homeomorphic_maps (Euclidean_space n) (top_of_set (span B)) ?f ?g"
lp15@70097
  1882
      unfolding homeomorphic_maps_def
lp15@70097
  1883
    proof (intro conjI)
lp15@70097
  1884
      have *: "continuous_map euclidean (top_of_set (span B)) ?f"
lp15@70097
  1885
        by (metis (mono_tags) biB continuous_map_span_sum lessThan_iff)
lp15@70097
  1886
      show "continuous_map (Euclidean_space n) (top_of_set (span B)) ?f"
lp15@70097
  1887
        unfolding Euclidean_space_def
lp15@70097
  1888
        by (rule continuous_map_from_subtopology) (simp add: euclidean_product_topology *)
lp15@70097
  1889
      show "continuous_map (top_of_set (span B)) (Euclidean_space n) ?g"
lp15@70097
  1890
        unfolding Euclidean_space_def
lp15@70097
  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)
lp15@70097
  1892
      have [simp]: "\<And>x i. i<n \<Longrightarrow> x i *\<^sub>R b i \<in> span B"
lp15@70097
  1893
        by (simp add: biB span_base span_scale)
lp15@70097
  1894
      have "representation B (?f x) (b j) = x j"
lp15@70097
  1895
        if 0: "\<forall>i\<ge>n. x i = (0::real)" and "j < n" for x j
lp15@70097
  1896
      proof -
lp15@70097
  1897
        have "representation B (?f x) (b j) = (\<Sum>i<n. representation B (x i *\<^sub>R b i) (b j))"
lp15@70097
  1898
          by (subst real_vector.representation_sum) (auto simp add: \<open>independent B\<close>)
lp15@70097
  1899
        also have "... = (\<Sum>i<n. x i * representation B (b i) (b j))"
lp15@70097
  1900
          by (simp add: assms(2) biB representation_scale span_base)
lp15@70097
  1901
        also have "... = (\<Sum>i<n. if b j = b i then x i else 0)"
lp15@70097
  1902
          by (simp add: biB if_distrib cong: if_cong)
lp15@70097
  1903
        also have "... = x j"
lp15@70097
  1904
          using that inj_on_eq_iff [OF injb] by auto
lp15@70097
  1905
        finally show ?thesis .
lp15@70097
  1906
      qed
lp15@70097
  1907
      then show "\<forall>x\<in>topspace (Euclidean_space n). ?g (?f x) = x"
lp15@70097
  1908
        by (auto simp: Euclidean_space_def)
lp15@70097
  1909
      show "\<forall>y\<in>topspace (top_of_set (span B)). ?f (?g y) = y"
lp15@70097
  1910
        using repr by (auto simp: Euclidean_space_def)
lp15@70097
  1911
    qed
lp15@70097
  1912
  qed
lp15@70097
  1913
qed
lp15@70097
  1914
lp15@70097
  1915
proposition homeomorphic_maps_Euclidean_space_euclidean_gen:
lp15@70097
  1916
  fixes B :: "'n::euclidean_space set"
lp15@70097
  1917
  assumes "independent B" and orth: "pairwise orthogonal B" and n: "card B = n"
lp15@70097
  1918
    and 1: "\<And>u. u \<in> B \<Longrightarrow> norm u = 1"
lp15@70097
  1919
  obtains f g where "homeomorphic_maps (Euclidean_space n) (top_of_set (span B)) f g"
lp15@70097
  1920
    and "\<And>x. x \<in> topspace (Euclidean_space n) \<Longrightarrow> (norm (f x))\<^sup>2 = (\<Sum>i<n. (x i)\<^sup>2)"
lp15@70097
  1921
proof -
lp15@70097
  1922
  note representation_basis [OF \<open>independent B\<close>, simp]
lp15@70097
  1923
  have "finite B"
lp15@70097
  1924
    using \<open>independent B\<close> finiteI_independent by metis
lp15@70097
  1925
  obtain b where injb: "inj_on b {..<n}" and beq: "b ` {..<n} = B"
lp15@70097
  1926
    using finite_imp_nat_seg_image_inj_on [OF \<open>finite B\<close>]
lp15@70097
  1927
    by (metis n card_Collect_less_nat card_image lessThan_def)
lp15@70097
  1928
  then have biB: "\<And>i. i < n \<Longrightarrow> b i \<in> B"
lp15@70097
  1929
    by force
lp15@70097
  1930
  have "0 \<notin> B"
lp15@70097
  1931
    using \<open>independent B\<close> dependent_zero by blast
lp15@70097
  1932
  have [simp]: "b i \<bullet> b j = (if j = i then 1 else 0)"
lp15@70097
  1933
    if "i < n" "j < n" for i j
lp15@70097
  1934
  proof (cases "i = j")
lp15@70097
  1935
    case True
lp15@70097
  1936
    with 1 that show ?thesis
lp15@70097
  1937
      by (auto simp: norm_eq_sqrt_inner biB)
lp15@70097
  1938
  next
lp15@70097
  1939
    case False
lp15@70097
  1940
    then have "b i \<noteq> b j"
lp15@70097
  1941
      by (meson inj_onD injb lessThan_iff that)
lp15@70097
  1942
    then show ?thesis
lp15@70097
  1943
      using orth by (auto simp: orthogonal_def pairwise_def norm_eq_sqrt_inner that biB)
lp15@70097
  1944
  qed
lp15@70097
  1945
  have [simp]: "\<And>x i. i<n \<Longrightarrow> x i *\<^sub>R b i \<in> span B"
lp15@70097
  1946
    by (simp add: biB span_base span_scale)
lp15@70097
  1947
  have repr: "\<And>v. v \<in> span B \<Longrightarrow> (\<Sum>i<n. representation B v (b i) *\<^sub>R b i) = v"
lp15@70097
  1948
    using real_vector.sum_representation_eq [OF \<open>independent B\<close> _ \<open>finite B\<close>]
lp15@70097
  1949
    by (metis (no_types, lifting) injb beq order_refl sum.reindex_cong)
lp15@70097
  1950
    define f where "f \<equiv> \<lambda>x. \<Sum>i<n. x i *\<^sub>R b i"
lp15@70097
  1951
    define g where "g \<equiv> \<lambda>v i. if i < n then representation B v (b i) else 0"
lp15@70097
  1952
  show thesis
lp15@70097
  1953
  proof
lp15@70097
  1954
    show "homeomorphic_maps (Euclidean_space n) (top_of_set (span B)) f g"
lp15@70097
  1955
      unfolding homeomorphic_maps_def
lp15@70097
  1956
    proof (intro conjI)
lp15@70097
  1957
      have *: "continuous_map euclidean (top_of_set (span B)) f"
lp15@70097
  1958
        unfolding f_def
lp15@70097
  1959
        by (rule continuous_map_span_sum) (use biB \<open>0 \<notin> B\<close> in auto)
lp15@70097
  1960
      show "continuous_map (Euclidean_space n) (top_of_set (span B)) f"
lp15@70097
  1961
        unfolding Euclidean_space_def
lp15@70097
  1962
        by (rule continuous_map_from_subtopology) (simp add: euclidean_product_topology *)
lp15@70097
  1963
      show "continuous_map (top_of_set (span B)) (Euclidean_space n) g"
lp15@70097
  1964
        unfolding Euclidean_space_def g_def
lp15@70097
  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)
lp15@70097
  1966
      have "representation B (f x) (b j) = x j"
lp15@70097
  1967
        if 0: "\<forall>i\<ge>n. x i = (0::real)" and "j < n" for x j